feat: high-level order typeclasses by datokrat · Pull Request #9729 · leanprover/lean4

datokrat · 2025-08-05T12:47:57Z

This PR introduces a canonical way to endow a type with an order structure. The basic operations (LE, LT, Min, Max, and in later PRs BEq, Ord, ...) and any higher-level property (a preorder, a partial order, a linear order etc.) are then put in relation to LE as necessary. The PR provides IsLinearOrder instances for many core types and updates the signatures of some lemmas.

BREAKING CHANGES:

The requirements of the lt_of_le_of_lt/le_trans lemmas for Vector, List and Array are simplified. They now require an IsLinearOrder instance. The new requirements are logically equivalent to the old ones, but the IsLinearOrder instance is not automatically inferred from the smaller typeclasses.
Hypotheses of type Std.Total (¬ · < · : α → α → Prop) are replaced with the equivalent class Std.Asymm (· < · : α → α → Prop). Breakage should be limited because there is now an instance that derives the latter from the former.
In Init.Data.List.MinMax, multiple theorem signatures are modified, replacing explicit parameters for antisymmetry, totality, min_ex_or etc. with corresponding instance parameters.

datokrat · 2025-08-05T13:13:01Z

!bench

ghost · 2025-08-05T13:34:26Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 09e8079ea3a7dd9a57cae5b417c7f2d84c8fcb81 --onto c260435913353a138e3d463b533d1449de0d0062. You can force Mathlib CI using the force-mathlib-ci label. (2025-08-05 13:34:26)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ed860dfa23acab2178686d85f463101f5adbddf1 --onto c260435913353a138e3d463b533d1449de0d0062. You can force Mathlib CI using the force-mathlib-ci label. (2025-08-05 20:39:11)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ed860dfa23acab2178686d85f463101f5adbddf1 --onto 12cd4ca7423119c116dcef78d5ae972d44f8af47. You can force Mathlib CI using the force-mathlib-ci label. (2025-08-06 07:30:33)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ed860dfa23acab2178686d85f463101f5adbddf1 --onto d5e19f9b288abe7e2c1ed359fb026ed9ae83f6e0. You can force Mathlib CI using the force-mathlib-ci label. (2025-08-08 13:16:24)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f15d531acbc1ba972d88fff2e0557590b20c0ef2 --onto 544f9912b70df75511e73eaef1f57573bf92b351. You can force Mathlib CI using the force-mathlib-ci label. (2025-08-11 08:48:48)
Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f15d531acbc1ba972d88fff2e0557590b20c0ef2 --onto e0fcaf5e7ddab2fcab51be8c403446d84a8a0d45. (2025-08-11 11:40:11)
💥 Mathlib branch lean-pr-testing-9729 build failed against this PR. (2025-08-11 11:54:27) View Log
✅ Mathlib branch lean-pr-testing-9729 has successfully built against this PR. (2025-08-11 13:06:43) View Log

leanprover-bot · 2025-08-05T13:34:28Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 09e8079ea3a7dd9a57cae5b417c7f2d84c8fcb81 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-08-05 13:34:27)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ed860dfa23acab2178686d85f463101f5adbddf1 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-08-05 20:39:13)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase f15d531acbc1ba972d88fff2e0557590b20c0ef2 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-08-11 08:48:49)

leanprover-bot · 2025-08-05T14:53:00Z

Here are the benchmark results for commit 8073e81.Found no runs to compare against.

datokrat · 2025-08-05T14:57:37Z

Since the commit at the merge base has not been benchmarked so far, here's the comparison to the previous commit: https://speed.lean-lang.org/lean4/compare/bab50d33-13a1-40c4-85a0-fda5f93f8b22/to/8b0e8a4c-cd31-460c-a038-3a479367140d?hash1=b42a7780e2f284dc53956ada763bd1ba575ef670

datokrat · 2025-08-05T16:08:21Z

!bench

leanprover-bot · 2025-08-05T17:30:37Z

Here are the benchmark results for commit 057efbc.
There were significant changes against commit ed860df:

  Benchmark                          Metric           Change
  ======================================================================
