feat: make cdot expansion take hygiene into account by kmill · Pull Request #9443 · leanprover/lean4

kmill · 2025-07-20T17:49:00Z

This PR makes cdot function expansion take hygiene information into account, fixing "parenthesis capturing" errors that can make erroneous cdots trigger cdot expansion in conjunction with macros. For example, given

macro "baz% " t:term : term => `(1 + ($t))

it used to be that baz% · would expand to 1 + fun x => x, but now the parentheses in ($t) do not capture the cdot. We also fix an oversight where cdot function expansion ignored the fact that type ascriptions and tuples were supposed to delimit expansion, and also now the quotation prechecker ignores the identifier in hygieneInfo. (#9491 added the hygiene information to the parenthesis and cdot syntaxes.)

This fixes a bug discovered by Google DeepMind, which made use of useλy . x=>y.rec λS p=>?_. The use tactic from Mathlib wrapped the provided term in a type ascription, and so this was equivalent to use fun x => λy x x=>y.rec λS p=>?_. (Note that cdot function expansion is not able to take into account where the cdots are located, and it is syntactically valid to insert an identifier into the binder list like this. If we ever want to address this in the future, we could have cdots expand into a special term that wraps an identifier that evaluates to a local, but which would cause errors in other contexts.)

Design note: we put the hygieneInfo on the open parenthesis rather than at the end, since that way the hygiene information is available even when there are parsing errors. This is important since we rely on being able to elaborate partial syntax to get elab info (e.g. in (a. to get completion info). Note that syntax matchers check that the hygieneInfo is actually present, so such partial syntax would not be matched.

eric-wieser · 2025-07-20T18:41:07Z

This fixes a bug discovered by Google DeepMind, which made use of useλy . x=>y.rec λS p=>?_.

Perhaps worth noting that this is already fixed in the use tactic, and that this is more about a mechanism to make such mistakes impossible in other tactics.

src/Lean/Elab/BuiltinNotation.lean

kmill · 2025-07-20T18:43:42Z

I'm aware that you fixed use already @eric-wieser (thanks!). I've changed a sentence in the summary to use the past tense.

leanprover-bot · 2025-07-21T03:45:15Z

Reference manual CI status:

❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-07-18 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-21 03:45:14)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9d93b10919ba21cbc2855b73d2d2302567bb9fd8 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-23 22:40:04)

ghost · 2025-07-21T03:51:18Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-9443 build failed against this PR. (2025-07-21 03:51:16) View Log
❌ Mathlib branch lean-pr-testing-9443 built against this PR, but testing failed. (2025-07-21 05:28:13) View Log
✅ Mathlib branch lean-pr-testing-9443 has successfully built against this PR. (2025-07-22 01:37:55) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9d93b10919ba21cbc2855b73d2d2302567bb9fd8 --onto cdab726e3d289b80860ae9f5a7de21d990c8b95f. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-23 22:40:02)

This PR adds hygiene info to paren/tuple/typeAscription syntaxes, which will be used to implement hygienic cdot function expansion in leanprover#9443.

This PR adds hygiene info to paren/tuple/typeAscription syntaxes, which will be used to implement hygienic cdot function expansion in #9443.

This PR makes cdot function expansion take hygiene information into account, fixing "parenthesis capturing" errors that affect cdot functions in macros. For example, given ```lean macro "baz% " t:term : term => `(1 + ($t)) ``` it used to be that `baz% ·` would expand to `1 + fun x => x`, but now the parentheses in `($t)` do not capture the cdot. We also fix a bug where cdot function expansion ignored the fact that type ascriptions and tuples were supposed to delimit expansion.

