[Merged by Bors] - feat: add lake exe shake to CI

[digama0]

• depends on: [Merged by Bors] - chore: reduce imports #9830
• depends on: [Merged by Bors] - fix: shake bug, improve noshake.json generation #9772
• depends on: [Merged by Bors] - feat(Shake): output clarifications #9996

This checks files for unused imports. The output here is piped through gh-problem-matcher-wrap so that it will show up as annotations.

---

[semorrison]

I think we need more straightforwardly human readable output. e.g.

./././Mathlib/GroupTheory/Subgroup/ZPowers.lean:
  remove #[Mathlib.Algebra.GroupPower.Lemmas]
  fix Mathlib.Algebra.GroupPower.Lemmas: #[Mathlib.Analysis.SpecificLimits.Basic, Mathlib.Data.Complex.Exponential]

should become:

In the file Mathlib/GroupTheory/Subgroup/ZPowers.lean, we can remove:
```
import Mathlib.Algebra.GroupPower.Lemmas
```
after which we'll add that import back into the following files:
* Mathlib/Analysis/SpecificLimits/Basic.lean
* Mathlib/Data/Complex/Exponential.lean

[digama0]

I was hoping people would be using the github annotations, which are a bit more user friendly. The CLI output is more optimized for batch usage, where that kind of verbosity is a bit overwhelming if there are 30-100 of them. You can also just ignore the CLI output entirely and use lake exe shake --fix > /dev/null || git diff HEAD instead.

[urkud]

You can also just ignore the CLI output entirely and use lake exe shake --fix > /dev/null || git diff HEAD instead.

Can we turn this into clickable suggestions like we have for some style linters? Or it will fail because github won't accept suggestions to the lines that aren't touched by the PR?

[Vierkantor]

You can also just ignore the CLI output entirely and use lake exe shake --fix > /dev/null || git diff HEAD instead.

That's definitely not something a user newly encountering shake is going to know, or teachable to the average mathematician. Before we encourage everyone to use this tool, we should make sure it doesn't raise further questions. Especially the output of --fix appearing to be in the imperative mood and the meaning of "fix" in the output looks confusing, and should be easy to fix. I've opened #9996 with my proposal.

[urkud]

What does --gh-style do and where can I see the output it generates?

[digama0]

--gh-style produces additional output from shake (which you can see in the build logs), these are lines that look like file:line:col: warning: ... and shake does not normally produce them. The purpose is that this particular error format is understood by gh-problem-matcher-wrap, and it uses them to produce annotations that appear on the PR itself next to other lint warnings. Just look for the comments about unused import (use `lake exe shake --fix` to fix this... in https://github.com/leanprover-community/mathlib4/pull/9751/files, and the annotations also appear on the build summary page and are highlighted in yellow in the build log itself.

[semorrison]

I was hoping people would be using the github annotations, which are a bit more user friendly. The CLI output is more optimized for batch usage, where that kind of verbosity is a bit overwhelming if there are 30-100 of them. You can also just ignore the CLI output entirely and use lake exe shake --fix > /dev/null || git diff HEAD instead.

I think we either need to have human readable output, or entirely suppress the non human readable output from the CI logs when you click on a red X! How is a new contributor meant to know they are meant to ignore this output?

[digama0]

Does #9996 address your concerns? (The output is of course human readable and useful, so I definitely would not want to suppress it, it's just not exactly intended to be a tutorial about itself. Most other CI logs are at a similar level of verbosity.)

[digama0]

This disables batching for this PR, so that it doesn't race with other PRs:

bors single on

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - chore: reduce imports #9830
• [Merged by Bors] - fix: shake bug, improve noshake.json generation #9772
• [Merged by Bors] - feat(Shake): output clarifications #9996
  By Dependent Issues (🤖). Happy coding!

[jcommelin]

Thanks 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

[mathlib-bors]

✌️ digama0 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[digama0]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style