[Merged by Bors] - chore: backports of adaptations for leanprover/lean4#6024 #18896
Conversation
github-actions
bot
added
the
large-import
PR summary ea2e06bd54Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for |
github-actions
bot
removed
the
large-import
There was a problem hiding this comment.
This is all fine. Re the new adaptation notes: I don't really understand enough about why they are there to comment, but I was surprised that they just all mentioned a date 11-11-2024 rather than the Lean issue leanprover/lean4#6024 which was the cause of the adaptation.
I also note that the Lean PR is not yet merged. I'm just flagging this because I don't really understand the workflow.
|
bors d+ |
|
✌️ kim-em can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Good point @kbuzzard, I'll adjust the adaptation notes. Regarding the workflow, with this PR we're just trying to modify Mathlib to avoid making use of an existing bug. It's not necessary to do this, but it's a way we can make the adaptation PRs less massive down the line. It can also make fixing |
|
bors r+ |
leanprover/lean4#6024 fixes a serious elaboration bug which, perversely, was quite helpful. Kyle is investigating replacing the bug with something intentional, but we definitively need to fix the bug in the meantime. This is the backport of changes from lean-pr-testing-6024 which do not have conflicts with `master`. There are a few more changes that we'll need to handle separately later. Co-authored-by: Kyle Miller <kmill31415@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
leanprover/lean4#6024 fixes a serious elaboration bug which, perversely, was quite helpful. Kyle is investigating replacing the bug with something intentional, but we definitively need to fix the bug in the meantime. This is the backport of changes from lean-pr-testing-6024 which do not have conflicts with `master`. There are a few more changes that we'll need to handle separately later. Co-authored-by: Kyle Miller <kmill31415@gmail.com>
leanprover/lean4#6024 fixes a serious elaboration bug which, perversely, was quite helpful.
Kyle is investigating replacing the bug with something intentional, but we definitively need to fix the bug in the meantime.
This is the backport of changes from lean-pr-testing-6024 which do not have conflicts with
master. There are a few more changes that we'll need to handle separately later.