- big_match                          branch-misses      1.2%    (21.9 σ)
- big_omega.lean                     branches         202.5%  (4693.1 σ)
- big_omega.lean                     instructions     208.3%  (5382.5 σ)
- big_omega.lean                     maxrss            63.6%   (488.8 σ)
- big_omega.lean                     task-clock       217.3%   (437.9 σ)
- big_omega.lean                     wall-clock       214.6%   (490.3 σ)
- big_omega.lean MT                  branches         203.5%  (4625.8 σ)
- big_omega.lean MT                  instructions     208.8%  (5947.0 σ)
- big_omega.lean MT                  maxrss            63.1%   (289.4 σ)
- big_omega.lean MT                  task-clock       217.5%   (203.4 σ)
- big_omega.lean MT                  wall-clock       214.7%   (199.4 σ)
- channel.lean                       boundedn_seq       1.1%
- channel.lean                       unbounded_seq      1.1%
+ deriv                              task-clock        -1.8%   (-37.8 σ)
+ deriv                              wall-clock        -1.8%   (-48.9 σ)
+ lake build clean                   task-clock        -1.0%   (-25.3 σ)
- phashmap.lean                      eraseInsert        1.6%
+ qsort                              instructions      -3.4% (-2623.7 σ)
- stdlib                             congr simp thm     1.4%   (138.3 σ)
- treemap.lean                       iterate            8.1%
- workspaceSymbols with new ranges   branch-misses      1.3%    (26.1 σ)

datokrat · 2025-08-05T19:58:22Z

!bench

leanprover-bot · 2025-08-05T20:39:33Z

Here are the benchmark results for commit 55d6e30.
There were significant changes against commit ed860df:

  Benchmark                 Metric                 Change
  ===================================================================
- Init size                 bytes .olean.private     1.2%
- big_omega.lean            branches                 7.0%   (624.9 σ)
- big_omega.lean            instructions             7.2%   (880.8 σ)
- big_omega.lean MT         branches                 7.0%  (1034.8 σ)
- big_omega.lean MT         instructions             7.2%  (2224.2 σ)
- channel.lean              unbounded_seq            1.1%
+ omega_stress.lean async   branches                -1.9%   (-86.9 σ)
+ omega_stress.lean async   instructions            -2.0%   (-72.7 σ)
+ qsort                     instructions            -3.4% (-3415.8 σ)

datokrat · 2025-08-05T20:48:46Z

Note: The last benchmark was obtained after basing this PR on the PR stabilizing omega's performance (#9723). The 7% slowdown of the big_omega.lean benchmark is inherited from there.

src/Init/Data/List/Lex.lean

src/Init/Data/Order/Classes.lean

src/Init/Data/Order/Factories.lean

src/Init/Data/Order/Lemmas.lean

src/Init/Data/SInt/Lemmas.lean

src/Init/Data/Order/Factories.lean

src/Init/Data/BitVec/Lemmas.lean

src/Init/Data/Order/Subtype.lean

src/Init/Data/UInt/Basic.lean

src/Std/Data/Internal/List/Associative.lean

datokrat · 2025-08-11T08:05:22Z

!bench

leanprover-bot · 2025-08-11T09:02:21Z

Here are the benchmark results for commit a7e7d4c.
There were significant changes against commit f15d531:

  Benchmark        Metric                       Change
  ==============================================================
- binarytrees      maxrss                         2.8% (178.7 σ)
- riscv-ast.lean   wall-clock                     4.4%  (29.9 σ)
+ stdlib           compilation (LCNF mono)       -1.1% (-56.0 σ)
+ stdlib           grind canon                   -2.4% (-35.3 σ)
+ stdlib           let-to-have transformation    -2.8% (-25.7 σ)
+ stdlib           type checking                 -1.2% (-24.9 σ)

This PR is initially motivated by noticing `Lean.Grind.Preorder.toLE` appearing in long Mathlib typeclass searches; this change will prevent these searches. These changes are also helpful preparation for potentially dropping the custom `Lean.Grind.*` typeclasses, and unifying with the new typeclasses introduced in #9729.

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

