Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
wants to merge 25 commits into from

Conversation

adomani
Copy link
Collaborator

@adomani adomani commented Apr 16, 2024

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.


Open in Gitpod

@adomani
Copy link
Collaborator Author

adomani commented Apr 17, 2024

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
Copy link
Collaborator Author

adomani commented Apr 17, 2024

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
Copy link
Member

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
Copy link
Collaborator Author

adomani commented Apr 17, 2024

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?

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 7, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 9, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 15, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 20, 2024
Copy link

github-actions bot commented Jun 17, 2024

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.

Copy link
Collaborator

@joneugster joneugster left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Mathlib/Tactic/Linter/HaveLetLinter.lean Outdated Show resolved Hide resolved
Mathlib/Tactic/Linter/HaveLetLinter.lean Outdated Show resolved Hide resolved
test/HaveLetLinter.lean Outdated Show resolved Hide resolved
test/HaveLetLinter.lean Outdated Show resolved Hide resolved
have _b : 0 = 0 := rfl
have _oh : Nat := 0
have _b : Nat := 2
tauto
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator Author

@adomani adomani Aug 6, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

@joneugster joneugster added the awaiting-author A reviewer has asked the author a question or requested changes label Aug 1, 2024
@joneugster joneugster self-assigned this Aug 1, 2024
Copy link
Collaborator Author

@adomani adomani left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Mathlib/Tactic/Linter/HaveLetLinter.lean Outdated Show resolved Hide resolved
Mathlib/Tactic/Linter/HaveLetLinter.lean Outdated Show resolved Hide resolved
test/HaveLetLinter.lean Outdated Show resolved Hide resolved
have _b : 0 = 0 := rfl
have _oh : Nat := 0
have _b : Nat := 2
tauto
Copy link
Collaborator Author

@adomani adomani Aug 6, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

test/HaveLetLinter.lean Outdated Show resolved Hide resolved
…community/mathlib4 into adomani/have_let_linter_only
@adomani adomani removed the awaiting-author A reviewer has asked the author a question or requested changes label Aug 6, 2024
@joneugster
Copy link
Collaborator

joneugster commented Aug 7, 2024

maintainer merge

Copy link

github-actions bot commented Aug 7, 2024

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

/-- The `have` vs `let` linter emits a warning on `have`s introducing a hypothesis whose
Type is not `Prop`.
There are three settings:
* `0` -- inactive;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

@adomani adomani Aug 7, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@mattrobball
Copy link
Collaborator

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 7, 2024
mathlib-bors bot pushed a commit that referenced this pull request Aug 7, 2024
The main PR for the `have` vs `let` linter.

The `have` vs `let` linter emits a warning on `have`s 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.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Aug 7, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: have/let linter [Merged by Bors] - feat: have/let linter Aug 7, 2024
@mathlib-bors mathlib-bors bot closed this Aug 7, 2024
@mathlib-bors mathlib-bors bot deleted the adomani/have_let_linter_only branch August 7, 2024 13:48
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
The main PR for the `have` vs `let` linter.

The `have` vs `let` linter emits a warning on `have`s 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.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
The main PR for the `have` vs `let` linter.

The `have` vs `let` linter emits a warning on `have`s 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.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
The main PR for the `have` vs `let` linter.

The `have` vs `let` linter emits a warning on `have`s 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
maintainer-merge ready-to-merge This PR has been sent to bors. t-linter Linter
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants