perf: clarify and granularize access to async env ext state by Kha · Pull Request #9587 · leanprover/lean4

Kha · 2025-07-28T08:30:45Z

Have asynchronous environment extensions specify whether they are manipulate data for declarations from the "outside"/main branch (e.g. attributes) or from the "inside"/async branch (e.g. data collected from body elaboration) in order to avoid unnecessary waiting.
Merge findStateAsync? into getState via a new, optional asyncDecl parameter.
Make mayContainAsync check an automatic part of modifyState.

Kha · 2025-07-28T08:30:57Z

!bench

leanprover-bot · 2025-07-28T09:10:22Z

Here are the benchmark results for commit 1f05cbc.
There were significant changes against commit 95e753c:

  Benchmark                              Metric                      Change
  =====================================================================================
- Init.Data.BitVec.Lemmas                wall-clock                   53.2%   (121.2 σ)
- Init.Data.BitVec.Lemmas re-elab        maxrss                        4.6%    (31.9 σ)
- Init.Data.List.Sublist async           wall-clock                   28.7%    (31.2 σ)
- Init.Prelude async                     branches                      1.5%    (50.2 σ)
- Init.Prelude async                     instructions                  1.3%    (38.0 σ)
- Std.Data.DHashMap.Internal.RawLemmas   branch-misses                 2.4%    (23.3 σ)
- Std.Data.DHashMap.Internal.RawLemmas   wall-clock                   58.5%    (23.5 σ)
- Std.Data.Internal.List.Associative     branch-misses                 7.5%    (53.8 σ)
- Std.Data.Internal.List.Associative     branches                      1.9%   (107.0 σ)
- Std.Data.Internal.List.Associative     instructions                  2.0%    (97.1 σ)
- Std.Data.Internal.List.Associative     wall-clock                   94.8%   (105.8 σ)
- grind_bitvec2.lean                     branch-misses                 8.3%    (22.8 σ)
- grind_bitvec2.lean                     branches                      1.6%    (34.6 σ)
- grind_bitvec2.lean                     instructions                  1.7%    (35.0 σ)
- grind_bitvec2.lean                     maxrss                       22.4%    (34.7 σ)
+ grind_bitvec2.lean                     task-clock                  -19.8%   (-64.1 σ)
- grind_bitvec2.lean                     wall-clock                  167.7%   (217.2 σ)
- grind_list2.lean                       branch-misses                 9.4%    (32.3 σ)
- grind_list2.lean                       branches                      1.6%    (42.9 σ)
- grind_list2.lean                       instructions                  1.7%    (42.2 σ)
- grind_list2.lean                       wall-clock                   50.2%    (92.5 σ)
- identifier auto-completion             branches                      8.9%   (680.1 σ)
- identifier auto-completion             instructions                  7.8%   (573.0 σ)
- simp_bubblesort_256                    branches                      1.0%    (31.5 σ)
- simp_congr                             wall-clock                   33.0%    (22.7 σ)
- simp_subexpr                           branches                      1.0%    (26.0 σ)
+ stdlib                                 blocked                     -99.4% (-4956.8 σ)
- stdlib                                 blocked (unaccounted)       230.1%   (342.2 σ)
+ stdlib                                 congr simp thm              -13.2%   (-33.2 σ)
+ stdlib                                 dsimp                       -37.2%   (-38.3 σ)
+ stdlib                                 grind                       -24.3%   (-78.9 σ)
+ stdlib                                 grind canon                 -29.9%  (-116.7 σ)
+ stdlib                                 grind cutsat                -20.0%   (-20.3 σ)
+ stdlib                                 grind ematch                -18.2%  (-107.9 σ)
+ stdlib                                 grind mark subsingleton     -30.3%  (-852.6 σ)
+ stdlib                                 grind simp                  -27.9%  (-124.5 σ)
+ stdlib                                 grind typeclass inference   -24.7%  (-113.1 σ)
+ stdlib                                 tactic execution            -17.8%   (-33.5 σ)
+ stdlib                                 task-clock                   -4.0%   (-58.6 σ)
+ stdlib                                 type checking                -3.4%   (-23.5 σ)
- stdlib                                 wall-clock                   16.0%    (59.8 σ)

leanprover-bot · 2025-07-28T09:16:56Z

Reference manual CI status:

❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-07-27 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-07-28 09:16:55)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-07-31 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-07-31 12:51:38)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-08-02 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-08-02 12:55:54)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase d9956a9d0542f32f52e743dc14205d6f05dd266d --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-08-02 15:30:32)

