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
  

• 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
  

[github-actions[bot]]

PR summary 18c7894c63

Import changes exceeding 2%

%	File
+7.41%	Mathlib.Init

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Init	27	29	+2 (+7.41%)
Mathlib.Algebra.Group.Idempotent	128	130	+2 (+1.56%)
Mathlib.Algebra.GroupWithZero.Idempotent	130	132	+2 (+1.54%)
Mathlib.Data.Finite.Defs	137	139	+2 (+1.46%)
Mathlib.Data.Int.Cast.Field	144	146	+2 (+1.39%)
Mathlib.Order.BoundedOrder.Basic	160	162	+2 (+1.25%)
Mathlib.Order.Monotone.Monovary	182	184	+2 (+1.10%)
Mathlib.Order.BoundedOrder.Monotone	184	186	+2 (+1.09%)
Mathlib.Order.BoundedOrder.Lattice	185	187	+2 (+1.08%)
Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous	2070	2072	+2 (+0.10%)
Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique	2310	2312	+2 (+0.09%)
Mathlib.NumberTheory.LSeries.PrimesInAP	2977	2979	+2 (+0.07%)

Import changes for all files

Files	Import difference
There are 6396 files with changed transitive imports taking up over 269024 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ D + X1 + X11 + XX + binders + cleanUpExplicitUniverses + exampleToDef + filter + filterMap + filterMapM + findBinders + getBracketedBinderIds + getExtendBinders + getForallStrings + getNamelessVars + getPropValue + getUsedVariableFromName + getUsedVariableNames + includedVariables + instance : Add C := ‹_› + instance : Add.{v} C := ‹_› + lemmaToThm + mkThm + mkThmCore + toFalse + unusedVariableCommandLinter + usedVarsRef.addDefDict + usedVarsRef.addDict + usedVarsRef.addUsedVarName + varsTracker + varsTracker.isEmpty ++++ X

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[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.

[leanprover-community-bot-assistant]

This pull request has conflicts, please merge master and resolve them.