* 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 * Update lean-toolchain for testing leanprover/lean4#9915 * fix tests * fix * 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). * fix * chore: bump to nightly-2025-08-16 * bump proofwidgets * bump proofwidgets * Update lean-toolchain for testing leanprover/lean4#9942 * fix: namespace linter should not care about private names * 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#9915 * 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 * fix * fix test * chore: bump to nightly-2025-08-18 * Update lean-toolchain for leanprover/lean4#9915 * 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 * Update lean-toolchain for leanprover/lean4#9915 * Filter out the build progress lines. * Switch `doc-gen4` version to "main", otherwise it complains there is no nightly-testing release. * Update lean-toolchain for leanprover/lean4#9915 * lake update * cleanup imports * Fix `git remote` complaining that `nightly-testing` already exists. * Fix error message. * Update lean-toolchain for leanprover/lean4#9915 * fix tests * shake --fix * fix says * . * says * chore: `curl --retry-all-errors` in `cache get` * remove says * chore: bump to nightly-2025-08-20 * Drop more noise from the grind report. * lake update * fix * fix tests * manual shake * chore: adaptations for nightly-2025-08-20 * 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: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Mac Malone <tydeu@hatpress.net> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

* 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 * Update lean-toolchain for testing leanprover/lean4#9915 * fix tests * fix * 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). * fix * chore: bump to nightly-2025-08-16 * bump proofwidgets * bump proofwidgets * Update lean-toolchain for testing leanprover/lean4#9942 * fix: namespace linter should not care about private names * 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#9915 * 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 * fix * fix test * chore: bump to nightly-2025-08-18 * Update lean-toolchain for leanprover/lean4#9915 * 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 * Update lean-toolchain for leanprover/lean4#9915 * Filter out the build progress lines. * Switch `doc-gen4` version to "main", otherwise it complains there is no nightly-testing release. * Update lean-toolchain for leanprover/lean4#9915 * lake update * cleanup imports * Fix `git remote` complaining that `nightly-testing` already exists. * Fix error message. * Update lean-toolchain for leanprover/lean4#9915 * fix tests * shake --fix * fix says * . * says * chore: `curl --retry-all-errors` in `cache get` * remove says * chore: bump to nightly-2025-08-20 * Drop more noise from the grind report. * lake update * fix * fix tests * manual shake * chore: adaptations for nightly-2025-08-20 * chore: bump to nightly-2025-08-21 * chore: adaptations for nightly-2025-08-21 * 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: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Mac Malone <tydeu@hatpress.net> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

* 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 * Update lean-toolchain for testing leanprover/lean4#9915 * fix tests * fix * 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). * fix * chore: bump to nightly-2025-08-16 * bump proofwidgets * bump proofwidgets * Update lean-toolchain for testing leanprover/lean4#9942 * fix: namespace linter should not care about private names * 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#9915 * 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 * fix * fix test * chore: bump to nightly-2025-08-18 * Update lean-toolchain for leanprover/lean4#9915 * 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 * Update lean-toolchain for leanprover/lean4#9915 * Filter out the build progress lines. * Switch `doc-gen4` version to "main", otherwise it complains there is no nightly-testing release. * Update lean-toolchain for leanprover/lean4#9915 * lake update * cleanup imports * Fix `git remote` complaining that `nightly-testing` already exists. * Fix error message. * Update lean-toolchain for leanprover/lean4#9915 * fix tests * shake --fix * fix says * . * says * chore: `curl --retry-all-errors` in `cache get` * remove says * chore: bump to nightly-2025-08-20 * Drop more noise from the grind report. * lake update * fix * fix tests * manual shake * chore: adaptations for nightly-2025-08-20 * chore: bump to nightly-2025-08-21 * chore: adaptations for nightly-2025-08-21 * feat: create `nightly-testing-daily` and `nightly-testing-green` branches These two branches track the `nightly-testing-YYYY-MM-DD` tags and the latest successfully built `nightly-testing` commit, respectively. These can then be used for other CI actions such as tests that run every night. * chore: bump to nightly-2025-08-22 * Switch the workflows over to nightly-testing-green branch * chore: bump to nightly-2025-08-23 * chore: bump to nightly-2025-08-24 * satisfy actionlint * shellcheck * fix * fix * fix for nightly-2025-08-24 (#42) * fix * please rebuild yourself * maybe that works? * fix * rat fixes * fixes * fixes * fix * .' * fix * not there yet * comment out Int.shiftLeft_add' * Revert "comment out Int.shiftLeft_add'" This reverts commit b33c9d7. * fix proof * change Polynomial.eval signature * workaround for initialization order issue * fixes * fix * fix message * Actually import the linters we want to run. * chore: bump to nightly-2025-08-25 * remove upstream `Rat` material * fix `sigmaProdDistrib` * more `Rat` fixes * `Rat.inv_def'` -> `Rat.inv_def` * fixes * comment out `rw_search` tests * small test fix * shake --fix * Revert --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Mac Malone <tydeu@hatpress.net> Co-authored-by: github-actions <github-actions@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: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Rob23oba <robin.arnez@web.de>

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

