Skip to content

[Merged by Bors] - chore: bump toolchain to v4.29.0-rc7#37034

Closed
kim-em wants to merge 19 commits intomasterfrom
bump_toolchain_v4.29.0-rc7
Closed

[Merged by Bors] - chore: bump toolchain to v4.29.0-rc7#37034
kim-em wants to merge 19 commits intomasterfrom
bump_toolchain_v4.29.0-rc7

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Mar 23, 2026

This brings the new inferInstanceAs implementation.

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 23, 2026

PR summary 1ea3462986

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ add_top
+ rec_bot
+ rec_coe
+ rec_top
+ stripHeaderEmoji
+ top_add
- instance : IsUniformGroup Circle := inferInstance

You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.


Increase in tech debt: (relative, absolute) = (6.39, 1.33)
Current number Change Type
10 1 maxHeartBeats modifications
8562 -151 backward.isDefEq
12 3 disabled deprecation lints
40 40 backward.inferInstanceAs

Current commit ae37be3877
Reference commit 1ea3462986

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@kim-em kim-em force-pushed the bump_toolchain_v4.29.0-rc7 branch from 7b5065e to 3dfedb3 Compare March 23, 2026 11:51
@leanprover-community leanprover-community deleted a comment from github-actions bot Mar 23, 2026
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Mar 24, 2026

These changes have already been reviewed in leanprover-community#201, and I've gone through all the files looking for anything different from that, so I'm going to put this on the queue now.

bors p=100

bors merge

@mathlib-triage mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Mar 24, 2026
mathlib-bors bot pushed a commit that referenced this pull request Mar 24, 2026
This brings the new `inferInstanceAs` implementation.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 24, 2026

Build failed:

kim-em and others added 18 commits March 24, 2026 01:57
- Remove orphaned adaptation notes in AlgCat/Limits and ModuleCat/ChangeOfRings
- Convert plain comments to #adaptation_note in MonoidAlgebra/Defs
- Move CanonicallyOrderedAdd deriving before CommSemiring ENat (no longer causes downstream failures)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
@kim-em kim-em force-pushed the bump_toolchain_v4.29.0-rc7 branch from e87300a to 90714c1 Compare March 24, 2026 01:59
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Mar 24, 2026

Problem with a newly landed file. Rebasing and fixing now.

@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Mar 24, 2026

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Mar 24, 2026
This brings the new `inferInstanceAs` implementation.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 24, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: bump toolchain to v4.29.0-rc7 [Merged by Bors] - chore: bump toolchain to v4.29.0-rc7 Mar 24, 2026
@mathlib-bors mathlib-bors bot closed this Mar 24, 2026
@mathlib-bors mathlib-bors bot deleted the bump_toolchain_v4.29.0-rc7 branch March 24, 2026 02:45
@JovanGerb
Copy link
Copy Markdown
Contributor

@kim-em, I have noticed now that this PR makes a change in to_additive and fun_prop that makes the trace messages worse. Could you please, in the future, be transparent about this, and clearly mention such changes in the PR description? That way, we can remember to fix such things later!

justus-springer pushed a commit to justus-springer/mathlib4 that referenced this pull request Mar 28, 2026
This brings the new `inferInstanceAs` implementation.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants