[Merged by Bors] - chore: adaptations for nightly-2025-09-17 #68
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…hlib4-nightly-testing into nightly-testing
* 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>
Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Mac Malone <mac@lean-fro.org>
|
bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Sep 18, 2025
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com>
|
Pull request successfully merged into bump/v4.25.0. Build succeeded: |
mathlib-bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.