ghost · 2025-07-28T09:21:42Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-9587 build failed against this PR. (2025-07-28 09:21:40) View Log
💥 Mathlib branch lean-pr-testing-9587 build failed against this PR. (2025-07-31 12:56:41) View Log
✅ Mathlib branch lean-pr-testing-9587 has successfully built against this PR. (2025-08-02 13:47:24) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d9956a9d0542f32f52e743dc14205d6f05dd266d --onto 08c3f3c2366db7000fd20267e84aeb6e06487323. You can force Mathlib CI using the force-mathlib-ci label. (2025-08-02 15:30:30)

Kha · 2025-07-28T10:17:01Z

!bench

leanprover-bot · 2025-07-28T10:17:49Z

Here are the benchmark results for commit 1f05cbc.
There were significant changes against commit 95e753c:

  Benchmark                              Metric                      Change
  =====================================================================================
- Init.Data.BitVec.Lemmas                wall-clock                   53.2%   (121.2 σ)
- Init.Data.BitVec.Lemmas re-elab        maxrss                        4.6%    (31.9 σ)
- Init.Data.List.Sublist async           wall-clock                   28.7%    (31.2 σ)
- Init.Prelude async                     branches                      1.5%    (50.2 σ)
- Init.Prelude async                     instructions                  1.3%    (38.0 σ)
- Std.Data.DHashMap.Internal.RawLemmas   branch-misses                 2.4%    (23.3 σ)
- Std.Data.DHashMap.Internal.RawLemmas   wall-clock                   58.5%    (23.5 σ)
- Std.Data.Internal.List.Associative     branch-misses                 7.5%    (53.8 σ)
- Std.Data.Internal.List.Associative     branches                      1.9%   (107.0 σ)
- Std.Data.Internal.List.Associative     instructions                  2.0%    (97.1 σ)
- Std.Data.Internal.List.Associative     wall-clock                   94.8%   (105.8 σ)
- grind_bitvec2.lean                     branch-misses                 8.3%    (22.8 σ)
- grind_bitvec2.lean                     branches                      1.6%    (34.6 σ)
- grind_bitvec2.lean                     instructions                  1.7%    (35.0 σ)
- grind_bitvec2.lean                     maxrss                       22.4%    (34.7 σ)
+ grind_bitvec2.lean                     task-clock                  -19.8%   (-64.1 σ)
- grind_bitvec2.lean                     wall-clock                  167.7%   (217.2 σ)
- grind_list2.lean                       branch-misses                 9.4%    (32.3 σ)
- grind_list2.lean                       branches                      1.6%    (42.9 σ)
- grind_list2.lean                       instructions                  1.7%    (42.2 σ)
- grind_list2.lean                       wall-clock                   50.2%    (92.5 σ)
- identifier auto-completion             branches                      8.9%   (680.1 σ)
- identifier auto-completion             instructions                  7.8%   (573.0 σ)
- simp_bubblesort_256                    branches                      1.0%    (31.5 σ)
- simp_congr                             wall-clock                   33.0%    (22.7 σ)
- simp_subexpr                           branches                      1.0%    (26.0 σ)
+ stdlib                                 blocked                     -99.4% (-4956.8 σ)
- stdlib                                 blocked (unaccounted)       230.1%   (342.2 σ)
+ stdlib                                 congr simp thm              -13.2%   (-33.2 σ)
+ stdlib                                 dsimp                       -37.2%   (-38.3 σ)
+ stdlib                                 grind                       -24.3%   (-78.9 σ)
+ stdlib                                 grind canon                 -29.9%  (-116.7 σ)
+ stdlib                                 grind cutsat                -20.0%   (-20.3 σ)
+ stdlib                                 grind ematch                -18.2%  (-107.9 σ)
+ stdlib                                 grind mark subsingleton     -30.3%  (-852.6 σ)
+ stdlib                                 grind simp                  -27.9%  (-124.5 σ)
+ stdlib                                 grind typeclass inference   -24.7%  (-113.1 σ)
+ stdlib                                 tactic execution            -17.8%   (-33.5 σ)
+ stdlib                                 task-clock                   -4.0%   (-58.6 σ)
+ stdlib                                 type checking                -3.4%   (-23.5 σ)
- stdlib                                 wall-clock                   16.0%    (59.8 σ)

Kha · 2025-07-28T10:23:32Z

!bench

leanprover-bot · 2025-07-28T10:30:15Z

Here are the benchmark results for commit 6f8cfe9.
The entire run failed.
Found no significant differences.

