feat: the unusedVariableCommand linter

[adomani]

This is still work-in-progress, but also help-wanted!

The linter reliably flags unused variables: so far, only examples fool it (and that is simply because I did not implement a fix, as there are very few variables that are only used in examples in mathlib).

The work-in-progress part refers to the fact that the linter uses an IO.Ref to keep track of variables and this does not work well with editing the file. The linter works on a fresh parse of a file, but becomes out-of-sync with every edit.

The help-wanted is to ask for help to make mathlib compliant with the linter, by checking out this branch and PR-ing a few variable removals!

Zulip discussion

---

Known issues:

• automatic namespacing and nonrec may cause difficulty when the newly introduced declaration is preferred in the term, rather than the original one (see examples here

  code -r -g  ././././Mathlib/Analysis/SpecialFunctions/Arsinh.lean:183
  code -r -g  ././././Mathlib/Probability/Independence/Basic.lean:368

  where, for instance, ContinuousOn.arsinh is used internally instead of Real.arsinh).

• mutual declarations confuse the linter

  code -r -g  ././././Mathlib/SetTheory/Lists.lean:313

• code -r -g Mathlib/CategoryTheory/EffectiveEpi/Comp.lean:133:29

• universe annotations confuse the linter:

  code -r -g  ././././Mathlib/Topology/Category/CompactlyGenerated.lean:53
  code -r -g  ././././Mathlib/AlgebraicTopology/CechNerve.lean:46

• inductives confusing the linter

  code -r -g  ././././Mathlib/Deprecated/Subgroup.lean:389
  code -r -g  ././././Mathlib/FieldTheory/PerfectClosure.lean:55

• defs confusing the linter

  code -r -g  ././././Mathlib/Data/MLList/BestFirst.lean:104

• special typeclass assumptions

  code -r -g  ././././Mathlib/RingTheory/WittVector/Truncated.lean:273
  code -r -g  ././././Mathlib/Topology/Category/Profinite/Product.lean:79
  

• not sure what is going on here:

  code -r -g  ././././Mathlib/RingTheory/WittVector/IsPoly.lean:95
  code -r -g  ././././Mathlib/Probability/Independence/Basic.lean:368
  code -r -g  ././././Mathlib/Analysis/Calculus/FDeriv/Star.lean:30

[grunweg]

Adding this for reference: I presume the new async linting also confuses the linter, so would have to be turned off as well, right? See #20755 for reference.