feat: config options for fail_if_no_progress#3757
Conversation
|
@thorimur what's the status of this, is there anything I can do to help move it forward? |
f37e947 to
c181194
Compare
* evaluates tactics given instead of running them on the main goal * uses config to specify/restrict progress check
c181194 to
ab5540e
Compare
* namespacing to use `.compare` notation * take length check out of `compareListM`, put in usages * add `resultMsg` to take mode into account * add args to let decl's be accessed in the correct state then passed in
Mathlib/Lean/Meta/Compare.lean
Outdated
| * Different `ExprComparisonConfig`s for each location expressions are compared, ideally with | ||
| default propagation from the top level when writing configs, one way or another |
There was a problem hiding this comment.
I can't make sense of this sentence.
Mathlib/Tactic/FailIfNoProgress.lean
Outdated
| def runAndFailIfNoProgress (goal : MVarId) (tacs : TacticM Unit) | ||
| (cfg : FailIfNoProgress.Config := {}) : TacticM (List MVarId) := do |
There was a problem hiding this comment.
This seems a weird type signature. Perhaps that return type should be MetaM (List MVarId)?
Possibly also tacs should be a MVarId \to MetaM (List MVarId)?
There was a problem hiding this comment.
Does this make sense? My objections are:
- This is all operating in
MetaManyway, usingrun. (maybe TermElabM, whatever) - TacticM shouldn't ever be returning
List MVarId: that's what its state is for! - I want a purely
MetaMlevel version of all this anyway.
There was a problem hiding this comment.
You're right! Looking back I actually don't know why I even defined runAndFailIfNoProgress. I replaced it with MVarId.failIfNoProgress, MVarId.failIfNoProgress', and MVarId.failIfNoProgress1 in analogy to the corresponding liftMetaTactics, all in MetaM.
| @@ -1,12 +1,18 @@ | |||
| import Mathlib.Tactic.FailIfNoProgress | |||
| import Mathlib.Data.List.Basic | |||
|
|
|||
There was a problem hiding this comment.
I'm not going to insist, but it seems the ratio of configuration options to tests is high! We could add more exhaustive tests, or perhaps just try next time to resist the temptation to add so many knobs that we can't even be bothered testing them. :-)
* to `Mathlib.Lean.Meta`
* got rid of `runAndFailIfNoProgress` * added `MVarId.failIfNoProgress` * also `MVarId.failIfNoProgress'`, `MVarId.failIfNoProgress1`
* also strange unintended EOL changes!
Mathlib/Lean/Meta/Compare.lean
Outdated
|
|
||
| /-- Returns `true` if using `BEq` (`.beq`) and `false` if using `isDefEq` (`.defEq`). -/ | ||
| def EqKind.isBEq : EqKind → Bool | ||
| | .beq => true |
There was a problem hiding this comment.
[lint-style] reported by reviewdog 🐶
| | .beq => true | |
| | .beq => true |
There was a problem hiding this comment.
I'm surprised this is part of the linter. There's currently an RFC about this: leanprover/lean4#2580.
There was a problem hiding this comment.
I'm not sure the RFC has much traction. :-)
This PR creates config options for
fail_if_no_progressthat allow the user to tweak what exactly counts as "progress". This includes whether to use defeq orBEq, what transparency to use, and which parts of the goal and local context to check.It also splits off the comparison functionality into
Mathlib.Lean.Meta.Compare, which provides fully configurable comparison functions for common complex metaprogramming types not specific tofail_if_no_progress. These types areExpr,LocalDecl,LocalContext,MetavarDecl,MVarId, andList MVarId.See zulip for a couple review questions.
Status update: this PR is now basically done, save for some extra tests which should probably be included.