docs.yml

# Publishes the documentation site to GitHub Pages (gh-pages branch) with mike.
#   push to main  -> "dev" version (what's being built)
#   tag vX.Y.Z    -> version "X.Y", and "latest" moves to it
# Every published version stays available, so an older app's help links keep working.
name: Docs

on:
  push:
    branches: [main]
    tags: ["v*"]
    paths-ignore:
      - "docs/PLAN-*.md"
  workflow_dispatch:
    inputs:
      version:
        description: Docs version to publish (e.g. 0.1, or dev)
        required: true
        default: dev
      latest:
        description: Also point "latest" at it
        type: boolean
        default: false

permissions:
  contents: write # mike commits to gh-pages

concurrency:
  group: docs-publish
  cancel-in-progress: false

jobs:
  publish:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
        with:
          fetch-depth: 0 # mike needs gh-pages history

      - uses: actions/setup-java@v6
        with:
          distribution: temurin
          java-version: "21"

      - uses: gradle/actions/setup-gradle@v6

      - uses: actions/setup-python@v7
        with:
          python-version: "3.12"
          cache: pip
          cache-dependency-path: site/requirements.txt

      - name: Docs toolchain
        run: python -m venv site/.venv && site/.venv/bin/pip install -r site/requirements.txt

      - name: Generate and check
        run: make docs

      - name: Work out the version
        id: version
        run: |
          if [ "${{ github.event_name }}" = "workflow_dispatch" ]; then
            echo "name=${{ inputs.version }}" >> "$GITHUB_OUTPUT"
            echo "latest=${{ inputs.latest }}" >> "$GITHUB_OUTPUT"
          elif [[ "${GITHUB_REF}" == refs/tags/v* ]]; then
            tag="${GITHUB_REF#refs/tags/v}"
            echo "name=$(echo "$tag" | cut -d. -f1-2)" >> "$GITHUB_OUTPUT"
            echo "latest=true" >> "$GITHUB_OUTPUT"
          else
            echo "name=dev" >> "$GITHUB_OUTPUT"
            echo "latest=false" >> "$GITHUB_OUTPUT"
          fi

      - name: Publish with mike
        working-directory: site
        run: |
          git config user.name "github-actions[bot]"
          git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
          if [ "${{ steps.version.outputs.latest }}" = "true" ]; then
            .venv/bin/mike deploy --push --update-aliases "${{ steps.version.outputs.name }}" latest
            .venv/bin/mike set-default --push latest
          else
            .venv/bin/mike deploy --push "${{ steps.version.outputs.name }}"
            # Until the first release, the site root opens the dev docs.
            if ! .venv/bin/mike list | grep -q latest; then .venv/bin/mike set-default --push dev; fi
          fi