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

feat: have vs let linter #12157

Closed
wants to merge 17 commits into from
Closed

feat: have vs let linter #12157

wants to merge 17 commits into from

Conversation

adomani
Copy link
Collaborator

@adomani adomani commented Apr 15, 2024

#12190 seems to have become the main PR for this linter.

The have vs let linter flags uses of have to introduce a hypothesis whose Type is not Prop

Here is a summary of the PR. Besides changes have --> let this is everything else.

  • Mathlib/Analysis/Convolution.lean: two parallel simplified proofs.
  • Mathlib/CategoryTheory/Limits/Final.lean: a have that could not be replaced by let.
  • Mathlib/Combinatorics/SimpleGraph/Connectivity.lean: vanishing haveSuffices due to have --> let.
  • Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean: have := ...; exact this becoming exact ....
  • Mathlib/FieldTheory/Finite/GaloisField.lean: using let makes the unusedVariable linter complain.
  • Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean: unset linter since clear_value complains.
  • Mathlib/Tactic/NormNum/Inv.lean: unset linter since generalize complains.

What is the syntax in Mathlib/CategoryTheory/Extensive.lean?

bench at #12180, testing only the replacements, not the linter itself.


Open in Gitpod

@YaelDillies
Copy link
Collaborator

I'm slightly concerned that the haves you're turning into lets were declaring data that we didn't care about and that Lean now has the option of unfolding when we know it is unnecessary.

  1. Could you benchmark this PR once CI is green?
  2. Could the linter only run on definitions and incomplete proofs? If a proof is complete, we know for sure the haves can stay haves. In a definition however, a type-valued have is most certainly a mistake.

@adomani
Copy link
Collaborator Author

adomani commented Apr 16, 2024

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 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 Apr 16, 2024
This was referenced Apr 16, 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 Apr 16, 2024
-- 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
Copy link
Member

Choose a reason for hiding this comment

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

Are you looking for Lean.Elab.ContextInfo.runMetaM here?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

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

Copy link
Member

Choose a reason for hiding this comment

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

Discussed further in #12190

@eric-wieser
Copy link
Member

Is it possible to split this PR into:

  • Add the new linter, disabled-by-default
  • Enable the linter and fix all the occurences

Scrolling through 150 files to find the new meta code is pretty annoying, especially over a train internet connection...

@adomani
Copy link
Collaborator Author

adomani commented Apr 16, 2024

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

@YaelDillies
Copy link
Collaborator

YaelDillies commented Apr 16, 2024

Actually, I don't really like my previous comment anymore. What about this instead?

The linter should send a warning on:

  • a Prop-valued let
  • a Type-valued have in an erroring branch of a proof

Note that the "Type-valued have in a completed sorry-free def" that I was referring to before is actually not bad since it's defeq to its value once the def is completed.

@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 Apr 17, 2024
@adomani adomani marked this pull request as draft April 20, 2024 05:26
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.
@adomani adomani closed this Aug 7, 2024
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
merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-linter Linter
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants