Daily CI Workflow #304
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-leanchecker: | |
| runs-on: ubuntu-latest | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| strategy: | |
| fail-fast: false | |
| 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@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.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@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.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@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: true | |
| reinstall-transient-toolchain: true | |
| - name: Check environments using leanchecker # make sure this name is consistent with "Get job status and URLs" in the notify job | |
| id: leanchecker | |
| run: | | |
| # `--fresh` is safe and in fact currently faster for projects with many modules | |
| lake env leanchecker --fresh Mathlib | |
| lake env leanchecker --fresh Batteries | |
| notify-leanchecker: | |
| runs-on: ubuntu-latest | |
| needs: check-leanchecker | |
| if: github.repository == 'leanprover-community/mathlib4' && always() | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| branch_type: [master, nightly] | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | |
| - name: Get job status and URLs | |
| id: get-status | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| run: | | |
| JOB_NAME="check-leanchecker (${{ matrix.branch_type }})" | |
| # Get URL and conclusion for the specific job | |
| JOB_DATA=$(gh run view ${{ github.run_id }} --json jobs --jq \ | |
| ".jobs[] | select(.name == \"$JOB_NAME\")") | |
| LEANCHECKER_URL=$(echo "$JOB_DATA" | jq -r \ | |
| '(.url + (.steps[] | select(.name == "Check environments using leanchecker") | |
| | "#step:\(.number):1"))') | |
| JOB_CONCLUSION=$(echo "$JOB_DATA" | jq -r '.conclusion') | |
| echo "leanchecker_url=${LEANCHECKER_URL}" | tee -a "$GITHUB_OUTPUT" | |
| echo "job_conclusion=${JOB_CONCLUSION}" | tee -a "$GITHUB_OUTPUT" | |
| - name: Fetch latest tags (if nightly) | |
| if: matrix.branch_type == 'nightly' | |
| run: | | |
| 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}" | tee -a "$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 | |
| - name: Post success message for leanchecker on Zulip | |
| if: steps.get-status.outputs.job_conclusion == '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: 'leanchecker' | |
| content: | | |
| ✅ leanchecker [succeeded](${{ steps.get-status.outputs.leanchecker_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }}) | |
| - name: Post failure / cancelled message for leanchecker on Zulip | |
| if: steps.get-status.outputs.job_conclusion != '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: 'leanchecker failure' | |
| content: | | |
| ❌ leanchecker [${{ steps.get-status.outputs.job_conclusion }}](${{ steps.get-status.outputs.leanchecker_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }}) | |
| check-mathlib_test_executable: | |
| runs-on: ubuntu-latest | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| strategy: | |
| fail-fast: false | |
| 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@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.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@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.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@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: true | |
| reinstall-transient-toolchain: true | |
| - name: Run mathlib_test_executable # make sure this name is consistent with "Get job status and URLs" in the notify job | |
| id: mathlib-test | |
| run: | | |
| lake exe mathlib_test_executable | |
| notify-mathlib_test_executable: | |
| runs-on: ubuntu-latest | |
| needs: check-mathlib_test_executable | |
| if: github.repository == 'leanprover-community/mathlib4' && always() | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| branch_type: [master, nightly] | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | |
| - name: Get job status and URLs | |
| id: get-status | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| run: | | |
| JOB_NAME="check-mathlib_test_executable (${{ matrix.branch_type }})" | |
| # Get URL and conclusion for the specific job | |
| JOB_DATA=$(gh run view ${{ github.run_id }} --json jobs --jq \ | |
| ".jobs[] | select(.name == \"$JOB_NAME\")") | |
| MATHLIB_TEST_EXECUTABLE_URL=$(echo "$JOB_DATA" | jq -r \ | |
| '(.url + (.steps[] | select(.name == "Run mathlib_test_executable") | |
| | "#step:\(.number):1"))') | |
| JOB_CONCLUSION=$(echo "$JOB_DATA" | jq -r '.conclusion') | |
| echo "mathlib_test_executable_url=${MATHLIB_TEST_EXECUTABLE_URL}" | tee -a "$GITHUB_OUTPUT" | |
| echo "job_conclusion=${JOB_CONCLUSION}" | tee -a "$GITHUB_OUTPUT" | |
| - name: Fetch latest tags (if nightly) | |
| if: matrix.branch_type == 'nightly' | |
| run: | | |
| 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}" | tee -a "$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 | |
| - name: Post success message for mathlib_test_executable on Zulip | |
| if: steps.get-status.outputs.job_conclusion == '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.get-status.outputs.mathlib_test_executable_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }}) | |
| - name: Post failure / cancelled message for mathlib_test_executable on Zulip | |
| if: steps.get-status.outputs.job_conclusion != '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 failure' | |
| content: | | |
| ❌ mathlib_test_executable [${{ steps.get-status.outputs.job_conclusion }}](${{ steps.get-status.outputs.mathlib_test_executable_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }}) | |
| check-nanoda: | |
| runs-on: ubuntu-latest | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| strategy: | |
| fail-fast: false | |
| 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@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.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@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.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@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: true | |
| reinstall-transient-toolchain: true | |
| - name: Install Rust | |
| uses: dtolnay/rust-toolchain@631a55b12751854ce901bb631d5902ceb48146f7 # stable | |
| - name: Check Mathlib using nanoda # make sure this name is consistent with "Get job status and URLs" in the notify job | |
| id: nanoda | |
| run: | | |
| # Clone and build lean4export | |
| # TODO: Once https://github.com/leanprover/lean4export/pull/11 is merged, | |
| # switch to leanprover/lean4export and remove the `git checkout` line below. | |
| git clone https://github.com/kim-em/lean4export | |
| cd lean4export | |
| git checkout fix-nondep-normalization | |
| # Match toolchain to mathlib | |
| cp ../lean-toolchain . | |
| lake build | |
| cd .. | |
| # Clone and build nanoda_lib | |
| git clone https://github.com/ammkrn/nanoda_lib | |
| cd nanoda_lib | |
| git checkout debug | |
| cargo build --release | |
| cd .. | |
| # Export Mathlib | |
| lake env lean4export/.lake/build/bin/lean4export Mathlib > mathlib_export.txt | |
| # Create config | |
| cat > nanoda_config.json << 'EOF' | |
| { | |
| "export_file_path": "mathlib_export.txt", | |
| "permitted_axioms": [ | |
| "propext", | |
| "Classical.choice", | |
| "Quot.sound", | |
| "Lean.trustCompiler" | |
| ], | |
| "unpermitted_axiom_hard_error": false, | |
| "nat_extension": true, | |
| "string_extension": true, | |
| "print_success_message": true | |
| } | |
| EOF | |
| # Run nanoda | |
| nanoda_lib/target/release/nanoda_bin nanoda_config.json | |
| notify-nanoda: | |
| runs-on: ubuntu-latest | |
| needs: check-nanoda | |
| if: github.repository == 'leanprover-community/mathlib4' && always() | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| branch_type: [master, nightly] | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | |
| - name: Get job status and URLs | |
| id: get-status | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| run: | | |
| JOB_NAME="check-nanoda (${{ matrix.branch_type }})" | |
| # Get URL and conclusion for the specific job | |
| JOB_DATA=$(gh run view ${{ github.run_id }} --json jobs --jq \ | |
| ".jobs[] | select(.name == \"$JOB_NAME\")") | |
| NANODA_URL=$(echo "$JOB_DATA" | jq -r \ | |
| '(.url + (.steps[] | select(.name == "Check Mathlib using nanoda") | |
| | "#step:\(.number):1"))') | |
| JOB_CONCLUSION=$(echo "$JOB_DATA" | jq -r '.conclusion') | |
| echo "nanoda_url=${NANODA_URL}" | tee -a "$GITHUB_OUTPUT" | |
| echo "job_conclusion=${JOB_CONCLUSION}" | tee -a "$GITHUB_OUTPUT" | |
| - name: Fetch latest tags (if nightly) | |
| if: matrix.branch_type == 'nightly' | |
| run: | | |
| 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}" | tee -a "$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 | |
| - name: Post success message for nanoda on Zulip | |
| if: steps.get-status.outputs.job_conclusion == '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: 'nanoda' | |
| content: | | |
| ✅ nanoda [succeeded](${{ steps.get-status.outputs.nanoda_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }}) | |
| - name: Post failure / cancelled message for nanoda on Zulip | |
| if: steps.get-status.outputs.job_conclusion != '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: 'nanoda failure' | |
| content: | | |
| ❌ nanoda [${{ steps.get-status.outputs.job_conclusion }}](${{ steps.get-status.outputs.nanoda_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }}) |