Running `mk_all` twice in CI?

Stream: mathlib4

[Kim Morrison]

@Damiano Testa, why do we have two separate steps running mk_all in CI?

      # We update `Mathlib.lean` as a convenience here,
      # but verify that this didn't change anything in the `check_imported` job.
      - name: update Mathlib.lean
        run: |
          lake exe mk_all --lib Mathlib

      - 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: update {Mathlib, Tactic, Counterexamples, Archive}.lean
        run: lake exe mk_all

[Ruben Van de Velde]

#13667

[Damiano Testa]

I do not know why there are two such steps, but I do remember preserving them, since I did not feel confident enough with CI to simply remove one.

I think that the Michael's PR linked by Ruben is good, and it could probably also remove the git diff step that follows the remaining lake exe mk_all step, since the exit code of mk_all is the number of updated/modified files, so it will fail when the "import all" files are not up to date.

I'll leave this comment on the PR as well.