Skip to content

feat: add failIfUnchanged flag to simp#2334

Merged
leodemoura merged 1 commit intoleanprover:masterfrom
kim-em:simp_failIfUnchanged
Aug 13, 2023
Merged

feat: add failIfUnchanged flag to simp#2334
leodemoura merged 1 commit intoleanprover:masterfrom
kim-em:simp_failIfUnchanged

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Jul 19, 2023 •
edited
Loading

This adds a flag failIfUnchanged to the configuration options of dsimp / simp / simp_all.

The followup PR #2336 turns the flag on by default. See there for links to builds for Std and Mathlib with the flag enabled.

digama0
digama0 reviewed Jul 19, 2023
View reviewed changes
@kim-em kim-em force-pushed the simp_failIfUnchanged branch 4 times, most recently from 32d61c5 to 8dcb32b Compare July 20, 2023 05:26
This was referenced Jul 20, 2023
Merged
Merged
@kim-em kim-em added the awaiting-review Waiting for someone to review the PR label Jul 20, 2023
@kim-em kim-em mentioned this pull request Jul 20, 2023
Closed
8 tasks
eric-wieser
eric-wieser reviewed Jul 20, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Jul 20, 2023
View reviewed changes
leodemoura
leodemoura reviewed Jul 20, 2023
View reviewed changes
@leodemoura leodemoura added the awaiting-author Waiting for PR author to address issues label Jul 24, 2023
@leodemoura
Copy link
Copy Markdown
Member

leodemoura commented Jul 24, 2023

Waiting on author addressing questions above.

@kim-em kim-em force-pushed the simp_failIfUnchanged branch 2 times, most recently from 78c8c84 to 2ab8c09 Compare July 31, 2023 00:19
digama0
digama0 reviewed Jul 31, 2023
View reviewed changes
@kim-em kim-em removed the awaiting-review Waiting for someone to review the PR label Aug 1, 2023
@kim-em kim-em force-pushed the simp_failIfUnchanged branch from d905021 to 485dfa8 Compare August 2, 2023 01:03
@kim-em kim-em added awaiting-review Waiting for someone to review the PR needs-update-stage0 stage 0 should be updated after merging this PR and removed awaiting-author Waiting for PR author to address issues labels Aug 2, 2023
leodemoura
leodemoura reviewed Aug 3, 2023
View reviewed changes
@kim-em kim-em force-pushed the simp_failIfUnchanged branch from 3c063d1 to 296a76e Compare August 9, 2023 01:37
@leodemoura leodemoura added awaiting-author Waiting for PR author to address issues and removed awaiting-review Waiting for someone to review the PR labels Aug 9, 2023
@kim-em kim-em mentioned this pull request Aug 10, 2023
Closed
1 task
@kim-em kim-em force-pushed the simp_failIfUnchanged branch from 296a76e to a30de15 Compare August 10, 2023 12:04
@kim-em kim-em force-pushed the simp_failIfUnchanged branch from a30de15 to 70a728b Compare August 10, 2023 12:07
@kim-em kim-em linked an issue Aug 10, 2023 that may be closed by this pull request
simp_all reorders hypotheses unnecessarily #2402
Closed
1 task
@kim-em kim-em added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Aug 10, 2023
@kim-em kim-em requested a review from leodemoura August 10, 2023 12:08
@leodemoura
Copy link
Copy Markdown
Member

leodemoura commented Aug 13, 2023

I am going to merge it as-is. From now on, I expect way more tests when making this kind of change. It is hard to believe 3 new simp_all tests covers all interesting cases.

@leodemoura leodemoura merged commit 61fea57 into leanprover:master Aug 13, 2023
@kim-em kim-em mentioned this pull request Oct 4, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@digama0 digama0 digama0 approved these changes

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

+1 more reviewer

@eric-wieser eric-wieser eric-wieser left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

awaiting-review Waiting for someone to review the PR needs-update-stage0 stage 0 should be updated after merging this PR

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

simp_all reorders hypotheses unnecessarily

4 participants

@kim-em @leodemoura @eric-wieser @digama0