Bump lean-toolchain on nightly-testing #425
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: Bump lean-toolchain on nightly-testing | |
| on: | |
| schedule: | |
| - cron: '0 10/3 * * *' | |
| # Run every three hours, starting at 11AM CET/2AM PT. | |
| # This should be 3 hours after lean4 starts building its nightly. | |
| workflow_dispatch: | |
| jobs: | |
| update-toolchain: | |
| if: github.repository == 'leanprover/cslib' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Generate app token | |
| id: app-token | |
| uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1 | |
| with: | |
| app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }} | |
| private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }} | |
| # The create-github-app-token README states that this token is masked and will not be logged accidentally. | |
| - name: Checkout code | |
| uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| with: | |
| ref: nightly-testing # checkout nightly-testing branch | |
| token: ${{ steps.app-token.outputs.token }} | |
| - name: Get latest release tag from leanprover/lean4-nightly | |
| id: get-latest-release | |
| env: | |
| GH_TOKEN: ${{ steps.app-token.outputs.token }} | |
| run: | | |
| RELEASE_TAG=$(gh api -X GET repos/leanprover/lean4-nightly/releases \ | |
| -f per_page=1 --jq '.[0].tag_name') | |
| if [ -z "$RELEASE_TAG" ] || [ "$RELEASE_TAG" = "null" ]; then | |
| echo "::error::Could not determine latest lean4-nightly release" | |
| exit 1 | |
| fi | |
| echo "RELEASE_TAG=$RELEASE_TAG" >> "${GITHUB_ENV}" | |
| - name: Check if nightly-testing tag exists in mathlib4-nightly-testing | |
| id: check-nightly-testing | |
| env: | |
| GH_TOKEN: ${{ steps.app-token.outputs.token }} | |
| run: | | |
| # Extract date from RELEASE_TAG (format: nightly-YYYY-MM-DD) | |
| DATE_PART=$(echo "$RELEASE_TAG" | sed 's/nightly-//') | |
| NIGHTLY_TESTING_TAG="nightly-testing-${DATE_PART}" | |
| echo "NIGHTLY_TESTING_TAG=$NIGHTLY_TESTING_TAG" >> "${GITHUB_ENV}" | |
| # Check if the tag exists in leanprover-community/mathlib4-nightly-testing | |
| if gh api "repos/leanprover-community/mathlib4-nightly-testing/git/ref/tags/${NIGHTLY_TESTING_TAG}" > /dev/null 2>&1; then | |
| echo "Tag ${NIGHTLY_TESTING_TAG} exists in mathlib4-nightly-testing" | |
| echo "tag_exists=true" >> "${GITHUB_OUTPUT}" | |
| else | |
| echo "Tag ${NIGHTLY_TESTING_TAG} does not exist in mathlib4-nightly-testing" | |
| echo "tag_exists=false" >> "${GITHUB_OUTPUT}" | |
| fi | |
| - name: Configure Lean | |
| uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| - name: Update toolchain and dependencies | |
| if: steps.check-nightly-testing.outputs.tag_exists == 'true' | |
| run: | | |
| # Update lean-toolchain file | |
| echo "leanprover/lean4:${RELEASE_TAG}" > lean-toolchain | |
| # Verify lakefile.toml has git-based mathlib4-nightly-testing dependency | |
| if ! grep -q 'git = "https://github.com/leanprover-community/mathlib4-nightly-testing"' lakefile.toml; then | |
| echo "Error: lakefile.toml must already have a git-based mathlib4-nightly-testing dependency" | |
| exit 1 | |
| fi | |
| # Update only the rev field for the mathlib4-nightly-testing dependency | |
| # Find the line after the git URL and update the rev on the next line | |
| sed -i '/git = "https:\/\/github\.com\/leanprover-community\/mathlib4-nightly-testing"/,/^rev = / s/^rev = .*/rev = "'"${NIGHTLY_TESTING_TAG}"'"/' lakefile.toml | |
| # Update dependencies | |
| lake update | |
| - name: Commit and push changes | |
| if: steps.check-nightly-testing.outputs.tag_exists == 'true' | |
| run: | | |
| git config user.name "mathlib-nightly-testing[bot]" | |
| git config user.email "mathlib-nightly-testing[bot]@users.noreply.github.com" | |
| git add lean-toolchain lakefile.toml lake-manifest.json | |
| # Don't fail if there's nothing to commit | |
| git commit -m "chore: bump to ${RELEASE_TAG} with mathlib at ${NIGHTLY_TESTING_TAG}" || true | |
| git push origin nightly-testing |