feat: add the haveILetI linter, flagging haveI/letI in tactic proofs.#41562
feat: add the haveILetI linter, flagging haveI/letI in tactic proofs.#41562kbuzzard wants to merge 3 commits into
Conversation
…of propositions The tactics `haveI` and `letI` differ from `have` and `let` only in that they inline the given value into the term being constructed (in current core they are literally `have +zeta` and `let +zeta`, sharing a single elaborator). In a tactic proof of a proposition this difference is invisible by proof irrelevance, so `have`/`let` should be used instead. The linter walks the InfoTree and flags each user-written `haveI`/`letI` tactic whose main goal is a proposition, checked by running `Meta.isProp` on the goal type in the recorded metavariable/local context. Term-mode `haveI`/`letI` and macro-generated syntax are not flagged (documented TODO). The option `linter.style.haveILetI` is off by default; mathlib currently contains ~2,300 sites the linter would flag. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
kbuzzard
added
WIP
PR summary 3ed3c10cef
|
| Files | Import difference |
|---|---|
| ../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all | |
| There are 7255 files with changed transitive imports taking up over 325477 characters: this is too many to display! | |
You can run this locally from your mathlib4 directory: |
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
Declarations diff (regex)
+ Candidate
+ auxLaterTrue.{v}
+ auxSortData
+ auxSortTrue
+ dataFromMixed
+ haveILetILinter
+ oneAsSubtype
+ propEvidence
+ replacement?
+ subsingletonInstance
+ tacticGoalIsProp?
+ termIsProof?
+ trivialTheorem
+ zero
+ zero'
You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.
Declarations diff (Lean)
✅ Lean-aware diff — post-build, computed from the Lean environment (commit
3ed3c10).
- +1 new declarations
- −0 removed declarations
+Mathlib.Linter.linter.style.haveILetINo changes to strong technical debt.
No changes to weak technical debt.
Current commit 3ed3c10cef
Reference commit 32ea179db3
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
I believe we had such a linter in the past. @adomani Did you write that one? Do you remember if that was worth it? |
|
I don't remember this linter, but I do remember writing one to detect |
| let mut seen : Std.HashSet (Option String.Pos.Raw × Option String.Pos.Raw) := {} | ||
| for t in ← getInfoTrees do | ||
| for (ctx, i, kw, repl) in candidates t do | ||
| let range := (i.stx.getPos?, i.stx.getTailPos?) |
There was a problem hiding this comment.
This seems a bit awkward: can't you use directly getRange?? (Talking to Claude here!)
There was a problem hiding this comment.
Claude says you're right and claims that 3ed3c10 implements this.
kbuzzard
changed the title
…argeted suggestion The linter now walks the command's source syntax for user-written haveI/letI (both the tactic and the term versions), looks up the TacticInfo resp. (Partial)TermInfo elaboration records for each occurrence by source range and syntax kind, and flags an occurrence when at least one recorded elaboration is confirmed to have a propositional goal (tactic) resp. to construct a proof of a proposition (term), and none is confirmed otherwise. In particular a haveI run by <;> against both a data goal and a Prop goal is no longer flagged: the single source replacement would also affect the data-goal run. Each flagged occurrence gets one interactive hint (click-to-apply in the InfoView) replacing just the haveI/letI keyword token with have/let, sidestepping any pretty-printing or reformatting of the rest of the syntax. (Lightbulb code actions cannot be offered from linters: runLinters discards info-tree additions made by linters, see leanprover/lean4#4363.) Prop-ness is checked giving every chance to succeed: negative Meta.isProp answers are distrusted while metavariables remain in the type or its sort, and inconclusive checks are retried in the final metavariable context of the surrounding declaration. The latter requires a custom info-tree fold: unlike InfoTree.foldInfo, it does not narrow the context at each info node to the enclosing tactic's own mctxAfter, which would hide metavariable assignments made by later sibling tactic steps (e.g. in later branches of a <;>). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
| return | ||
| unless (← getInfoState).enabled do | ||
| return | ||
| let cands := candidates stx |
There was a problem hiding this comment.
It seems a bit strange to loop through the entire syntax once looking for haveI/letI, followed by looping through all the infotrees trying to refind the haveI/letIs associated to a piece of syntax, finishing by looping through all the haveI/letIs again. I would expect a single loop through the infotrees that does the selection and reporting at once.
I'd hope that a TacticAnalysis pass could even do this looping for us, but perhaps that's expecting too much of my work :)
There was a problem hiding this comment.
Claude says:
- The unit of reporting is a source location, not an elaboration event. One written
haveI
produces several elaboration records (one per goal under<;>/all_goals, plus macro-expansion
copies and postponement retries), and the flag condition is "at least one run confirmed
propositional and none confirmed otherwise" — you can't decide that until you've grouped all
records per occurrence, which is exactly what the syntax-first pass provides. The previous
single-loop version needed a seen-set to dedup and could only express "some run is a Prop", which
is genuinely wrong: for a mixed data/Prop <;>, applying the one source edit changes the data
run's term (there's now a test locking this down). - The suggestion is a source edit of the keyword token, so candidates must be things the user
literally wrote (.originaltoken) — a property of the source syntax, not of info-tree nodes. TacticAnalysiswouldn't cover the term-modehaveI/letIthis PR now lints (including inside
exact/refineand in instance bodies), though a tactic-only fragment could plausibly be expressed
there.- Cost-wise it's still effectively one info-tree fold; the syntax walk is trivial and
short-circuits on commands containing nohaveI/letI.
Let me know if you don't want to talk to an AI. This is Fable 5, the new top model from Anthropic, and I will be losing access to it on Sunday so I am just trying various experiments while I can (e.g. "is it good enough to write a linter")
There was a problem hiding this comment.
Oh, looping through syntax first is at my request in the zulip thread that led to the prompt :) My reasoning is more or less claude's, because I think it's just filling in details of the prompt! XD Not sure about the last loop. And I've only glanced, but in general this code seems waaay more complicated than I think it would need to be... 👀 I wonder if ultracode on relatively straightforward tasks might translate to "more complicated code", not necessarily better code.
…getRange? The docBlame environment linter flagged the auto-generated instInhabitedCandidate.default. The instance was only needed for a `cands[idx]!` lookup, which disappears by storing the candidate itself in the range-keyed map. Also key that map by `Syntax.Range` obtained from `Syntax.getRange?` instead of a hand-rolled pair of positions, as requested in review. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
5 participants
The tactics
haveIandletIdiffer fromhaveandletonly in that they inline the given value into the term being constructed (in current core they are literallyhave +zetaandlet +zeta, sharing a single elaborator). In a tactic proof of a proposition this difference is invisible by proof irrelevance, sohave/letshould be used instead.The linter walks the InfoTree and flags each user-written
haveI/letItactic whose main goal is a proposition, checked by runningMeta.isPropon the goal type in the recorded metavariable/local context. Term-modehaveI/letIand macro-generated syntax are not flagged (documented TODO). The optionlinter.style.haveILetIis off by default; mathlib currently contains ~2,300 sites the linter would flag.This PR is 100% vibe-coded with Claude Fable and I (Kevin Buzzard) can not vouch for any of it, not even the PR description.