feat: config options for `fail_if_no_progress` #3757

thorimur · 2023-05-01T18:02:27Z

This PR creates config options for fail_if_no_progress that allow the user to tweak what exactly counts as "progress". This includes whether to use defeq or BEq, 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 to fail_if_no_progress. These types are Expr, LocalDecl, LocalContext, MetavarDecl, MVarId, and List 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.

alexjbest · 2023-05-28T19:35:32Z

@thorimur what's the status of this, is there anything I can do to help move it forward?

* evaluates tactics given instead of running them on the main goal * uses config to specify/restrict progress check

* 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

joneugster

lgtm :)

kim-em · 2023-08-27T01:19:00Z

Mathlib/Lean/Meta/Compare.lean

+* Different `ExprComparisonConfig`s for each location expressions are compared, ideally with
+default propagation from the top level when writing configs, one way or another


I can't make sense of this sentence.

Rewritten. :)

Mathlib/Lean/Meta/Compare.lean

kim-em · 2023-08-27T01:25:07Z

Mathlib/Tactic/FailIfNoProgress.lean

+def runAndFailIfNoProgress (goal : MVarId) (tacs : TacticM Unit)
+    (cfg : FailIfNoProgress.Config := {}) : TacticM (List MVarId) := do


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)?

Does this make sense? My objections are:

This is all operating in MetaM anyway, using run. (maybe TermElabM, whatever)

TacticM shouldn't ever be returning List MVarId: that's what its state is for!

I want a purely MetaM level version of all this anyway.

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.

Mathlib/Tactic/FailIfNoProgress.lean

kim-em · 2023-08-27T01:31:37Z

test/fail_if_no_progress.lean

@@ -1,12 +1,18 @@
 import Mathlib.Tactic.FailIfNoProgress
+import Mathlib.Data.List.Basic



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!

github-actions · 2023-10-22T05:21:44Z

Mathlib/Lean/Meta/Compare.lean

+
+/-- Returns `true` if using `BEq` (`.beq`) and `false` if using `isDefEq` (`.defEq`). -/
+def EqKind.isBEq : EqKind → Bool
+| .beq   => true


[lint-style] _{reported by reviewdog 🐶}

Suggested change

| .beq => true

| .beq => true

I'm surprised this is part of the linter. There's currently an RFC about this: leanprover/lean4#2580.

I'm not sure the RFC has much traction. :-)

thorimur added WIP Work in progress t-meta Tactics, attributes or user commands labels May 1, 2023

This was referenced May 1, 2023

[Merged by Bors] - feat: implement intermediate state for simp_rw #3738

Closed

feat: implement simp_rw fails if unchanged #3782

Closed

kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 2, 2023

thorimur force-pushed the fail_if_no_progress branch from f37e947 to c181194 Compare June 5, 2023 00:01

kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 5, 2023

kim-em added the awaiting-author A reviewer has asked the author a question or requested changes label Jun 20, 2023

kim-em mentioned this pull request Jul 8, 2023

chore: make sure simp_rw uses each lemma #5770

Closed

thorimur added 3 commits July 9, 2023 01:33

enhance: fail_if_no_progress

0d96418

* evaluates tactics given instead of running them on the main goal * uses config to specify/restrict progress check

test: basic config tests

b4c5b21

minor fixes

ab5540e

thorimur force-pushed the fail_if_no_progress branch from c181194 to ab5540e Compare July 9, 2023 05:34

thorimur added 2 commits July 9, 2023 06:25

feat: revamp configs

96bd5ae

docs: config note

2646fdb

thorimur removed the awaiting-author A reviewer has asked the author a question or requested changes label Jul 9, 2023

thorimur added 13 commits July 10, 2023 07:06

remove default propagation

c484d8b

remove zips and unnecessary logic functions

3997461

more removal of default propagation

6f66143

compare* implementations (first draft)

23c4347

adjust main functions accordingly

8e6d3a2

change default for includeImplDetails to false

e93e053

deriving Repr, Inhabited for new structures etc.

fde8aa4

change default for checkIndex of mvars to false

a053d6d

remove erroneous comment

d4c8f6d

remove erroneous comment (2)

468087a

tweak: adjust default values

dc3a0de

feat: MVarIdComparisonConfig

709b346

style, refactor fixes:

e521ca9

* 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

docs: explain two-config pattern

c3bee29

thorimur commented Aug 13, 2023

View reviewed changes

Mathlib/Lean/Meta/Compare.lean Outdated Show resolved Hide resolved

lint: long lines

0b61185

joneugster approved these changes Aug 13, 2023

View reviewed changes

kim-em reviewed Aug 27, 2023

View reviewed changes

Mathlib/Lean/Meta/Compare.lean Outdated Show resolved Hide resolved

kim-em reviewed Aug 27, 2023

View reviewed changes

Mathlib/Tactic/FailIfNoProgress.lean Outdated Show resolved Hide resolved

kim-em reviewed Aug 27, 2023

View reviewed changes

kim-em added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Aug 27, 2023

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 Sep 10, 2023

bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:23

kim-em changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:18

thorimur added 8 commits October 21, 2023 22:58

Merge remote-tracking branch 'origin/master' into fail_if_no_progress

d4d3180

chore: alphabetize Mathlib.lean

e2375f7

refactor: move BEq MetavarKind instance

70cc2bf

* to `Mathlib.Lean.Meta`

chore: misc. reorganization of Mathlib.Lean.Meta

68b07e0

feat: preset: .nothing for single-field checks

3a2c1e6

refactor, feat: MetaM versions

1c8edf1

* got rid of `runAndFailIfNoProgress` * added `MVarId.failIfNoProgress` * also `MVarId.failIfNoProgress'`, `MVarId.failIfNoProgress1`

fix: imports

9ef668c

docs: misc. fixes

9b89aa2

* also strange unintended EOL changes!

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 Oct 22, 2023

github-actions bot reviewed Oct 22, 2023

View reviewed changes

satisfy the linter

bd1f963

thorimur added WIP Work in progress and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 22, 2023

lint: add docstring

55757c5

thorimur mentioned this pull request Nov 19, 2023

[Merged by Bors] - fix: local context handling in fail_if_no_progress #8482

Closed

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 Nov 22, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: config options for `fail_if_no_progress` #3757

feat: config options for `fail_if_no_progress` #3757

thorimur commented May 1, 2023 •

edited

Loading

alexjbest commented May 28, 2023

joneugster left a comment

kim-em Aug 27, 2023

thorimur Oct 22, 2023

kim-em Aug 27, 2023

kim-em Aug 27, 2023

thorimur Oct 22, 2023

kim-em Aug 27, 2023

github-actions bot Oct 22, 2023

thorimur Oct 22, 2023

kim-em Oct 23, 2023

		* Different `ExprComparisonConfig`s for each location expressions are compared, ideally with
		default propagation from the top level when writing configs, one way or another

		def runAndFailIfNoProgress (goal : MVarId) (tacs : TacticM Unit)
		(cfg : FailIfNoProgress.Config := {}) : TacticM (List MVarId) := do

		@@ -1,12 +1,18 @@
		import Mathlib.Tactic.FailIfNoProgress
		import Mathlib.Data.List.Basic

feat: config options for fail_if_no_progress #3757

Are you sure you want to change the base?

feat: config options for fail_if_no_progress #3757

Conversation

thorimur commented May 1, 2023 • edited Loading

alexjbest commented May 28, 2023

joneugster left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

github-actions bot Oct 22, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

feat: config options for `fail_if_no_progress` #3757

feat: config options for `fail_if_no_progress` #3757

thorimur commented May 1, 2023 •

edited

Loading