name: Update nightly-testing

on:
    schedule:
        - cron: "0 10/6 * * *"
        # Run every six hours, starting at 11AM CET/2AM PT.
        # This should be 3 hours after lean4 starts building its nightly
    workflow_dispatch: # Allow manual triggering

env:
    TARGET_BRANCH: nightly-testing

jobs:
    # This job checks whether there's been a new nightly since the last
    # successful automatic update
    check-update:
        runs-on: nscloud-ubuntu-22.04-amd64-8x16
        if: github.repository == 'leanprover/reference-manual'
        outputs:
            update-needed: ${{ steps.check-update.outputs.update-needed }}
            latest-version: ${{ steps.latest-available.outputs.version }}

        steps:
            - name: Checkout repository
              uses: actions/checkout@v4
              with:
                  ref: ${{ env.TARGET_BRANCH }}
                  token: ${{ secrets.GITHUB_TOKEN }}

            - name: Configure Git
              run: |
                  git config user.name "github-actions[bot]"
                  git config user.email "github-actions[bot]@users.noreply.github.com"

            - name: Verify target branch exists
              run: |
                  if ! git show-ref --verify --quiet refs/heads/${{ env.TARGET_BRANCH }}; then
                    echo "Error: Target branch '${{ env.TARGET_BRANCH }}' does not exist"
                    exit 1
                  fi
                  echo "Target branch '${{ env.TARGET_BRANCH }}' exists"

            - name: Get current nightly version
              id: last-working
              run: |
                  TOOLCHAIN="$(cut -f2 -d: ./lean-toolchain)"
                  echo "version=$TOOLCHAIN" >> $GITHUB_OUTPUT

            - name: Get latest release tag from leanprover/lean4-nightly
              id: latest-available
              run: |
                  RELEASE_TAG="$(curl -s "https://api.github.com/repos/leanprover/lean4-nightly/releases" | jq -r '.[0].tag_name')"
                  echo "RELEASE_TAG=$RELEASE_TAG" >> "${GITHUB_ENV}"
                  echo "version=$RELEASE_TAG" >> $GITHUB_OUTPUT

            - name: Check if update needed
              id: check-update
              run: |
                  if [ "${{ steps.last-working.outputs.version }}" = "${{ steps.latest-available.outputs.version }}" ]; then
                    echo "No update needed - versions match"
                    echo "✅ Nightly version ${{ steps.last-working.outputs.version }} is already up to date"
                    echo "✅ Nightly version \`${{ steps.last-working.outputs.version }}\` is already up to date" >> $GITHUB_STEP_SUMMARY
                    echo "update-needed=false" >> $GITHUB_OUTPUT
                  else
                    echo "Update needed: ${{ steps.last-working.outputs.version }} -> ${{ steps.latest-available.outputs.version }}"
                    echo "Update needed: \`${{ steps.last-working.outputs.version }}\` -> \`${{ steps.latest-available.outputs.version }}\`" >> $GITHUB_STEP_SUMMARY
                    echo "update-needed=true" >> $GITHUB_OUTPUT
                  fi

    # This job tries to update nightly-testing, and pushes if successful
    test-and-update:
        runs-on: ubuntu-latest
        needs: check-update
        if: needs.check-update.outputs.update-needed == 'true'
        permissions:
            contents: write
        outputs:
            changes-pushed: ${{ steps.commit.outputs.changes-pushed }}

        steps:
            - name: Checkout repository
              uses: actions/checkout@v4
              with:
                  ref: ${{ env.TARGET_BRANCH }}
                  token: ${{ secrets.GITHUB_TOKEN }}

            - name: Configure Git
              run: |
                  git config user.name "github-actions[bot]"
                  git config user.email "github-actions[bot]@users.noreply.github.com"

            - name: Update toolchain file to ${{ needs.check-update.outputs.latest-version }}
              run: |
                  echo "leanprover/lean4:${{ needs.check-update.outputs.latest-version }}" > lean-toolchain

            - name: Install deps for figures (OS packages)
              run: |
                  sudo apt update && sudo apt install -y poppler-utils

            - name: Install deps for figures (TeX)
              uses: zauguin/install-texlive@v4
              with:
                  texlive_version: 2025
                  packages: |
                      scheme-small
                      latex-bin
                      fontspec
                      standalone
                      pgf
                      pdftexcmds
                      luatex85
                      lualatex-math
                      infwarerr
                      ltxcmds
                      xcolor
                      fontawesome
                      spath3
                      inter
                      epstopdf-pkg
                      tex-gyre
                      tex-gyre-math
                      unicode-math
                      amsmath
                      sourcecodepro

            - name: Do we have lualatex?
              run: |
                  lualatex --version

            - name: Install elan
              run: |
                  set -o pipefail
                  curl -sSfL https://github.com/leanprover/elan/releases/download/v4.1.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
                  ./elan-init -y --default-toolchain none
                  echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

            - name: Build figures
              run: |
                  lake build figures

            - name: Build
              run: |
                  lake build

            - name: Generate HTML
              if: steps.check-update.outputs.update-needed == 'true'
              run: |
                  lake exe generate-manual --depth 2 --without-html-single

            - name: Commit and push changes
              id: commit
              run: |
                  git add lean-toolchain
                  git commit -m "chore: bump to nightly ${{ needs.check-update.outputs.latest-version }}"
                  git push origin ${{ env.TARGET_BRANCH }}

                  if [[ -f "lean-toolchain" && $(cat "lean-toolchain") == leanprover/lean4:nightly-* ]]; then
                      toolchain=$(cat "lean-toolchain")
                      version=${toolchain#leanprover/lean4:nightly-}
                      git tag "nightly-testing-$version"
                      git push origin "nightly-testing-$version"
                      echo "changes-pushed=true" >> $GITHUB_OUTPUT
                  fi

    trigger-nightly-with-manual:
        needs: test-and-update
        if: needs.test-and-update.outputs.changes-pushed == 'true'
        uses: ./.github/workflows/nightly-with-manual.yml
        secrets: inherit