Update nightly-testing #353
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 | |
| 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 | |
| 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" | |
| fi |