docs-build.yaml

name: docs-build

on:
  pull_request:
    branches: [ main, release-* ]
    types: [ opened, synchronize ]

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

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

defaults:
  run:
    shell: bash

jobs:
  build-docs:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout
        uses: actions/checkout@v4
      - name: Build image
        run: |
          docker build --pull --tag docs-builder:latest --file docs/Dockerfile .
      - name: Build docs
        run: |
          docker run -v $(pwd):/work -w /work docs-builder:latest sphinx-build -b html -d /tmp docs docs/_build/output
      - name: Delete unnecessary files
        run: |
          sudo rm -rf docs/_build/jupyter_execute
          sudo rm -rf docs/_build/.buildinfo
      - name: Upload HTML
        uses: actions/upload-artifact@v4
        with:
          name: html-build-artifact
          path: docs/_build/
          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@v4
        with:
          name: pr
          path: pr/

  store-html:
    needs: [ build-docs ]
    if: ${{ github.event_name == 'push' }}
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
        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@v4
        with:
          name: html-build-artifact
      - name: Copy HTML directories
        run: |
          ls -asl
      - name: Store bleeding edge docs from main
        if: ${{ github.ref == 'refs/heads/main' }}
        run: |
          mkdir main || true
          rsync -av --progress --delete output/ main/
          git add main
      - name: Store docs for a release tag
        if: ${{ startsWith(github.ref, 'refs/tags/v') }}
        env:
          LATEST: ${{ contains(github.event.head_commit.message, '/not-latest') && 'not-true' || 'true' }}
        run: |
          printenv LATEST
          if [[ "${GITHUB_REF}" =~ "-rc" ]]; then
            echo "Not saving documents for release candidates."
            exit 0
          fi
          if [[ "${GITHUB_REF}" =~ v([0-9]+\.[0-9]+\.[0-9]+) ]]; then
            TAG="${BASH_REMATCH[1]}"
            mkdir "${TAG}" || true
            rsync -av --progress --delete output/ "${TAG}/"
            git add "${TAG}/"
            if [[ "${LATEST}" == 'true' ]]; then
              mkdir latest || true
              rsync -av --progress --delete output/ latest/
              cp output/versions.json .
              git add latest
              git add versions.json
            fi
          fi
      - 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.
          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}'/latest/index.html">'        >> index.html
          echo '    <link rel="canonical" href="'${html_url}'/latest/index.html">'                      >> index.html
          echo '    <script language="javascript">'                                                     >> index.html
          echo '      function redirect() {'                                                            >> index.html
          echo '        window.location.assign("'${html_url}'/latest/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}'/latest/index.html">'        >> index.html
          echo 'latest</a> 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