[Merged by Bors] - feat: have/let linter

[adomani]

The main PR for the have vs let linter.

The have vs let linter emits a warning on haves introducing a hypothesis whose
Type is not Prop.
There are three settings:

• 0 -- inactive;
• 1 -- active only on noisy declarations;
• 2 or more -- always active.
  The default value is 1.

The linter lints mathlib, but, by default, it is silent on complete proofs.

#12157 is an experiment showing what changes the linter would suggest on mathlib.

---

[adomani]

As a test, I ran the linter with the "new" monad on a fresh copy of mathlib: I wanted to make sure that it picked up the same issues that the previous version of the linter noticed.

The result is an improvement: I think that they flag essentially the same issues and the new monad pretty-prints better. However, there is an overflow that I cannot debug. You can see its effects in this failed linting step.

The two places that I identified are a run_cmd in Mathlib/Data/UInt.lean and a local notation3 in Mathlib/Algebra/Lie/Weights/Basic.lean.

[adomani]

Looking at the places where I had to unset the linter, I am guessing that this is just a matter of a slowdown: notation3, theorem, run_command` all appear among the list of unlinted commands.

diff --git a/Mathlib/Algebra/Lie/Weights/Basic.lean b/Mathlib/Algebra/Lie/Weights/Basic.lean
index 7742e87568..3ea8cbfefe 100644
--- a/Mathlib/Algebra/Lie/Weights/Basic.lean
+++ b/Mathlib/Algebra/Lie/Weights/Basic.lean
@@ -56,8 +56,10 @@ open scoped BigOperators TensorProduct
 
 section notation_weightSpaceOf
 
+set_option linter.haveLet false
 /-- Until we define `LieModule.weightSpaceOf`, it is useful to have some notation as follows: -/
 local notation3 "𝕎("M", " χ", " x")" => (toEndomorphism R L M x).maximalGeneralizedEigenspace χ
+set_option linter.haveLet true
 
 /-- See also `bourbaki1975b` Chapter VII §1.1, Proposition 2 (ii). -/
 protected theorem weight_vector_multiplication (M₁ M₂ M₃ : Type*)
diff --git a/Mathlib/AlgebraicGeometry/Restrict.lean b/Mathlib/AlgebraicGeometry/Restrict.lean
index 11aecab1ec..a209fdc975 100644
--- a/Mathlib/AlgebraicGeometry/Restrict.lean
+++ b/Mathlib/AlgebraicGeometry/Restrict.lean
@@ -35,10 +35,12 @@ section
 
 variable (X : Scheme)
 
+set_option linter.haveLet false in
 /-- `f ⁻¹ᵁ U` is notation for `(Opens.map f.1.base).obj U`,
   the preimage of an open set `U` under `f`. -/
 notation3:90 f:91 "⁻¹ᵁ " U:90 => (Opens.map (f : LocallyRingedSpace.Hom _ _).val.base).obj U
 
+set_option linter.haveLet false in
 /-- `X ∣_ᵤ U` is notation for `X.restrict U.openEmbedding`, the restriction of `X` to an open set
   `U` of `X`. -/
 notation3:60 X:60 " ∣_ᵤ " U:61 => Scheme.restrict X (U : Opens X).openEmbedding
diff --git a/Mathlib/MeasureTheory/Covering/Vitali.lean b/Mathlib/MeasureTheory/Covering/Vitali.lean
index 536f1a2dbd..e976f9c92f 100644
--- a/Mathlib/MeasureTheory/Covering/Vitali.lean
+++ b/Mathlib/MeasureTheory/Covering/Vitali.lean
@@ -192,6 +192,7 @@ theorem exists_disjoint_subfamily_covering_enlargment_closedBall [MetricSpace α
     exact ⟨c, cu, by simp only [closedBall_eq_empty.2 h'a, empty_subset]⟩
 #align vitali.exists_disjoint_subfamily_covering_enlargment_closed_ball Vitali.exists_disjoint_subfamily_covering_enlargment_closedBall
 
+set_option linter.haveLet false in
 /-- The measurable Vitali covering theorem. Assume one is given a family `t` of closed sets with
 nonempty interior, such that each `a ∈ t` is included in a ball `B (x, r)` and covers a definite
 proportion of the ball `B (x, 3 r)` for a given measure `μ` (think of the situation where `μ` is ... -/
diff --git a/Mathlib/RingTheory/Kaehler.lean b/Mathlib/RingTheory/Kaehler.lean
index 1796e93347..052ed3af6a 100644
--- a/Mathlib/RingTheory/Kaehler.lean
+++ b/Mathlib/RingTheory/Kaehler.lean
@@ -481,10 +481,12 @@ noncomputable def KaehlerDifferential.kerTotal : Submodule S (S →₀ S) :=
       Set.range fun x : R => single (algebraMap R S x) 1)
 #align kaehler_differential.ker_total KaehlerDifferential.kerTotal
 
+set_option linter.haveLet false
 unsuppress_compilation in
 -- Porting note: was `local notation x "𝖣" y => (KaehlerDifferential.kerTotal R S).mkQ (single y x)`
 -- but not having `DFunLike.coe` leads to `kerTotal_mkQ_single_smul` failing.
 local notation3 x "𝖣" y => DFunLike.coe (KaehlerDifferential.kerTotal R S).mkQ (single y x)
+set_option linter.haveLet true
 
 theorem KaehlerDifferential.kerTotal_mkQ_single_add (x y z) : (z𝖣x + y) = (z𝖣x) + z𝖣y := by
   rw [← map_add, eq_comm, ← sub_eq_zero, ← map_sub (Submodule.mkQ (kerTotal R S)),
diff --git a/Mathlib/SetTheory/Game/Basic.lean b/Mathlib/SetTheory/Game/Basic.lean
index ec92a0d3dc..6f3259b0d9 100644
--- a/Mathlib/SetTheory/Game/Basic.lean
+++ b/Mathlib/SetTheory/Game/Basic.lean
@@ -519,6 +519,7 @@ theorem quot_mul_neg (x y : PGame) : ⟦x * -y⟧ = (-⟦x * y⟧ : Game) :=
   Quot.sound (mulNegRelabelling x y).equiv
 #align pgame.quot_mul_neg SetTheory.PGame.quot_mul_neg
 
+set_option linter.haveLet false in
 @[simp]
 theorem quot_left_distrib (x y z : PGame) : (⟦x * (y + z)⟧ : Game) = ⟦x * y⟧ + ⟦x * z⟧ :=
   match x, y, z with
@@ -689,6 +690,7 @@ theorem one_mul_equiv (x : PGame) : 1 * x ≈ x :=
   Quotient.exact <| quot_one_mul x
 #align pgame.one_mul_equiv SetTheory.PGame.one_mul_equiv
 
+set_option linter.haveLet false in
 theorem quot_mul_assoc (x y z : PGame) : (⟦x * y * z⟧ : Game) = ⟦x * (y * z)⟧ :=
   match x, y, z with
   | mk xl xr xL xR, mk yl yr yL yR, mk zl zr zL zR => by

[eric-wieser]

I think the issue is that InfoTree.foldInfoM is a hack, and the right way to do it is to modify InfoTree.foldInfo to be monadic.

[adomani]

Eric, fair enough! Do you still think that this version is better or should I revert it to the one with the handcrafted MetaM state?

[github-actions]

PR summary 94894a93a9

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Linter	12	14	+2 (+16.67%)
Mathlib.Tactic	2144	2146	+2 (+0.09%)

Import changes for all files

Files	Import difference
There are 4048 files with changed transitive imports: this is too many to display!

---

Declarations diff

+ InfoTree.foldInfoM
+ areProp_toFormat
+ ghi
+ haveLetLinter
+ isHave?
+ nonPropHaves

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.

[joneugster]

Looks quite clean to me! However, I did not quite figure out how level 1 is supposed to work, see comments below.

I also have some remaining thoughts on whether it's actually useful to enforce this linter in mathlib, but if I understand it correctly, the current PR does not and only shows the warnings while working on a statement, which seems nice.

[joneugster]

Is there a way to guard an unfinished proof, like this one without tauto? If I understand your motivation for level 1 correctly, it's also to trigger on unfinished proofs, isn't it?

I expected that if I delete the #guard_msgs here and then delete tauto that the linter warnings would pop up. Did I understand this wrongly?

[adomani]

The linter emits a warning if a declaration simultaneously does not have errors and yet emits messages. Simply removing tauto leaves an unsolved goals error, so the linter shuts up. If, instead, you replace tauto with sorry, then the linter will tell you that you should use let/have.

I could make the linter chatty also in the presence of errors, but I think that on an erroring declaration, the linter will yield dubious reports and would be simply extra noise.

[joneugster]

ok. I somehow expect that an "unsolved goals" error behaves very similar to a "declaration uses sorry" warning in as many aspects as possible but I see that's not as easy with how messages are reported.

Looks good to me as is.

[adomani]

@joneugster, thank you very much for the review! I acted on all your comments and they were all great!

I also left some clarifications in the various discussions.

[adomani]

The linter emits a warning if a declaration simultaneously does not have errors and yet emits messages. Simply removing tauto leaves an unsolved goals error, so the linter shuts up. If, instead, you replace tauto with sorry, then the linter will tell you that you should use let/have.

I could make the linter chatty also in the presence of errors, but I think that on an erroring declaration, the linter will yield dubious reports and would be simply extra noise.

[joneugster]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by joneugster.

[mattrobball]

Is this just a limitation of the types that can be passed to a built in option?

[adomani]

Essentially yes. A Lean.Option is

/-- A strongly-typed reference to an option. -/
protected structure Option (α : Type) where
  name     : Name
  defValue : α
  deriving Inhabited

with an arbitrary type α. However, the Option is then stored in a KVMap, whose Values need to be in a

/-- Value stored in a key-value map. -/
inductive DataValue where
  | ofString (v : String)
  | ofBool   (v : Bool)
  | ofName   (v : Name)
  | ofNat    (v : Nat)
  | ofInt    (v : Int)
  | ofSyntax (v : Syntax)
  deriving Inhabited, BEq, Repr

I felt that remembering 0, 1 and 2 was easier than remembering three strings for the settings.

[mattrobball]

I guess it is discoverable but it would nice to have custom syntax for verbosity of things.

[mattrobball]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style