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