nightly-testing regression report #81
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: nightly-testing regression report | |
| on: | |
| schedule: | |
| - cron: '37 4 * * *' # Run at 04:37 UTC every day (generated by fair dice roll) | |
| workflow_dispatch: | |
| env: | |
| TOP_MODULE: Mathlib | |
| jobs: | |
| grind-regressions: | |
| name: Build | |
| runs-on: pr | |
| if: github.repository == 'leanprover-community/mathlib4-nightly-testing' | |
| steps: | |
| - name: cleanup | |
| run: | | |
| find . -name . -o -prune -exec rm -rf -- {} + | |
| # 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 | |
| - uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1 | |
| with: | |
| ref: nightly-testing-green | |
| - name: Configure Lean | |
| uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| reinstall-transient-toolchain: true | |
| - name: add nightly regression linter option | |
| run: | | |
| # Reset contents of the lakefile, so we don't leave the wrong options enabled. | |
| git checkout HEAD -- lakefile.lean | |
| # we disable checking for backticks inside single quotes with the next line | |
| # shellcheck disable=SC2016 | |
| # Enable the linter | |
| sed -i -- '/^ -- '\`'latest_import.yml'\`' uses this comment/{s=^= ⟨`linter.nightlyRegressionSet, true⟩,\n=}' lakefile.lean | |
| # stage the changes in git so that `git diff` can confirm what changed | |
| git add -u | |
| git diff HEAD #lakefile.lean | |
| printf $'\n\nRunning a test %slake build` to verify, for instance, the absence of import loops\n' $'`' | |
| lake build Mathlib.Init | |
| - name: Add GitHub problem matcher wrapper | |
| uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23 | |
| with: | |
| action: add | |
| linters: lean | |
| - name: build mathlib | |
| id: build | |
| continue-on-error: true | |
| run: | | |
| # Use a temporary file to ensure we don't overflow max variable size. | |
| lean_outfile=$(mktemp) | |
| # Show the stdout in the GitHub build logs, while we process it from the file. | |
| (lake build || true) | tee "${lean_outfile}" | |
| # Process output for posting to Zulip | |
| SHA=${{ github.sha }} \ | |
| REPO=${{ github.repository }} \ | |
| RUN_ID=${{ github.run_id }} \ | |
| ./scripts/zulip_build_report.sh "${lean_outfile}" > "${GITHUB_OUTPUT}" | |
| - name: Remove GitHub problem matcher wrapper | |
| uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23 | |
| with: | |
| action: remove | |
| linters: lean | |
| - name: Post output to Zulip | |
| 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: nightly-testing regression log | |
| content: ${{ steps.build.outputs.zulip-message }} |