Late importers report #7
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: Late importers report | |
| on: | |
| schedule: | |
| - cron: '0 4 * * 1' # Run at 04:00 UTC every Monday | |
| workflow_dispatch: | |
| env: | |
| TOP_MODULE: Mathlib | |
| jobs: | |
| late-importers: | |
| name: Build | |
| runs-on: pr | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| 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@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - 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: add minImports linter option | |
| run: | | |
| # we disable checking for backticks inside single quotes with the next line | |
| # shellcheck disable=SC2016 | |
| # set `linter.minImports option` to true and `Elab.async` to false in `lakefile` | |
| sed -i -- '/^ -- '\`'latest_import.yml'\`' uses this comment/{s=^= ⟨`linter.minImports, true⟩,\n ⟨`Elab.async, false⟩,\n=}' lakefile.lean | |
| # import the `minImports` linter in `Mathlib.Init` | |
| sed -i -z 's=^=import Mathlib.Tactic.Linter.MinImports\n=' Mathlib/Init.lean | |
| # remove the `Mathlib.Init` import from the `minImports` command to avoid a loop | |
| sed -i '/import Mathlib.Init/d' Mathlib/Tactic/MinImports.lean | |
| # stage the changes in git so that `git diff` can confirm what changed | |
| git add -u | |
| git diff HEAD #lakefile.lean Mathlib/Init.lean Mathlib/Tactic/MinImports.lean | |
| printf $'\n\nRunning a test %slake build` to verify, for instance, the absence of import loops\n' $'`' | |
| lake build Mathlib.Init | |
| - name: build mathlib | |
| id: build | |
| uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23 | |
| with: | |
| linters: lean | |
| run: | | |
| lake build | |
| - name: Full report | |
| run: | | |
| ./scripts/late_importers.sh Mathlib 0 0 "${{ github.run_id }}" | |
| - name: Zulip report | |
| id: late_importers | |
| run: | | |
| jobID="${{ github.run_id }}" | |
| printf $'summary<<EOF\n%s\nEOF' "$(./scripts/late_importers.sh Mathlib 15 10 "${jobID}")" | | |
| tee "$GITHUB_OUTPUT" | |
| - 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: 'mathlib4' | |
| type: 'stream' | |
| topic: Late importers report | |
| content: ${{ steps.late_importers.outputs.summary }} |