Kha · 2025-07-31T09:55:22Z

!bench

leanprover-bot · 2025-07-31T10:05:20Z

Here are the benchmark results for commit 49a8b1a.
The entire run failed.
Found no significant differences.

Kha · 2025-07-31T12:05:29Z

!bench

leanprover-bot · 2025-07-31T12:39:09Z

Here are the benchmark results for commit 21312f9.
There were significant changes against commit 3a3c816:

  Benchmark                              Metric                      Change
  ====================================================================================
- Init.Data.BitVec.Lemmas                task-clock                   22.3%   (40.2 σ)
+ Init.Data.BitVec.Lemmas                wall-clock                  -42.8%  (-89.1 σ)
+ Init.Data.List.Sublist async           wall-clock                  -30.2%  (-65.0 σ)
+ Std.Data.DHashMap.Internal.RawLemmas   wall-clock                  -16.1%  (-24.4 σ)
+ hashmap.lean                           containsHit                  -2.4%
+ hashmap.lean                           insertHit                    -2.8%
+ hashmap.lean                           insertIfNewHit               -4.8%
- identifier auto-completion             branches                      2.8%  (135.3 σ)
- identifier auto-completion             instructions                  2.7%  (112.8 σ)
+ stdlib                                 blocked (unaccounted)       -59.7% (-515.9 σ)
- stdlib                                 congr simp thm                9.9%   (35.3 σ)
- stdlib                                 grind typeclass inference     3.6%  (630.0 σ)
- stdlib                                 task-clock                    3.3%   (52.9 σ)
- stdlib                                 type checking                 6.0%   (60.7 σ)
+ tests/bench/ interpreted               task-clock                   -9.8%  (-34.3 σ)

Kha · 2025-08-01T15:24:50Z

!bench

ghost · 2025-08-01T17:21:26Z

✅ Mathlib branch lean-pr-testing-9587 has successfully built against this PR. (2025-08-01 17:21:23) View Log

Kha · 2025-08-02T11:28:02Z

!bench

Kha · 2025-08-02T12:10:19Z

!bench

leanprover-bot · 2025-08-02T12:46:17Z

Here are the benchmark results for commit b4c3119.
There were significant changes against commit 08c3f3c:

  Benchmark                      Metric                  Change
  ========================================================================
- Init.Data.BitVec.Lemmas        maxrss                   20.5%   (25.4 σ)
- Init.Data.BitVec.Lemmas        task-clock               25.3%   (24.2 σ)
+ Init.Data.BitVec.Lemmas        wall-clock              -42.1%  (-92.0 σ)
+ Init.Data.List.Sublist async   wall-clock              -17.2%  (-24.3 σ)
+ channel.lean                   boundedn_seq             -5.3%
+ channel.lean                   unbounded_seq            -6.9%
- identifier auto-completion     branches                  2.0%   (99.5 σ)
- identifier auto-completion     instructions              2.1%   (90.4 σ)
- mut_rec_wf                     task-clock                3.5%   (30.5 σ)
- mut_rec_wf                     wall-clock                3.5%   (30.8 σ)
+ rbmap_library                  maxrss                   -5.6%  (-29.5 σ)
- stdlib                         blocked                  54.8%   (52.1 σ)
- stdlib                         congr simp thm           11.2%   (25.9 σ)
+ stdlib                         grind simp               -3.7%  (-27.5 σ)
- stdlib                         tactic execution         11.1%   (51.5 σ)
- stdlib                         task-clock                3.8% (1156.3 σ)
- stdlib                         type checking             3.2%   (35.2 σ)
+ treemap.lean                   insertHit               -12.6%  (-46.8 σ)
+ treemap.lean                   insertRandomMissEmpty    -9.1%  (-34.6 σ)
+ treemap.lean                   iterate                  -4.0%
+ treemap.lean                   task-clock               -8.5%  (-29.8 σ)
+ treemap.lean                   wall-clock               -8.5%  (-29.5 σ)

Kha · 2025-08-02T14:45:51Z

!bench

leanprover-bot · 2025-08-02T15:36:54Z

Here are the benchmark results for commit 45543a3.
There were significant changes against commit d9956a9:

  Benchmark                    Metric           Change
  ===============================================================
- Init.Data.BitVec.Lemmas      task-clock        25.9%   (24.2 σ)
+ Init.Data.BitVec.Lemmas      wall-clock       -41.8% (-151.7 σ)
+ grind_bitvec2.lean           wall-clock        -4.2%  (-28.5 σ)
- identifier auto-completion   branches           2.0%   (92.8 σ)
- identifier auto-completion   instructions       2.1%  (103.5 σ)
- stdlib                       congr simp thm     8.8%   (53.4 σ)

