docs-build.yaml

name: docs-build

on:
  pull_request:
    branches: [ master ]
    types: [ opened, synchronize ]

  push:
    branches: [ master ]
    tags:
      - v*
  workflow_dispatch:

env:
  REGISTRY: ghcr.io
  IMAGE_NAME: ${{ github.repository }}
  TAG: 0.1.0

concurrency:
  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
  cancel-in-progress: true

jobs:
  dockerfile-changed:
    runs-on: ubuntu-latest
    permissions:
      contents: read
    outputs:
      changed: ${{ steps.change.outputs.changed }}
      image: ${{ steps.change.outputs.image }}
    steps:
      - name: Checkout
        uses: actions/checkout@v3
        with:
          fetch-depth: 2
      - name: Detect change
        id: change
        run: |
          first_commit=$(git rev-list HEAD | tail -n 1)
          diff=$(git diff --name-only HEAD..${first_commit})
          if [[ "${diff}" =~ docker/Dockerfile ]] && [[ "${{ github.event_name }}" == 'pull_request' ]]; then
            echo "changed=true" >> "$GITHUB_OUTPUT"
            echo "image=${REGISTRY}/${IMAGE_NAME}:${{ github.event.pull_request.number }}" >> "$GITHUB_OUTPUT"
          else
            echo "changed=false" >> "$GITHUB_OUTPUT"
            echo "image=${REGISTRY}/${IMAGE_NAME}:${TAG}" >> "$GITHUB_OUTPUT"
          fi
        shell: bash

  build-and-push-image:
    needs: dockerfile-changed
    if: needs.dockerfile-changed.outputs.changed == 'true'
    runs-on: ubuntu-latest
    permissions:
      contents: read
      packages: write
    steps:
      - name: Checkout
        uses: actions/checkout@v3
        with:
          fetch-depth: 1
      - name: Log in to Container Registry
        uses: docker/login-action@v2
        with:
          registry: ${{ env.REGISTRY }}
          username: ${{ github.actor }}
          password: ${{ secrets.GITHUB_TOKEN }}
      - name: Build and push
        uses: docker/build-push-action@v4
        with:
          context: .
          file: docker/Dockerfile
          push: true
          tags: ${{ needs.dockerfile-changed.outputs.image }}

  build-docs:
    needs: [dockerfile-changed, build-and-push-image]
    if: ${{ always() }}
    runs-on: ubuntu-latest
    container:
      image: ${{ needs.dockerfile-changed.outputs.image }}
    steps:
      - name: Checkout
        uses: actions/checkout@v3
        with:
          fetch-depth: 1
      - name: Set ownership
        run: |
          chown -R $(id -u):$(id -g) $PWD
      - name: Build docs
        run: |
          make html
      - name: Delete unnecessary files
        run: |
          find _build/html -name .doctrees -prune -exec rm -rf {} \;
          find _build/html -name .buildinfo -exec rm {} \;
      - name: Upload HTML
        uses: actions/upload-artifact@v3
        with:
          name: html-build-artifact
          path: _build/html
          if-no-files-found: error
          retention-days: 1
      - name: Store PR information
        if: ${{ github.event_name == 'pull_request' }}
        run: |
          mkdir ./pr
          echo ${{ github.event.number }}              > ./pr/pr.txt
          echo ${{ github.event.pull_request.merged }} > ./pr/merged.txt
          echo ${{ github.event.action }}              > ./pr/action.txt
      - name: Upload PR information
        if: ${{ github.event_name == 'pull_request' }}
        uses: actions/upload-artifact@v3
        with:
          name: pr
          path: pr/

  store-html:
    needs: [ build-docs ]
    if: ${{ github.event_name == 'push' }}
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v3
        with:
          ref: "gh-pages"
      - name: Initialize Git configuration
        run: |
          git config user.name docs-build
          git config user.email do-not-send@github.com
      - name: Download artifacts
        uses: actions/download-artifact@v3
        with:
          name: html-build-artifact
      - name: Copy HTML directories
        run: |
          ls -asl
          for i in `ls -d *`
          do
            echo "Git adding ${i}"
            git add "${i}"
          done
      - name: Check or create dot-no-jekyll file
        run: |
          if [ -f ".nojekyll" ]; then
            echo "The dot-no-jekyll file already exists."
            exit 0
          fi
          touch .nojekyll
          git add .nojekyll
      - name: Check or create redirect page
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
        run: |
          resp=$(grep 'http-equiv="refresh"' index.html 2>/dev/null) || true
          if [ -n "${resp}" ]; then
            echo "The redirect file already exists."
            exit 0
          fi
          # If any of these commands fail, fail the build.
          def_branch=$(gh api "repos/${GITHUB_REPOSITORY}" --jq ".default_branch")
          html_url=$(gh api "repos/${GITHUB_REPOSITORY}/pages" --jq ".html_url")
          # Beware ugly quotation mark avoidance in the foll lines.
          echo '<!DOCTYPE html>'                                                                         > index.html
          echo '<html>'                                                                                 >> index.html
          echo '  <head>'                                                                               >> index.html
          echo '    <title>Redirect to documentation</title>'                                           >> index.html
          echo '    <meta charset="utf-8">'                                                             >> index.html
          echo '    <meta http=equiv="refresh" content="3; URL='${html_url}${def_branch}'/index.html">' >> index.html
          echo '    <link rel="canonical" href="'${html_url}${def_branch}'/index.html">'                >> index.html
          echo '    <script language="javascript">'                                                     >> index.html
          echo '      function redirect() {'                                                            >> index.html
          echo '        window.location.assign("'${html_url}${def_branch}'/index.html")'                >> index.html
          echo '      }'                                                                                >> index.html
          echo '    </script>'                                                                          >> index.html
          echo '  </head>'                                                                              >> index.html
          echo '  <body onload="redirect()">'                                                           >> index.html
          echo '    <p>Please follow the link to the <a href="'${html_url}${def_branch}'/index.html">'  >> index.html
          echo      ${def_branch}'</a> branch documentation.</p>'                                       >> index.html
          echo '  </body>'                                                                              >> index.html
          echo '</html>'                                                                                >> index.html
          git add index.html
      - name: Commit changes to the GitHub Pages branch
        run: |
          git status
          if git commit -m 'Pushing changes to GitHub Pages.'; then
            git push -f
          else
           echo "Nothing changed."
          fi