Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: turning on failIfUnchanged by default in simp #2336

Merged
merged 1 commit into from
Aug 16, 2023
Merged

feat: turning on failIfUnchanged by default in simp #2336

merged 1 commit into from
Aug 16, 2023

Conversation

kim-em
Copy link
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
@leodemoura
Copy link
Member

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/plfl 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

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

@digama0 digama0 digama0 left review comments

@leodemoura leodemoura leodemoura left review comments

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