[Merged by Bors] - chore: bump toolchain to v4.30.0-rc1#37564
Closed
[Merged by Bors] - chore: bump toolchain to v4.30.0-rc1#37564
Conversation
Contributor
Garmelon
commented
Apr 2, 2026
Garmelon
commented
* fix_backward_defeq script * lake update batteries * non-local set_option, added manually * manual fixes, script confused by absence of blank lines * times out without manual fix * norm_num tests * reduce_mod_char * fix test output * set_option globally in RingTheory.SimpleModule.Isotypic * set_option globally in RingTheory.Adjoin.Dimension * set_option a section of LinearAlgebra.FiniteDimensional.Basic * set_option globally in Algebra.Homology.BifunctorAssociator * set_option in section in Algebra.Homology.BifunctorHomotopy * set_option globally in Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances * set_option globally in Algebra.Homology.BifunctorShift * set_option in section in Geometry.Manifold.Riemannian.Basic * set_option in section in NumberTheoryCyclotomic.Basic * set_option in section in Analysis.Distribution.SchwartzSpace.Fourier * global set_option in RingTheory.DedekindDomain.LinearDisjoint * manual fixes for CategoryTheory.Monoidal.DayConvolution.Closed * manual fixes for CategoryTheory.Sites.Descent.IsStack * manual fixes for Algebra.Homology.DifferentialObject * manual fixes for Geometry.RingedSpace.PresheafedSpace * manual fixes for CategoryTheory.Triangulated.Opposite.Functor * manual fixes in Algebra.Homology.HomotopyCategory.ShortExact * manual fixes for Geometry.RingedSpace.PresheafedSpace.Gluing Co-Authored-By: Claude Opus 4.6 <[email protected]> * manual fixes to CategoryTheory.Sites.Descent.DescentData * manual fixes, script confused by absence of blank lines, and a module-doc that should have been a doc-string * adaptation_note * x: ./fix_backward_defeq.py * x: ./fix_backward_defeq.py * set_option linter.style.longFile * remove unused simp args * remove noop tactic * lake update * optimistic linter fixes * patch and adaptation note * slightly more care with the linter * still getting it right * fix test * chore: adaptations for nightly-2026-02-16-rev1 * fix lakefile and manifest * remove fix_backward_defeq.py --------- Co-authored-by: Claude Opus 4.6 <[email protected]>
kim-em
reviewed
Apr 3, 2026
kim-em
reviewed
Apr 3, 2026
sgouezel
reviewed
Apr 3, 2026
sgouezel
reviewed
Apr 3, 2026
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
Outdated
Show resolved
Hide resolved
Contributor
|
Could you run the script removing unneeded backward options? I noticed a few of them browsing quickly through the files. The |
Contributor
|
bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Apr 4, 2026
Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Robin Arnez <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Joscha <[email protected]> Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com>
Contributor
|
Pull request successfully merged into master. Build succeeded:
|
mathlib-bors
bot
changed the title
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
11 participants
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.