feat: have vs let linter
#12157
feat: have vs let linter
#12157
Conversation
|
I'm slightly concerned that the
|
|
Yaël, with respect to benchmarking, I was definitely planning on doing that, once I finish up the missing replacements. Running the linter only on incomplete proofs: this is something that can probably be done. My first approach would probably be to run the linter only if the command emits a warning. I would probably still not run the linter with errors since then the type information is probably unreliable. |
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
| -- and the last declaration introduced: the one that `have` created | ||
| let ld := (lc.lastDecl.getD default).type | ||
| -- now, we get the `MetaM` state up and running to find the type of `ld` | ||
| let res ← liftCoreM do MetaM.run (ctx := { lctx := lc }) (s := { mctx := mctx }) <| do |
There was a problem hiding this comment.
Are you looking for Lean.Elab.ContextInfo.runMetaM here?
There was a problem hiding this comment.
Possibly, although here the node is a TacticInfo, rather than a ContextInfo. Maybe this is an indication that I should re-organize which nodes of the infotree I visit...
There was a problem hiding this comment.
Discussed further in #12190
|
Is it possible to split this PR into:
Scrolling through 150 files to find the new meta code is pretty annoying, especially over a train internet connection... |
|
@eric-wieser, I opened #12190 that contains only the linter and the tests. I did not disable the linter, but I also did not import the file anywhere. |
|
Actually, I don't really like my previous comment anymore. What about this instead? The linter should send a warning on:
Note that the "Type-valued |
leanprover-community-mathlib4-bot
added
the
merge-conflict
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.
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.
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.
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.
#12190 seems to have become the main PR for this linter.
The
havevsletlinter flags uses ofhaveto introduce a hypothesis whose Type is notPropHere is a summary of the PR. Besides changes
have --> letthis is everything else.Mathlib/Analysis/Convolution.lean: two parallel simplified proofs.Mathlib/CategoryTheory/Limits/Final.lean: ahavethat could not be replaced bylet.Mathlib/Combinatorics/SimpleGraph/Connectivity.lean: vanishinghaveSufficesdue tohave --> let.Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean:have := ...; exact thisbecomingexact ....Mathlib/FieldTheory/Finite/GaloisField.lean: usingletmakes theunusedVariablelinter complain.Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean: unset linter sinceclear_valuecomplains.Mathlib/Tactic/NormNum/Inv.lean: unset linter sincegeneralizecomplains.What is the syntax in
Mathlib/CategoryTheory/Extensive.lean?benchat #12180, testing only the replacements, not the linter itself.