latest_import.yml

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 }}