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

chore: simp tracing reports ← #2621

Merged
merged 5 commits into from
Oct 15, 2023
Merged

chore: simp tracing reports ← #2621

merged 5 commits into from
Oct 15, 2023

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Oct 4, 2023

@kim-em kim-em requested a review from digama0 October 4, 2023 02:42
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Oct 4, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 4, 2023
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#2621
1e34b23
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Oct 4, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Oct 4, 2023 •
edited
Loading

@digama0 digama0 self-assigned this Oct 4, 2023
@kim-em
Copy link
Collaborator Author

kim-em commented Oct 4, 2023

@digama0 if it's useful for reviewing I can make proposed downstream changes to Std and Mathlib as well, but won't immediately unless you say so.

@kim-em
Copy link
Collaborator Author

kim-em commented Oct 10, 2023

@digama0, I'd like to get this in, but am uncertain whether your self-assignment above means:

  • that I shouldn't do further work on this because you have in mind a better solution?
  • that I should do the downstream fixes to Std and Mathlib required for this approach, and then you'll review?

@digama0
Copy link
Collaborator

digama0 commented Oct 10, 2023

It means I was planning on reviewing it, but I was at a conference last week so I'm just now working down my backlog. I'll take a look at it now or tomorrow.

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 10, 2023
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#2621
bf05713
kim-em added a commit to kim-em/std4 that referenced this pull request Oct 13, 2023
@kim-em
chore: adapt to leanprover/lean4#2621
371f599
kim-em added a commit to kim-em/aesop that referenced this pull request Oct 13, 2023
@kim-em
chore: adapt to leanprover/lean4#2621
580935a
@kim-em kim-em mentioned this pull request Oct 13, 2023
Merged
@kim-em
Copy link
Collaborator Author

kim-em commented Oct 13, 2023

Phew, lots of downstream changes required for this one:

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 13, 2023
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#2621
6e35681
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 13, 2023
@kim-em
trigger CI for leanprover/lean4#2621
4aaf457
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Oct 13, 2023
@kim-em kim-em added the awaiting-review Waiting for someone to review the PR label Oct 14, 2023
@kim-em kim-em requested a review from digama0 October 14, 2023 03:32
@kim-em
Copy link
Collaborator Author

kim-em commented Oct 14, 2023

I've checked that downstream projects survive okay. There is some unfortunate copypasta there that ideally we can clean up later.

@kim-em kim-em merged commit 66ab016 into leanprover:master Oct 15, 2023
kim-em added a commit to leanprover-community/batteries that referenced this pull request Oct 16, 2023
@kim-em
chore: bump to v4.2.0-rc2 (#284)
85a0d48 
* chore: adapt to leanprover/lean4#2621

* bump to v4.2.0-rc2
kim-em added a commit to leanprover-community/aesop that referenced this pull request Oct 16, 2023
@kim-em
chore: bump to v4.2.0-rc2 (#72)
0bd8465 
* fix: use replay from leanprover/lean4#2617

* chore: adapt to leanprover/lean4#2621

* bump to v4.2.0-rc2
thorimur pushed a commit to thorimur/std4 that referenced this pull request Oct 23, 2023
@kim-em @thorimur
chore: adapt to leanprover/lean4#2621
152dd40
thorimur pushed a commit to thorimur/std4 that referenced this pull request Oct 23, 2023
@kim-em @thorimur
chore: adapt to leanprover/lean4#2621
4de66d7
thorimur pushed a commit to thorimur/std4 that referenced this pull request Oct 24, 2023
@kim-em @thorimur
chore: adapt to leanprover/lean4#2621
3db2e47
thorimur pushed a commit to thorimur/std4 that referenced this pull request Oct 24, 2023
@kim-em @thorimur
chore: adapt to leanprover/lean4#2621
02be031
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

Assignees

@digama0 digama0

Labels
awaiting-review Waiting for someone to review the PR builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Incorrect simp tracing for local right-to-left simp theorems ([<- x])
3 participants
@kim-em @leanprover-community-mathlib4-bot @digama0