chore: adaptations for nightly-2026-02-19#184
Closed
mathlib-nightly-testing[bot] wants to merge 10000 commits intobump/v4.30.0from
Closed
chore: adaptations for nightly-2026-02-19#184mathlib-nightly-testing[bot] wants to merge 10000 commits intobump/v4.30.0from
mathlib-nightly-testing[bot] wants to merge 10000 commits intobump/v4.30.0from
Conversation
…2-02 chore: adaptations for nightly-2026-02-02
🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
…into nightly-testing
* 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 <noreply@anthropic.com> * 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 <noreply@anthropic.com>
Rename instanceReducible to implicitReducible (lean4#12529). Update batteries for upstreamed List.scanl/scanr (lean4#12452) and Nat.Digits (lean4#12445).
Commit Verification SummaryWarning Some verifications failed. See details below. Commits to Review (12076)
|
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
6 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.
No description provided.