* 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>

* 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>

* 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 * fix * 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 * empty commit * restore test --------- Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Mac Malone <tydeu@hatpress.net> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com> 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: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

* 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>

* 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>

Kha requested review from leodemoura and zwarich as code owners July 28, 2025 08:30

Kha marked this pull request as draft July 28, 2025 08:31

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jul 28, 2025

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Jul 28, 2025

Update lean-toolchain for testing leanprover/lean4#9587

7c12a14

ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 28, 2025

Update lean-toolchain for testing leanprover/lean4#9587

2547b65

ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jul 28, 2025

Kha force-pushed the push-mvvwkrwsmumm branch from 1f05cbc to 6f8cfe9 Compare July 28, 2025 10:23

Kha force-pushed the push-mvvwkrwsmumm branch 2 times, most recently from 6eb6715 to 49a8b1a Compare July 31, 2025 09:55

Kha force-pushed the push-mvvwkrwsmumm branch from 49a8b1a to 21312f9 Compare July 31, 2025 12:05

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Jul 31, 2025

Update lean-toolchain for leanprover/lean4#9587

59a9802

ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 31, 2025

Update lean-toolchain for leanprover/lean4#9587

486f6d4

Kha force-pushed the push-mvvwkrwsmumm branch from 21312f9 to c3988ed Compare August 1, 2025 15:18

Kha added the awaiting-mathlib We should not merge this until we have a successful Mathlib build label Aug 1, 2025

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Aug 1, 2025

Update lean-toolchain for leanprover/lean4#9587

3ae1680

ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Aug 1, 2025

Update lean-toolchain for leanprover/lean4#9587

add3190

Kha force-pushed the push-mvvwkrwsmumm branch from c3988ed to 4aebc3a Compare August 2, 2025 11:27

Kha force-pushed the push-mvvwkrwsmumm branch from 6712ee1 to b4c3119 Compare August 2, 2025 12:10

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Aug 2, 2025

Update lean-toolchain for leanprover/lean4#9587

77372d7

ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Aug 2, 2025

Update lean-toolchain for leanprover/lean4#9587

a6fe029

Kha added 6 commits August 2, 2025 16:45

perf: clarify and granularize access to async env ext state

2721db6

perf: restore previous fallthrough

4bb44ce

fix: escalate .mainEnv to .asyncEnv on realized consts

afca154

harden async modifyState

dce8b39

docs

66d313d

optimize common case in getStateImpl

45543a3

Kha force-pushed the push-mvvwkrwsmumm branch from b4c3119 to 45543a3 Compare August 2, 2025 14:45

Kha marked this pull request as ready for review August 2, 2025 17:01

Kha requested a review from tydeu as a code owner August 2, 2025 17:01

Kha enabled auto-merge August 2, 2025 17:01

Kha added this pull request to the merge queue Aug 2, 2025

Merged via the queue into leanprover:master with commit 1e83f62 Aug 2, 2025
18 checks passed

Kha deleted the push-mvvwkrwsmumm branch August 2, 2025 19:11

Conversation

Kha commented Jul 28, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Kha commented Jul 28, 2025

Uh oh!

leanprover-bot commented Jul 28, 2025

Uh oh!

leanprover-bot commented Jul 28, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ghost commented Jul 28, 2025 • edited by ghost Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Kha commented Jul 28, 2025

Uh oh!

leanprover-bot commented Jul 28, 2025

Uh oh!

Kha commented Jul 28, 2025

Uh oh!

leanprover-bot commented Jul 28, 2025

Uh oh!

Kha commented Jul 31, 2025

Uh oh!

leanprover-bot commented Jul 31, 2025

Uh oh!

Kha commented Jul 31, 2025

Uh oh!

leanprover-bot commented Jul 31, 2025

Uh oh!

Kha commented Aug 1, 2025

Uh oh!

ghost commented Aug 1, 2025

Uh oh!

Kha commented Aug 2, 2025

Uh oh!

Kha commented Aug 2, 2025

Uh oh!

leanprover-bot commented Aug 2, 2025

Uh oh!

Kha commented Aug 2, 2025

Uh oh!

leanprover-bot commented Aug 2, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Kha commented Jul 28, 2025 •

edited

Loading

leanprover-bot commented Jul 28, 2025 •

edited

Loading

ghost commented Jul 28, 2025 •

edited by ghost

Loading