datokrat force-pushed the paul/order/draft3 branch from 8073e81 to 057efbc Compare August 5, 2025 15:33

datokrat force-pushed the paul/order/draft3 branch from 057efbc to 55d6e30 Compare August 5, 2025 19:57

datokrat changed the base branch from master to paul/base/order/draft3 August 5, 2025 20:46

datokrat marked this pull request as ready for review August 5, 2025 20:49

datokrat requested review from TwoFX and kim-em as code owners August 5, 2025 20:49

datokrat added the changelog-library Library label Aug 5, 2025

TwoFX reviewed Aug 8, 2025

View reviewed changes

datokrat requested a review from hargoniX as a code owner August 8, 2025 21:41

datokrat added 9 commits August 11, 2025 09:59

wip

e35ac4b

migrate min?_eq_some_iff

21131ec

fill sorry

a74e744

wip

dce2a74

cleanups

fd6d41a

implement the min?_eq_some_iff legacy lemma

358d31d

max lemmas

892bc61

fix errors

9863bcd

work on lex

7a87784

fix imports

a7e7d4c

datokrat force-pushed the paul/base/order/draft3 branch from 1559cd4 to f15d531 Compare August 11, 2025 08:03

datokrat force-pushed the paul/order/draft3 branch from 29d4f4e to a7e7d4c Compare August 11, 2025 08:03

fix docstrings

723bd4b

datokrat marked this pull request as draft August 11, 2025 09:28

datokrat added 4 commits August 11, 2025 11:28

Use LE instead of OrderData

ff81880

update docstrings

94e4b78

extract antisymmetry of subtype

37ba86b

fix a docstring

59e1607

datokrat added the force-mathlib-ci label Aug 11, 2025

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

Update lean-toolchain for testing leanprover/lean4#9729

5b66d06

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

Update lean-toolchain for testing leanprover/lean4#9729

fb46de9

ghost added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Aug 11, 2025

datokrat marked this pull request as ready for review August 11, 2025 13:56

datokrat changed the base branch from paul/base/order/draft3 to master August 11, 2025 14:54

datokrat added this pull request to the merge queue Aug 11, 2025

Merged via the queue into master with commit 0725349 Aug 11, 2025
41 checks passed

kim-em mentioned this pull request Aug 13, 2025

feat: make Lean.Grind.Preorder a mixin #9885

Merged

Conversation

datokrat commented Aug 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

datokrat commented Aug 5, 2025

Uh oh!

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

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

leanprover-bot commented Aug 5, 2025

Uh oh!

datokrat commented Aug 5, 2025

Uh oh!

datokrat commented Aug 5, 2025

Uh oh!

leanprover-bot commented Aug 5, 2025

Uh oh!

datokrat commented Aug 5, 2025

Uh oh!

leanprover-bot commented Aug 5, 2025

Uh oh!

datokrat commented Aug 5, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

datokrat commented Aug 11, 2025

Uh oh!

leanprover-bot commented Aug 11, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

datokrat commented Aug 5, 2025 •

edited

Loading

ghost commented Aug 5, 2025 •

edited by ghost

Loading

leanprover-bot commented Aug 5, 2025 •

edited

Loading