[Merged by Bors] - fix(scripts/create-adaptation-pr): improve find_remote#26974
Closed
Rob23oba wants to merge 1 commit intoleanprover-community:masterfrom
Closed
[Merged by Bors] - fix(scripts/create-adaptation-pr): improve find_remote#26974Rob23oba wants to merge 1 commit intoleanprover-community:masterfrom
Rob23oba wants to merge 1 commit intoleanprover-community:masterfrom
Conversation
PR summary cfc5f69eb8Import 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 No changes to technical debt.You can run this locally as
|
Contributor
|
Thanks! |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jul 10, 2025
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 :-)
Contributor
|
Pull request successfully merged into master. Build succeeded: |
BeibeiX0
pushed a commit
to BeibeiX0/mathlib4
that referenced
this pull request
Jul 16, 2025
…mmunity#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 :-)
Rob23oba
added a commit
to Rob23oba/mathlib4
that referenced
this pull request
Jul 18, 2025
…mmunity#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 :-)
callesonne
pushed a commit
to callesonne/mathlib4
that referenced
this pull request
Jul 24, 2025
…mmunity#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 :-)
hrmacbeth
pushed a commit
to szqzs/mathlib4
that referenced
this pull request
Jul 28, 2025
…mmunity#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 :-)
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jul 29, 2025
* Update lean-toolchain for testing leanprover/lean4#9084 * Update lean-toolchain for leanprover/lean4#9084 * 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 * 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 --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.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>
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Aug 6, 2025
* 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>
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Aug 6, 2025
* 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>
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Aug 7, 2025
* 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? * chore: bump to nightly-2025-08-06 --------- 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>
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Aug 17, 2025
* 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? * chore: adaptations for nightly-2025-08-04 (#26) * 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> * remove Shake * chore: adaptations for nightly-2025-08-05 (#27) * 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> * chore: bump to nightly-2025-08-06 * fix * chore: adaptations for nightly-2025-08-06 (#29) * 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? * chore: bump to nightly-2025-08-06 --------- 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> * chore: bump to nightly-2025-08-07 * lake update aesop * lake update aesop * deprecations * chore: bump to nightly-2025-08-08 * Update lean-toolchain for testing leanprover/lean4#9800 * Update lean-toolchain for leanprover/lean4#9800 * Update lean-toolchain for leanprover/lean4#9800 * Update lean-toolchain for leanprover/lean4#9800 * addressing some cases of mathlib4#380 * fix tests * Update lean-toolchain for leanprover/lean4#9800 * Update lean-toolchain for leanprover/lean4#9800 * chore: bump to nightly-2025-08-10 * fix (all?) `protected` regressions * Update lean-toolchain for leanprover/lean4#9800 * fix * adaptation note? * noncomputable * revert grind proof * remove upstreamed * fixes * feat: better statement of flip_map_app * sad adaptation note * update adaptation note * fix merge * chore: bump to nightly-2025-08-11 * chore: adaptations for nightly-2025-08-11 * chore: adaptations for nightly-2025-08-11 * fixes * fix * fix toolchain? * Update lean-toolchain for testing leanprover/lean4#9729 * use legacy lemma for now * revert bad changes * upstream LE/LT (Subtype p) instances * chore(Cache): use FRO cache (v2) (#30) * chore(Cache): enable FRO cache * feat: only print "packing" when actually packing * feat: always prefix with repo in FRO cache * fix * chore: bump to nightly-2025-08-12 * chore: trigger rebuild to test cache * chore: use `cache put!` in CI to debug * shake --update * chore: adaptations for nightly-2025-08-12 * empty * chore: bump to nightly-2025-08-13 * Revert "chore: use `cache put!` in CI to debug" This reverts commit 7c6202b. * redundant grind warnings * revert leanprover-community#28272: add back grind proofs * fix test * chore: adaptations for nightly-2025-08-13 * fixes * restore test * chore: bump to nightly-2025-08-14 * adaptation note about grind regression * fix tests * update test output * chore: bump to nightly-2025-08-16 * bump proofwidgets * bump proofwidgets * chore: bump to nightly-2025-08-17 * chore: adaptations for nightly-2025-08-17 * Apply suggestions from code review --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.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: 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: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Aug 24, 2025
* chore: bump to nightly-2025-08-05 * deprecations * shake --fix * fix imports * remove Shake again? * chore: adaptations for nightly-2025-08-04 (#26) * 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> * remove Shake * chore: adaptations for nightly-2025-08-05 (#27) * 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> * chore: bump to nightly-2025-08-06 * fix * chore: adaptations for nightly-2025-08-06 (#29) * 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? * chore: bump to nightly-2025-08-06 --------- 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> * chore: bump to nightly-2025-08-07 * lake update aesop * lake update aesop * deprecations * chore: bump to nightly-2025-08-08 * Update lean-toolchain for testing leanprover/lean4#9800 * Update lean-toolchain for leanprover/lean4#9800 * Update lean-toolchain for leanprover/lean4#9800 * Update lean-toolchain for leanprover/lean4#9800 * addressing some cases of mathlib4#380 * fix tests * Update lean-toolchain for leanprover/lean4#9800 * Update lean-toolchain for leanprover/lean4#9800 * chore: bump to nightly-2025-08-10 * fix (all?) `protected` regressions * Update lean-toolchain for leanprover/lean4#9800 * fix * adaptation note? * noncomputable * revert grind proof * remove upstreamed * fixes * feat: better statement of flip_map_app * sad adaptation note * update adaptation note * fix merge * chore: bump to nightly-2025-08-11 * chore: adaptations for nightly-2025-08-11 * chore: adaptations for nightly-2025-08-11 * fixes * fix * fix toolchain? * Update lean-toolchain for testing leanprover/lean4#9729 * use legacy lemma for now * revert bad changes * upstream LE/LT (Subtype p) instances * chore(Cache): use FRO cache (v2) (#30) * chore(Cache): enable FRO cache * feat: only print "packing" when actually packing * feat: always prefix with repo in FRO cache * fix * chore: bump to nightly-2025-08-12 * chore: trigger rebuild to test cache * chore: use `cache put!` in CI to debug * shake --update * chore: adaptations for nightly-2025-08-12 * empty * chore: bump to nightly-2025-08-13 * Revert "chore: use `cache put!` in CI to debug" This reverts commit 7c6202b. * redundant grind warnings * revert leanprover-community#28272: add back grind proofs * fix test * chore: adaptations for nightly-2025-08-13 * fixes * restore test * chore: bump to nightly-2025-08-14 * adaptation note about grind regression * fix tests * update test output * feat: workflow for reporting `grind` regressions This PR contains a (untested!) workflow that is supposed to build Mathlib with a few tactic analysis flags. It reports the results of these build steps to Zulip for the FRO (and in particular Kim). * chore: bump to nightly-2025-08-16 * bump proofwidgets * bump proofwidgets * Update lean-toolchain for testing leanprover/lean4#9942 * chore: bump to nightly-2025-08-17 * chore: adaptations for nightly-2025-08-17 * Update lean-toolchain for leanprover/lean4#9942 * Update lean-toolchain for leanprover/lean4#9942 * make `filter_upwards` more robust to side goals * Update lean-toolchain for leanprover/lean4#9674 * simpler change to filter_upwards * chore: bump to nightly-2025-08-18 * Apply suggestions from code review * Use JS to generate uuid instead of uuidgen which appears not to be installed * GH Problem Matcher wrapper doesn't like multiline arguments; wrap multiple steps instead. * Hmm, maybe uuidgen exists and it was gh-problem-matcher that was the issue? * Can we just `apt install` dependencies? * Apparently Linux exposes uuids from the kernel. Nifty! * Then we don't need to install uuidgen * Try also implementing a docgen step for nightly testing * Cut off the output after 9k bytes, otherwise Zulip complains * Fixes * chore: bump to nightly-2025-08-19 * Filter out the build progress lines. * Switch `doc-gen4` version to "main", otherwise it complains there is no nightly-testing release. * lake update * cleanup imports * Fix `git remote` complaining that `nightly-testing` already exists. * Fix error message. * fix tests * shake --fix * satisfy actionlint * shellcheck --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.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: 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: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
The old one was a syntax error and would've found a
mathlib4-nightly-testingremote as amathlib4remote (due to substring); this one is a bit more strict and works at least on my machine :-)