Commit 2024-04-18 05:39 278260ff

feat: shake --explain (#11982)

• Depends on: #11981 This adds a --explain flag to shake which will say, for each module in which it reports unnecessary imports, why all of the imports it is suggesting (as well as all the imports it does not recommend to remove) are required, in the form:

$ lake exe shake --explain
...
./././Mathlib/Tactic/Eqns.lean:
  remove #[Std.CodeAction.Attr, Std.Tactic.Lint.Basic]
  add #[Lean.Elab.InfoTree.Main, Lean.Elab.Exception]
  note: Mathlib.Tactic.Eqns requires Lean.Meta.Eqns
    because initFn✝ refers to Lean.Meta.EqnsExtState.map
  note: Mathlib.Tactic.Eqns requires Std.Lean.NameMapAttribute
    because eqnsAttribute refers to Lean.NameMapExtension
  note: Mathlib.Tactic.Eqns requires Lean.Elab.InfoTree.Main
    because initFn✝ refers to Lean.Elab.resolveGlobalConstNoOverloadWithInfo
  note: Mathlib.Tactic.Eqns requires Lean.Elab.Exception
    because initFn✝ refers to Lean.Elab.throwUnsupportedSyntax