[Merged by Bors] - chore: adaptations for nightly-2025-11-02 #103
Conversation
* switch to modulized quote4 * increment rootHashGeneration * include .ir files * try minimizing failure * minimize more * use adjusted cache * less minimal * unminimize all * restore --------- Co-authored-by: Kim Morrison <kim@tqft.net>
…hlib4-nightly-testing into nightly-testing
|
|
| Due to a change in `grind` between `nightly-2025-10-31` and `nightly-2025-11-02`, | ||
| this proof is no longer working. I've temporarily commented it out to get a build of | ||
| `nightly-testing`. | ||
| -/ |
There was a problem hiding this comment.
My understanding was that we now have a working proof again. Do we fix this now or tomorrow?
There was a problem hiding this comment.
I think it's best tomorrow. The working proof wasn't into nightly-testing in time for the nightly-testing-2025-11-02 tag. We could choose to abandon this PR and roll everything into tomorrow, if it's too painful to flip back and forth.
| theorem asString_nil : [].asString = "" := | ||
| rfl | ||
|
|
||
| theorem toList_empty : "".toList = [] := |
There was a problem hiding this comment.
Should the deleted theorems toList_inj and toList_empty be deprecated?
There was a problem hiding this comment.
These were upstreamed, not deleted. We don't really have good tooling to explain this automatically at present, beyond pasting them back in and seeing X has already been declared.
kbuzzard
left a comment
kbuzzard
left a comment
There was a problem hiding this comment.
Right at the bottom of the files diff there's a new file lean4checker in the root directoy, and I was not able to leave a github comment on it saying "was this file added intentionally?" for some reason.
fixed, that was my mistake |
|
Modulo the comments this looks ready to merge |
|
bors merge |
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: github-actions <github-actions@github.com>
|
Pull request successfully merged into bump/v4.26.0. Build succeeded: |
mathlib-bors
bot
changed the title
No description provided.