* Update lean-toolchain for testing leanprover/lean4#9084 * Update lean-toolchain for leanprover/lean4#9084 * Update lean-toolchain for testing leanprover/lean4#9423 * Update lean-toolchain for testing leanprover/lean4#9424 * chore: update 'unknown identifier' test ouputs * chore: update 'tactic failed' test outputs * fix(scripts/create-adaptation-pr): improve find_remote (leanprover-community#26974) The old one was a syntax error and would've found a `mathlib4-nightly-testing` remote as a `mathlib4` remote (due to substring); this one is a bit more strict and works at least on my machine :-) * Merge master into nightly-testing * Update lean-toolchain for leanprover/lean4#9423 * Update lean-toolchain for leanprover/lean4#9424 * chore: update tactic error test outputs * Update lean-toolchain for leanprover/lean4#9423 * Merge master into nightly-testing * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#9443 * fixes * fixes * Merge master into nightly-testing * Merge master into nightly-testing * fix * chore: bump to nightly-2025-07-22 * Merge master into nightly-testing * adaptation notes for breakages in batteries * update Cache * fix * lake update * Merge master into nightly-testing * deprecation * fixes for Shake * shake * shake --update * fix noisy build detection * Merge master into nightly-testing * chore: bump to nightly-2025-07-23 * Merge master into nightly-testing * Merge master into nightly-testing * fix * revert commenting out * fix noisy test * Merge master into nightly-testing * Merge master into nightly-testing * chore: bump to nightly-2025-07-24 * Merge master into nightly-testing * Merge master into nightly-testing * Merge master into nightly-testing * fixes for changes to Lean.Grind.NatModule * oops * Merge master into nightly-testing * chore: bump to nightly-2025-07-25 * fix * fix(scripts/create-adaption-pr.sh): fetch `master` if necessary (leanprover-community#27293) Makes sure that `master` is available, in particular when the remote has been automatically added. * chore: make create-adapation-pr.sh robust to running on nightly-testing fork (leanprover-community#27411) cf recent failures at [#nightly-testing > Mathlib bump branch reminders @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20bump.20branch.20reminders/near/530460702) * fix da script * `lake exe mk_all` * hmm let's see what breaks * not these * hmm..? * hmm this one as well * more changes that turn out to be necessary * Restore files from testing/nightly-testing * Restore files from testing/nightly-testing * Restore files from testing/nightly-testing * Revert accidentals * `mk_all` * fix `@[to_additive]` * Restore files from testing/nightly-testing * re-add changes * restore some more stuff carefully * these * try fix things * chore: bump to nightly-2025-07-26 * fix by restoring mathlib change * restore master versions of mis-merged files * restore master versions of mis-merged files * fix merge * comment out with adaptation note * huh? * lake update * lake update * fix import * shaking * shaking * shaking * chore: bump to nightly-2025-07-27 * lake update * mk_all * fix merges * more missed changes (#18) * Merge master into nightly-testing * feat: establish examples of harmonic functions (leanprover-community#26844) If `f : ℂ → F` is complex-differentiable, then show that `f` is harmonic. If `F = ℂ`, then so is its real part, imaginary part, and complex conjugate. If `f` has no zero, then `log ‖f‖` is harmonic. This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. It is one of the ingredients in the proof of Jensen's Formula in complex analysis. * chore: replace `Monoid.IsTorsionFree` with `IsMulTorsionFree` (leanprover-community#24311) From Toric * fix tests --------- Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> * fix test (#19) * last fix I swear * unnecessary duplicate imports * these are actual unused imports (because of core changes?) * test fix * chore: adaptations for nightly-2025-07-27 * chore: bump to nightly-2025-07-28 * grind lemma * more * chore(Cache): enable FRO cache (#17) * chore: revert "enable FRO cache (#17)" This reverts commit 1da13d9. * Restore regression * chore: adaptations for nightly-2025-07-28 * chore: adaptations for nightly-2025-07-28 * chore: adaptations for nightly-2025-07-28 * chore: adaptations for nightly-2025-07-28 * adaptation notes * chore: bump to nightly-2025-07-29 * chore: adaptations for nightly-2025-07-29 --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Mac Malone <tydeu@hatpress.net> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>

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

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

kmill added the changelog-language Language features and metaprograms label Jul 20, 2025

eric-wieser reviewed Jul 20, 2025

View reviewed changes

src/Lean/Elab/BuiltinNotation.lean Outdated Show resolved Hide resolved

kmill force-pushed the kmill_cdot_hygienic branch from 89223d7 to 7682df2 Compare July 21, 2025 02:51

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

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

Update lean-toolchain for testing leanprover/lean4#9443

04dc5bb

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

Update lean-toolchain for testing leanprover/lean4#9443

05dbfe5

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

ghost added 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 Jul 22, 2025

kmill mentioned this pull request Jul 23, 2025

feat: add hygiene info to paren/tuple/typeAscription syntaxes #9491

Merged

kmill force-pushed the kmill_cdot_hygienic branch from 7682df2 to 6fb6edb Compare July 23, 2025 21:34

kmill force-pushed the kmill_cdot_hygienic branch from 6fb6edb to a6d82c8 Compare July 23, 2025 21:50

kmill added this pull request to the merge queue Jul 23, 2025

github-merge-queue bot removed this pull request from the merge queue due to failed status checks Jul 23, 2025

fix

4617921

kmill requested a review from kim-em as a code owner July 24, 2025 00:31

kmill enabled auto-merge July 24, 2025 00:31

kmill added this pull request to the merge queue Jul 24, 2025

auto-merge was automatically disabled July 24, 2025 00:53
Pull Request is not mergeable

Merged via the queue into leanprover:master with commit d45cc67 Jul 24, 2025
15 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: make cdot expansion take hygiene into account#9443

feat: make cdot expansion take hygiene into account#9443
kmill merged 2 commits intoleanprover:masterfrom
kmill:kmill_cdot_hygienic

kmill commented Jul 20, 2025 •

edited

Loading

Uh oh!

eric-wieser commented Jul 20, 2025

Uh oh!

Uh oh!

kmill commented Jul 20, 2025 •

edited

Loading

Uh oh!

leanprover-bot commented Jul 21, 2025 •

edited

Loading

Uh oh!

ghost commented Jul 21, 2025 •

edited by ghost

Loading

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

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

Uh oh!

Uh oh!

eric-wieser commented Jul 20, 2025

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

kmill commented Jul 20, 2025 •

edited

Loading

kmill commented Jul 20, 2025 •

edited

Loading

leanprover-bot commented Jul 21, 2025 •

edited

Loading

ghost commented Jul 21, 2025 •

edited by ghost

Loading