Skip to content

feat: turning on failIfUnchanged by default in simp#2336

Merged
leodemoura merged 1 commit intoleanprover:masterfrom
kim-em:simp_failIfUnchanged_default
Aug 16, 2023
Merged

feat: turning on failIfUnchanged by default in simp#2336
leodemoura merged 1 commit intoleanprover:masterfrom
kim-em:simp_failIfUnchanged_default

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

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

@kim-em kim-em force-pushed the simp_failIfUnchanged_default branch 5 times, most recently from 092b366 to c57254e Compare July 20, 2023 05:27
@kim-em kim-em mentioned this pull request Jul 20, 2023
Merged
@kim-em kim-em force-pushed the simp_failIfUnchanged_default branch 2 times, most recently from db16124 to ad4e587 Compare July 20, 2023 07:13
@kim-em kim-em mentioned this pull request Jul 20, 2023
Merged
3 tasks
@kim-em kim-em changed the title experiment: turning on failIfUnchanged by default in simp feat: turning on failIfUnchanged by default in simp Jul 20, 2023
@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
Copy link
Copy Markdown
Member

leodemoura commented Jul 20, 2023

This change must be documented in the change log: https://github.com/leanprover/lean4/blob/master/RELEASES.md
We must also document why it has been made, and add links to zulip threads where the discussion happened, and how the consensus has been reached.
Reason: this change will affect (non mathlib) users.

@leodemoura leodemoura added the awaiting-author Waiting for PR author to address issues label Jul 24, 2023
@kim-em kim-em force-pushed the simp_failIfUnchanged_default branch 3 times, most recently from 2ecfdad to 18c3349 Compare August 2, 2023 01:06
@kim-em kim-em force-pushed the simp_failIfUnchanged_default branch 3 times, most recently from 1869e45 to 8cc17a3 Compare August 14, 2023 01:05
@kim-em kim-em force-pushed the simp_failIfUnchanged_default branch from 8cc17a3 to 6e8fec8 Compare August 15, 2023 03:31
@kim-em kim-em removed the awaiting-author Waiting for PR author to address issues label Aug 15, 2023
@leodemoura leodemoura merged commit f1412dd into leanprover:master Aug 16, 2023
rami3l added a commit to rami3l/PLFaLean that referenced this pull request Sep 2, 2023
@rami3l
chore(deps): upgrading lean to v4.0.0-rc4
a9f84a0 
Fixing breakages caused by leanprover/lean4#2336.
@rami3l rami3l mentioned this pull request Sep 2, 2023
Merged
@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 left review comments

@leodemoura leodemoura leodemoura left review comments

+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

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

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