Daily CI Workflow #307
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: Daily CI Workflow | |
| # This workflow runs daily on `master` and the latest `nightly-testing-YYYY-MM-DD` tag, | |
| # running some expensive CI checks that we don't want to run on every PR. | |
| # It reports results via Zulip. | |
| # This script requires that the ZULIP_API_KEY secret is available in both | |
| # `leanprover-community/mathlib4` and `leanprover-community/mathlib4-nightly-testing` | |
| # repositories. | |
| on: | |
| schedule: | |
| - cron: '0 0 * * *' # Runs at 00:00 UTC every day | |
| workflow_dispatch: | |
| env: | |
| DEFAULT_BRANCH: master | |
| TAG_PATTERN: '^nightly-testing-[0-9]{4}-[0-9]{2}-[0-9]{2}$' | |
| jobs: | |
| check-lean4checker: | |
| runs-on: ubuntu-latest | |
| if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing' | |
| strategy: | |
| matrix: | |
| branch_type: [master, nightly] | |
| steps: | |
| - name: Cleanup | |
| run: | | |
| # Delete all but the 5 most recent toolchains. | |
| # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file. | |
| # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`. | |
| if cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"'; then | |
| : # Do nothing on success | |
| else | |
| : # Do nothing on failure, but suppress errors | |
| fi | |
| # Checkout repository, so that we can fetch tags to decide which branch we want. | |
| - name: Checkout branch or tag | |
| uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - name: Fetch latest tags (if nightly) | |
| if: matrix.branch_type == 'nightly' | |
| run: | | |
| # When in nightly mode, fetch tags from the nightly-testing repository | |
| git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git | |
| git fetch nightly-testing --tags | |
| LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1) | |
| echo "LATEST_TAG=${LATEST_TAG}" >> "$GITHUB_ENV" | |
| - name: Set branch ref | |
| run: | | |
| if [ "${{ matrix.branch_type }}" == "master" ]; then | |
| echo "BRANCH_REF=${{ env.DEFAULT_BRANCH }}" >> "$GITHUB_ENV" | |
| else | |
| echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV" | |
| fi | |
| # Checkout the branch or tag we want to test. | |
| - name: Checkout branch or tag | |
| uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| with: | |
| repository: ${{ matrix.branch_type == 'nightly' && 'leanprover-community/mathlib4-nightly-testing' || github.repository }} | |
| ref: ${{ env.BRANCH_REF }} | |
| - name: Configure Lean | |
| uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| reinstall-transient-toolchain: true | |
| - name: Run lake exe cache get | |
| run: | | |
| lake exe cache get | |
| - name: Check environments using lean4checker | |
| id: lean4checker | |
| continue-on-error: true | |
| run: | | |
| git clone https://github.com/leanprover/lean4checker | |
| cd lean4checker | |
| # Read lean-toolchain file and checkout appropriate branch | |
| TOOLCHAIN=$(cat ../lean-toolchain) | |
| printf '%s\n' "${TOOLCHAIN}" | |
| if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v ]]; then | |
| VERSION=${TOOLCHAIN#leanprover/lean4:} | |
| git checkout "$VERSION" | |
| elif [[ "$TOOLCHAIN" =~ ^leanprover/lean4:nightly-[0-9]{4}-[0-9]{2}-[0-9]{2}$ ]]; then | |
| # Extract the date part from the toolchain string | |
| DATE=${TOOLCHAIN#leanprover/lean4:} | |
| # Try to checkout nightly-testing-YYYY-MM-DD, fallback to nightly-testing | |
| git checkout "nightly-testing-${DATE}" 2>/dev/null || git checkout nightly-testing | |
| else | |
| git checkout master | |
| fi | |
| # Now that the git hash is embedded in each olean, | |
| # we need to compile lean4checker on the same toolchain | |
| cp ../lean-toolchain . | |
| lake build | |
| ./test.sh | |
| cd .. | |
| # After https://github.com/leanprover/lean4checker/pull/26 | |
| # lean4checker by default only runs on the current project | |
| # so we explicitly check Batteries as well here. | |
| lake env lean4checker/.lake/build/bin/lean4checker Batteries Mathlib | |
| - name: Run mathlib_test_executable | |
| id: mathlib-test | |
| continue-on-error: true | |
| run: | | |
| lake exe mathlib_test_executable | |
| - name: Post success message for lean4checker on Zulip | |
| if: steps.lean4checker.outcome == 'success' | |
| uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2 | |
| with: | |
| api-key: ${{ secrets.ZULIP_API_KEY }} | |
| email: 'github-mathlib4-bot@leanprover.zulipchat.com' | |
| organization-url: 'https://leanprover.zulipchat.com' | |
| to: 'nightly-testing' | |
| type: 'stream' | |
| topic: 'lean4checker' | |
| content: | | |
| ✅ lean4checker [succeeded](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }}) | |
| - name: Post success message for mathlib_test_executable on Zulip | |
| if: steps.mathlib-test.outcome == 'success' | |
| uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2 | |
| with: | |
| api-key: ${{ secrets.ZULIP_API_KEY }} | |
| email: 'github-mathlib4-bot@leanprover.zulipchat.com' | |
| organization-url: 'https://leanprover.zulipchat.com' | |
| to: 'nightly-testing' | |
| type: 'stream' | |
| topic: 'mathlib test executable' | |
| content: | | |
| ✅ mathlib_test_executable [succeeded](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }}) | |
| - name: Post failure message for lean4checker on Zulip | |
| if: steps.lean4checker.outcome == 'failure' | |
| uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2 | |
| with: | |
| api-key: ${{ secrets.ZULIP_API_KEY }} | |
| email: 'github-mathlib4-bot@leanprover.zulipchat.com' | |
| organization-url: 'https://leanprover.zulipchat.com' | |
| to: 'nightly-testing' | |
| type: 'stream' | |
| topic: 'lean4checker failure' | |
| content: | | |
| ❌ lean4checker [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }}) | |
| continue-on-error: true | |
| - name: Post failure message for mathlib_test_executable on Zulip | |
| if: steps.mathlib-test.outcome == 'failure' | |
| uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2 | |
| with: | |
| api-key: ${{ secrets.ZULIP_API_KEY }} | |
| email: 'github-mathlib4-bot@leanprover.zulipchat.com' | |
| organization-url: 'https://leanprover.zulipchat.com' | |
| to: 'nightly-testing' | |
| type: 'stream' | |
| topic: 'mathlib test executable failure' | |
| content: | | |
| ❌ mathlib_test_executable [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }}) | |
| continue-on-error: true |