Late importers report #2
This file contains 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 | |
| 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 | |
| - name: install elan | |
| run: | | |
| set -o pipefail | |
| curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz | |
| ./elan-init -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" | |
| - uses: actions/checkout@v4 | |
| - name: If using a lean-pr-release toolchain, uninstall | |
| run: | | |
| if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then | |
| printf 'Uninstalling transient toolchain %s\n' "$(cat lean-toolchain)" | |
| elan toolchain uninstall "$(cat lean-toolchain)" | |
| fi | |
| - name: print lean and lake versions | |
| run: | | |
| lean --version | |
| lake --version | |
| - name: add minImports linter option | |
| run: | | |
| # set `linter.minImports option` to true in `lakefile` | |
| sed -i -- '/^ -- '\`'latest_import.yml'\`' uses this comment/{s=^= ⟨`linter.minImports, true⟩,\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: liskin/gh-problem-matcher-wrap@v3 | |
| with: | |
| linters: gcc | |
| 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@v1 | |
| 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 }} |