Daily CI Workflow #80
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}$' | |
| permissions: | |
| contents: read | |
| actions: read | |
| jobs: | |
| check-lean4checker: | |
| runs-on: ubuntu-latest | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| strategy: | |
| matrix: | |
| branch_type: [master, nightly] | |
| steps: | |
| # Checkout repository, so that we can fetch tags to decide which branch we want. | |
| - name: Checkout branch or tag | |
| uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 | |
| # this step needs to be run here while we have `mathlib4` checked out, | |
| # or else `gh run view` will try to look for runs in `mathlib4-nightly-testing` | |
| - name: Get URLs | |
| id: urls | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| run: | | |
| # adapted from https://cmbuckley.co.uk/blog/2024/04/09/deep-links-to-github-actions-job-logs/ | |
| lean4checker_url=$(gh run view ${{ github.run_id }} --json jobs --jq ' | |
| .jobs[] | select(.name == "check-lean4checker (${{ matrix.branch_type }})") | |
| | (.url + (.steps[] | select(.name == "Check environments using lean4checker") | |
| | "#step:\(.number):1"))') | |
| echo "lean4checker_url=$lean4checker_url" | tee -a "$GITHUB_OUTPUT" | |
| mathlib_test_executable_url=$(gh run view ${{ github.run_id }} --json jobs --jq ' | |
| .jobs[] | select(.name == "check-lean4checker (${{ matrix.branch_type }})") | |
| | (.url + (.steps[] | select(.name == "Run mathlib_test_executable") | |
| | "#step:\(.number):1"))') | |
| echo "mathlib_test_executable_url=$mathlib_test_executable_url" | tee -a "$GITHUB_OUTPUT" | |
| - 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@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 | |
| with: | |
| repository: ${{ matrix.branch_type == 'nightly' && 'leanprover-community/mathlib4-nightly-testing' || github.repository }} | |
| ref: ${{ env.BRANCH_REF }} | |
| - name: Configure Lean | |
| uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: true | |
| reinstall-transient-toolchain: true | |
| - name: Check environments using lean4checker # make sure this name is consistent with "Get URLs" | |
| 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 # make sure this name is consistent with "Get URLs" | |
| 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](${{ steps.urls.outputs.lean4checker_url }}) 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](${{ steps.urls.outputs.mathlib_test_executable_url }}) 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](${{ steps.urls.outputs.lean4checker_url }}) 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](${{ steps.urls.outputs.mathlib_test_executable_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }}) | |
| continue-on-error: true |