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

* chore: bump to nightly-2025-08-14

* adaptation note about grind regression

* Update lean-toolchain for testing leanprover/lean4#9915

* fix tests

* fix

* Update lean-toolchain for testing leanprover/lean4#9918

* Update 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).

* 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

* Move docgen reports to a different Zulip stream

* chore: adaptations for nightly-2025-08-25

* Fix `git checkout` not restoring the right version of the lakefile

* Fix name of mathlib dependency

* chore: bump to nightly-2025-08-26

* addSuggestionCore

* lake update

* chore: adapt `to_additive` to lean4#9966 (#45)

* lake update

* chore: Lean.Grind order structures replaced with Std versions

* ibid

* fixes

* comment out UInt theorems

* Bump batteries

* chore: adapt `hint` tactic to lean4#9966 (#46)

* chore: adapt Hint to lean4#9966

* space after emoji

* rework how `hint` finds try this suggestions

* fix tests

* docstring and formatting

* indentation

* chore: bump to nightly-2025-08-27

* TMToPartrec relies on a default value

oops

* lake update

* fix try this output in tests

* fix uint

* chore: adaptations for nightly-2025-08-27

* fix

* wrong toolchain??

* lake update

* fix merge

* fix merge

* revert sqrt changes

* ugh

* fix from nightly-testing

* fix test

* note about test

* .

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

* 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

* Move docgen reports to a different Zulip stream

* chore: adaptations for nightly-2025-08-25

* Fix `git checkout` not restoring the right version of the lakefile

* Fix name of mathlib dependency

* chore: bump to nightly-2025-08-26

* addSuggestionCore

* lake update

* chore: adapt `to_additive` to lean4#9966 (#45)

* lake update

* chore: Lean.Grind order structures replaced with Std versions

* ibid

* fixes

* comment out UInt theorems

* Bump batteries

* chore: adapt `hint` tactic to lean4#9966 (#46)

* chore: adapt Hint to lean4#9966

* space after emoji

* rework how `hint` finds try this suggestions

* fix tests

* docstring and formatting

* indentation

* chore: bump to nightly-2025-08-27

* TMToPartrec relies on a default value

oops

* lake update

* fix try this output in tests

* fix uint

* chore: adaptations for nightly-2025-08-27

* toolchain got reverted??

* merge lean-pr-testing-9918

* fix

* wrong toolchain??

* lake update

* field_simp Nat Int multiplication issue

* fixes to hint file after field_simp refactor

* fix refs + add adaptation note

* actually fix reassoc

* fix warnings

* oops

* chore: bump to nightly-2025-08-29

* lake exe shake --update

* restore Mathlib.Data.Seq.Basic from upstream

* chore: bump to nightly-2025-08-30

* lake update batteries

* fix

* fix merge

* fix merge

* revert sqrt changes

* ugh

* fix from nightly-testing

* fix merge

* fix test

* note about test

* .

* fix

* mk_all

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

* 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

* Move docgen reports to a different Zulip stream

* chore: adaptations for nightly-2025-08-25

* Fix `git checkout` not restoring the right version of the lakefile

* Fix name of mathlib dependency

* chore: bump to nightly-2025-08-26

* addSuggestionCore

* lake update

* chore: adapt `to_additive` to lean4#9966 (#45)

* lake update

* chore: Lean.Grind order structures replaced with Std versions

* ibid

* fixes

* comment out UInt theorems

* Bump batteries

* chore: adapt `hint` tactic to lean4#9966 (#46)

* chore: adapt Hint to lean4#9966

* space after emoji

* rework how `hint` finds try this suggestions

* fix tests

* docstring and formatting

* indentation

* chore: bump to nightly-2025-08-27

* TMToPartrec relies on a default value

oops

* lake update

* fix try this output in tests

* fix uint

* chore: adaptations for nightly-2025-08-27

* toolchain got reverted??

* merge lean-pr-testing-9918

* fix

* wrong toolchain??

* lake update

* field_simp Nat Int multiplication issue

* fixes to hint file after field_simp refactor

* fix refs + add adaptation note

* actually fix reassoc

* fix warnings

* oops

* chore: bump to nightly-2025-08-29

* lake exe shake --update

* restore Mathlib.Data.Seq.Basic from upstream

* chore: bump to nightly-2025-08-30

* Merge master into nightly-testing

* chore: bump to nightly-2025-08-31

* lake update batteries

* fix

* bump toolchain

* chore: adaptations for nightly-2025-08-31

* fix merge

* fix merge

* revert sqrt changes

* ugh

* fix from nightly-testing

* fix merge

* fix test

* note about test

* .

* fix

---------

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

…over-community#34568)

The script now checks for labels only the lines starting with `::notice::`.  This avoid matching the `::warning::` lines, which highlight gaps in the directory coverage of `lake exe autolabel`.

[#mathlib4 > Mathlib/* labels @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.2F*.20labels/near/569988520)

[#Is there code for X? > a &#42; b < a &#42; c and b < c implies 0 < a](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/a.20*.20b.20.3C.20a.20*.20c.20and.20b.20.3C.20c.20implies.200.20.3C.20a/with/573860260)