Daily CI Workflow #130
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. | |
| 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' | |
| 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: | | |
| git fetch --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: | |
| 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: 'mathlib reviewers' | |
| 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: 'mathlib reviewers' | |
| 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: 'mathlib reviewers' | |
| 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: 'mathlib reviewers' | |
| 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 |