[Merged by Bors] - chore: bump toolchain to v4.29.0-rc1#35459
Closed
[Merged by Bors] - chore: bump toolchain to v4.29.0-rc1#35459
Conversation
…1-05 chore: adaptations for nightly-2026-01-05
…1-06 chore: adaptations for nightly-2026-01-06
…1-07 chore: adaptations for nightly-2026-01-07
Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.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>
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>
* 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>
…_to_v4.29.0-rc1 # Conflicts: # lake-manifest.json # lakefile.lean # lean-toolchain
Contributor
Author
|
bors p=20 |
kim-em
added
the
auto-merge-after-CI
Contributor
Author
|
bors p=10 |
PR summary bd255db579Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 94 | 46 | adaptation notes |
| 630 | 1 | erw |
| 5 | 2 | maxHeartBeats modifications |
| 1328 | -2 | backward.privateInPublic |
| 150 | 150 | simp +instances |
| 49 | 49 | dsimp +instances |
| 239 | 4 | documentation nolint entries |
| 1 | 1 | large files |
| 13079 | 13079 | backward.isDefEq |
Current commit cf2471da2d
Reference commit bd255db579
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
Commit Verification SummaryWarning Some verifications failed. See details below. Commits to Review (11835)
|
|
As this PR is labelled bors merge |
Contributor
|
Build failed: |
Contributor
Author
|
bors merge |
|
As this PR is labelled bors merge |
Contributor
|
Already running a review |
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
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.