chore: adaptations for nightly-2025-08-19 #39
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…hlib4-nightly-testing into nightly-testing
* Update lean-toolchain for testing leanprover/lean4#9084 * Update lean-toolchain for leanprover/lean4#9084 * Update Batteries branch for testing leanprover-community/batteries#1306 * chore: adaptation to batteries#1306 * Update lean-toolchain for testing leanprover/lean4#9423 * Update lean-toolchain for testing leanprover/lean4#9424 * chore: update 'unknown identifier' test ouputs * chore: update 'tactic failed' test outputs * fix(scripts/create-adaptation-pr): improve find_remote (leanprover-community#26974) The old one was a syntax error and would've found a `mathlib4-nightly-testing` remote as a `mathlib4` remote (due to substring); this one is a bit more strict and works at least on my machine :-) * Merge master into nightly-testing * Update lean-toolchain for leanprover/lean4#9423 * Update lean-toolchain for leanprover/lean4#9424 * chore: update tactic error test outputs * Update lean-toolchain for leanprover/lean4#9423 * Merge master into nightly-testing * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#9443 * fixes * fixes * Merge master into nightly-testing * Merge master into nightly-testing * fix * chore: bump to nightly-2025-07-22 * Merge master into nightly-testing * adaptation notes for breakages in batteries * update Cache * fix * lake update * Merge master into nightly-testing * deprecation * fixes for Shake * shake * shake --update * fix noisy build detection * Merge master into nightly-testing * chore: bump to nightly-2025-07-23 * Merge master into nightly-testing * Merge master into nightly-testing * fix * revert commenting out * fix noisy test * Merge master into nightly-testing * Merge master into nightly-testing * chore: bump to nightly-2025-07-24 * Merge master into nightly-testing * Merge master into nightly-testing * Merge master into nightly-testing * fixes for changes to Lean.Grind.NatModule * oops * Merge master into nightly-testing * chore: bump to nightly-2025-07-25 * fix * fix(scripts/create-adaption-pr.sh): fetch `master` if necessary (leanprover-community#27293) Makes sure that `master` is available, in particular when the remote has been automatically added. * chore: make create-adapation-pr.sh robust to running on nightly-testing fork (leanprover-community#27411) cf recent failures at [#nightly-testing > Mathlib bump branch reminders @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20bump.20branch.20reminders/near/530460702) * fix da script * `lake exe mk_all` * hmm let's see what breaks * not these * hmm..? * hmm this one as well * more changes that turn out to be necessary * Restore files from testing/nightly-testing * Restore files from testing/nightly-testing * Restore files from testing/nightly-testing * Revert accidentals * `mk_all` * fix `@[to_additive]` * Restore files from testing/nightly-testing * re-add changes * restore some more stuff carefully * these * try fix things * chore: bump to nightly-2025-07-26 * fix by restoring mathlib change * restore master versions of mis-merged files * restore master versions of mis-merged files * fix merge * comment out with adaptation note * huh? * lake update * lake update * fix import * shaking * shaking * shaking * chore: bump to nightly-2025-07-27 * lake update * mk_all * fix merges * more missed changes (#18) * Merge master into nightly-testing * feat: establish examples of harmonic functions (leanprover-community#26844) If `f : ℂ → F` is complex-differentiable, then show that `f` is harmonic. If `F = ℂ`, then so is its real part, imaginary part, and complex conjugate. If `f` has no zero, then `log ‖f‖` is harmonic. This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. It is one of the ingredients in the proof of Jensen's Formula in complex analysis. * chore: replace `Monoid.IsTorsionFree` with `IsMulTorsionFree` (leanprover-community#24311) From Toric * fix tests --------- Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> * fix test (#19) * last fix I swear * unnecessary duplicate imports * these are actual unused imports (because of core changes?) * test fix * chore: adaptations for nightly-2025-07-27 * chore: bump to nightly-2025-07-28 * Update lean-toolchain for testing leanprover/lean4#9587 * grind lemma * more * chore(Cache): enable FRO cache (#17) * chore: revert "enable FRO cache (#17)" This reverts commit 1da13d9. * Restore regression * chore: adaptations for nightly-2025-07-28 * chore: adaptations for nightly-2025-07-28 * chore: adaptations for nightly-2025-07-28 * chore: adaptations for nightly-2025-07-28 * adaptation notes * chore: bump to nightly-2025-07-29 * chore: adaptations for nightly-2025-07-29 * fix; bad merge? * chore: bump to nightly-2025-07-30 * Update lean-toolchain for testing leanprover/lean4#9633 * deprecation * Update lean-toolchain for leanprover/lean4#9633 * chore: update test error message outputs * adaptation note about Xor' * shake --update * chore: bump to nightly-2025-07-31 * fix * fix test output * fix test output * fix test output * chore: bump to nightly-2025-08-01 * fix * Update lean-toolchain for leanprover/lean4#9587 * chore: bump to nightly-2025-08-02 * Bump batteries * Fix warning * chore: bump to nightly-2025-08-03 * update test * fix test * fix merge? * chore: bump to nightly-2025-08-04 * fix --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: F. G. Dorais <fgdorais@gmail.com> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Mac Malone <tydeu@hatpress.net> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
* Update lean-toolchain for testing leanprover/lean4#9084 * Update lean-toolchain for leanprover/lean4#9084 * Update Batteries branch for testing leanprover-community/batteries#1306 * chore: adaptation to batteries#1306 * Update lean-toolchain for testing leanprover/lean4#9423 * Update lean-toolchain for testing leanprover/lean4#9424 * chore: update 'unknown identifier' test ouputs * chore: update 'tactic failed' test outputs * fix(scripts/create-adaptation-pr): improve find_remote (leanprover-community#26974) The old one was a syntax error and would've found a `mathlib4-nightly-testing` remote as a `mathlib4` remote (due to substring); this one is a bit more strict and works at least on my machine :-) * Merge master into nightly-testing * Update lean-toolchain for leanprover/lean4#9423 * Update lean-toolchain for leanprover/lean4#9424 * chore: update tactic error test outputs * Update lean-toolchain for leanprover/lean4#9423 * Merge master into nightly-testing * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#9443 * fixes * fixes * Merge master into nightly-testing * Merge master into nightly-testing * fix * chore: bump to nightly-2025-07-22 * Merge master into nightly-testing * adaptation notes for breakages in batteries * update Cache * fix * lake update * Merge master into nightly-testing * deprecation * fixes for Shake * shake * shake --update * fix noisy build detection * Merge master into nightly-testing * chore: bump to nightly-2025-07-23 * Merge master into nightly-testing * Merge master into nightly-testing * fix * revert commenting out * fix noisy test * Merge master into nightly-testing * Merge master into nightly-testing * chore: bump to nightly-2025-07-24 * Merge master into nightly-testing * Merge master into nightly-testing * Merge master into nightly-testing * fixes for changes to Lean.Grind.NatModule * oops * Merge master into nightly-testing * chore: bump to nightly-2025-07-25 * fix * fix(scripts/create-adaption-pr.sh): fetch `master` if necessary (leanprover-community#27293) Makes sure that `master` is available, in particular when the remote has been automatically added. * chore: make create-adapation-pr.sh robust to running on nightly-testing fork (leanprover-community#27411) cf recent failures at [#nightly-testing > Mathlib bump branch reminders @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20bump.20branch.20reminders/near/530460702) * fix da script * `lake exe mk_all` * hmm let's see what breaks * not these * hmm..? * hmm this one as well * more changes that turn out to be necessary * Restore files from testing/nightly-testing * Restore files from testing/nightly-testing * Restore files from testing/nightly-testing * Revert accidentals * `mk_all` * fix `@[to_additive]` * Restore files from testing/nightly-testing * re-add changes * restore some more stuff carefully * these * try fix things * chore: bump to nightly-2025-07-26 * fix by restoring mathlib change * restore master versions of mis-merged files * restore master versions of mis-merged files * fix merge * comment out with adaptation note * huh? * lake update * lake update * fix import * shaking * shaking * shaking * chore: bump to nightly-2025-07-27 * lake update * mk_all * fix merges * more missed changes (#18) * Merge master into nightly-testing * feat: establish examples of harmonic functions (leanprover-community#26844) If `f : ℂ → F` is complex-differentiable, then show that `f` is harmonic. If `F = ℂ`, then so is its real part, imaginary part, and complex conjugate. If `f` has no zero, then `log ‖f‖` is harmonic. This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. It is one of the ingredients in the proof of Jensen's Formula in complex analysis. * chore: replace `Monoid.IsTorsionFree` with `IsMulTorsionFree` (leanprover-community#24311) From Toric * fix tests --------- Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> * fix test (#19) * last fix I swear * unnecessary duplicate imports * these are actual unused imports (because of core changes?) * test fix * chore: adaptations for nightly-2025-07-27 * chore: bump to nightly-2025-07-28 * Update lean-toolchain for testing leanprover/lean4#9587 * grind lemma * more * chore(Cache): enable FRO cache (#17) * chore: revert "enable FRO cache (#17)" This reverts commit 1da13d9. * Restore regression * chore: adaptations for nightly-2025-07-28 * chore: adaptations for nightly-2025-07-28 * chore: adaptations for nightly-2025-07-28 * chore: adaptations for nightly-2025-07-28 * adaptation notes * chore: bump to nightly-2025-07-29 * chore: adaptations for nightly-2025-07-29 * fix; bad merge? * chore: bump to nightly-2025-07-30 * Update lean-toolchain for testing leanprover/lean4#9633 * deprecation * Update lean-toolchain for leanprover/lean4#9633 * chore: update test error message outputs * adaptation note about Xor' * shake --update * chore: bump to nightly-2025-07-31 * fix * fix test output * fix test output * fix test output * chore: bump to nightly-2025-08-01 * fix * Update lean-toolchain for leanprover/lean4#9587 * chore: bump to nightly-2025-08-02 * Bump batteries * Fix warning * chore: bump to nightly-2025-08-03 * update test * fix test * fix merge? * chore: bump to nightly-2025-08-04 * fix * chore: bump to nightly-2025-08-05 * deprecations * shake --fix * fix imports * remove Shake again? --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: F. G. Dorais <fgdorais@gmail.com> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Mac Malone <tydeu@hatpress.net> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
…no nightly-testing release.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.