[Merged by Bors] - chore: adaptations for nightly-2025-03-02 by kim-em · Pull Request #22460 · leanprover-community/mathlib4

kim-em · 2025-03-02T11:09:40Z

No description provided.

…htly-2025-02-13

…hlib4 into nightly-testing

github-actions · 2025-03-02T11:10:42Z

PR summary caa8523b1b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Data.Array.ExtractLemmas`	-20
`Mathlib.Data.String.Lemmas`	1
`Mathlib.Data.Array.Extract`	20

Declarations diff

+ extract_append_left'
+ extract_append_right'
+ getElem?_take
+ getElem?_take_succ
+ instance (n : ℕ) : TopologicalSpace (Vector α n) := by unfold Vector; infer_instance
+ length_leftpad
+ list_getElem?₁
+ ofList_get?
+ takeUntil_nil
++- list_getElem?
++-- CategoryStruct
++-- list_get?
+--+ Hom
- eq_zero_of_dvd_of_natAbs_lt_natAbs
- extract_append_left
- extract_append_right
- extract_extract
- fvarId?
- instance (n : ℕ) : TopologicalSpace (List.Vector α n) := by unfold List.Vector; infer_instance
- pmap_map
- succ_div
- succ_div_of_dvd
- succ_div_of_not_dvd
- toNat_eq_zero
- toNat_of_nonpos

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

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

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

Increase in tech debt: (relative, absolute) = (5.06, 0.77)

Current number	Change	Type
110	6	adaptation notes
7	5	maxHeartBeats modifications

Current commit caa8523b1b
Reference commit 3f72c0fe93

You can run this locally as

./scripts/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).

kbuzzard · 2025-03-02T13:14:35Z

bors merge

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Markus Himmel <markus@lean-fro.org>

mathlib-bors · 2025-03-02T13:21:45Z

Build failed:

Build

kim-em · 2025-03-02T22:20:31Z

bors merge

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Markus Himmel <markus@lean-fro.org>

mathlib-bors · 2025-03-02T22:57:34Z

Pull request successfully merged into bump/v4.18.0.

Build succeeded:

* chore: adaptations for nightly-2025-02-20 * Merge master into nightly-testing * minor reverts * more * deprecation * another * more * restore check-yaml * . * . * chore: adaptations for nightly-2025-02-20 (#22144) * lake update * fixes * fix namespace * fix test * Merge master into nightly-testing * chore: bump to nightly-2025-02-06 * copy test from master * Merge master into nightly-testing * chore: bump to nightly-2025-02-07 * chore: bump to nightly-2025-02-08 * update * chore: bump to nightly-2025-02-09 * didn't commit * fix * fix test * Update lean-toolchain for testing leanprover/lean4#7013 * chore: bump to nightly-2025-02-10 * fixes for leanprover/lean4#7013 * fixes for leanprover/lean4#7013 * Trigger CI for leanprover/lean4#7013 * chore: bump to nightly-2025-02-11 * update * Update lean-toolchain for testing leanprover/lean4#7046 * Trigger CI for leanprover/lean4#7046 * Switch from mk to ofBitVec * chore: bump to nightly-2025-02-12 * Update lean-toolchain for testing leanprover/lean4#7050 * lake update * lake update * fixes * another maxheartbeats * fix tests * Update lean-toolchain for testing leanprover/lean4#7059 * fix * chore: bump to nightly-2025-02-13 * lake update * fixes * lake exe shake --fix * Update lean-toolchain for testing leanprover/lean4#7069 * Trigger CI for leanprover/lean4#7069 * chore: adaptations for nightly-2025-02-13 * remove upstreamed * Trigger CI for leanprover/lean4#7059 * Trigger CI for leanprover/lean4#7059 * chore: bump to nightly-2025-02-14 * Trigger CI for leanprover/lean4#7069 * Trigger CI for leanprover/lean4#7069 * Update lean-toolchain for testing leanprover/lean4#7082 * quite a bit more to go * lake update * fix merge * fix * adapt * adapt * Trigger CI for leanprover/lean4#7082 * Trigger CI for leanprover/lean4#7069 * lake update * lake update * fixes * fixes * chore: bump to nightly-2025-02-15 * Trigger CI for leanprover/lean4#7069 * Update lean-toolchain for testing leanprover/lean4#7100 * chore: bump to nightly-2025-02-16 * fixes * fixes 2 * fixes 3 * built mathlib * Trigger CI for leanprover/lean4#7069 * fix simps test * fixes for leanprover/lean4#7059 * fix: cache lib dir (adaption for lean4#7001) (#21967) * fixes * fixes for leanprover/lean4#7059 * restore broken files * chore: bump to nightly-2025-02-17 * lake update * lake update * oops * comment out broken files * longFile * oops, one more * . * searchPath * . * Update lean-toolchain for testing leanprover/lean4#7103 * fixes * update manifest * fix * fix * Trigger CI for leanprover/lean4#7103 * chore: bump to nightly-2025-02-18 * lake update * deprecations * restore computability files broken by defeq yesterday * fixes * chore: adaptations for nightly-2025-02-18 * chore: bump to nightly-2025-02-19 * lake update * fixes * fix merge * chore: adaptations for nightly-2025-02-19 * Merge master into nightly-testing * chore: bump to nightly-2025-02-20 * fix merge * chore: adaptations for nightly-2025-02-20 * minor reverts * more * deprecation * another * more * restore check-yaml * . * . --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Mac Malone <mac@lean-fro.org> * chore: bump to nightly-2025-02-21 * chore: bump to nightly-2025-02-22 * chore(Tactic/DeriveTraversable): adapt to `auxDeclToFullName` relocation * Update lean-toolchain for testing leanprover/lean4#7196 * fixes * update batteries * update proofwidgets * Trigger CI for leanprover/lean4#7166 * Trigger CI for leanprover/lean4#7166 * chore: bump to nightly-2025-02-24 * lake update * fixes * deprecations * . * archive * fix tests * fix tests * chore: adaptations for nightly-2025-02-24 (#22266) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> * chore: bump to nightly-2025-02-25 * Trigger CI for leanprover/lean4#7166 * Trigger CI for leanprover/lean4#7166 * Trigger CI for leanprover/lean4#7166 * Trigger CI for leanprover/lean4#7166 * Adapt * Trigger CI for leanprover/lean4#7166 * revert Mathlib/Data/Multiset/Basic, and refix * Merge master into nightly-testing * chore: bump to nightly-2025-02-26 * remove upstreamed * fix * fix tests * Apply suggestions from code review Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> * chore: adaptations for nightly-2025-02-26 (#22347) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> * chore: bump to nightly-2025-02-27 * Trigger CI for leanprover/lean4#7166 * Update lean-toolchain for testing leanprover/lean4#7259 * fix * I would not have guessed that this lemma already exists! * chore: bump to nightly-2025-02-28 * fix * chore: bump to nightly-2025-03-01 * chore: bump to nightly-2025-03-02 * Merge master into nightly-testing * deprecation * Trigger CI for leanprover/lean4#7166 * deprecation * chore: adaptations for nightly-2025-03-02 (#22460) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Markus Himmel <markus@lean-fro.org> * chore: adaptations for nightly-2025-03-02 * chore: bump to nightly-2025-03-03 * remove upstreamed * chore: adaptations for nightly-2025-03-03 * Trigger CI for leanprover/lean4#7166 * chore: adaptations for nightly-2025-03-03 (#22493) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> * bump toolchain and dependencies * Trigger CI for leanprover/lean4#7166 * chore: bump to nightly-2025-03-04 * lake update * Trigger CI for leanprover/lean4#7166 * chore: bump to nightly-2025-03-05 * fix? * add adaptation notes to revert _root_ * Update lean-toolchain for testing leanprover/lean4#7358 * chore: bump to nightly-2025-03-06 * chore: adaptations for nightly-2025-03-06 * chore: adaptations for nightly-2025-03-06 * Merge master into nightly-testing * chore: bump to nightly-2025-03-06 * Update lean-toolchain for testing leanprover/lean4#7261 * fixes for leanprover/lean4#7358 * fixes for leanprover/lean4#7358 * fixes for leanprover/lean4#7358 * Trigger CI for leanprover/lean4#7358 * Trigger CI for leanprover/lean4#7261 * fix Mathlib.Linter.getNamesFrom * chore: adaptations for nightly-2025-03-06 * chore: bump to nightly-2025-03-07 * lake update * add_div is protected * Update lean-toolchain for testing leanprover/lean4#7378 * More like that * adapt * Trigger CI for leanprover/lean4#7378 * Fix * fix * chore: bump to nightly-2025-03-08 * lake update * chore: bump to nightly-2025-03-09 * chore(RingTheory/LocalRing/ResidueField/Ideal): increase `simp` prio, analogous to #22215 * process adaptation notes --------- 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: Markus Himmel <markus@lean-fro.org> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com> Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>

* chore: bump to nightly-2025-02-21 * chore: bump to nightly-2025-02-22 * chore(Tactic/DeriveTraversable): adapt to `auxDeclToFullName` relocation * Update lean-toolchain for testing leanprover/lean4#7196 * fixes * update batteries * update proofwidgets * Trigger CI for leanprover/lean4#7166 * Trigger CI for leanprover/lean4#7166 * chore: bump to nightly-2025-02-24 * lake update * fixes * deprecations * . * archive * fix tests * fix tests * chore: adaptations for nightly-2025-02-24 (#22266) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> * chore: bump to nightly-2025-02-25 * Trigger CI for leanprover/lean4#7166 * Trigger CI for leanprover/lean4#7166 * Trigger CI for leanprover/lean4#7166 * Trigger CI for leanprover/lean4#7166 * Adapt * Trigger CI for leanprover/lean4#7166 * revert Mathlib/Data/Multiset/Basic, and refix * Merge master into nightly-testing * chore: bump to nightly-2025-02-26 * remove upstreamed * fix * fix tests * Apply suggestions from code review Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> * chore: adaptations for nightly-2025-02-26 (#22347) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> * chore: bump to nightly-2025-02-27 * Trigger CI for leanprover/lean4#7166 * Update lean-toolchain for testing leanprover/lean4#7259 * fix * I would not have guessed that this lemma already exists! * chore: bump to nightly-2025-02-28 * fix * chore: bump to nightly-2025-03-01 * chore: bump to nightly-2025-03-02 * Merge master into nightly-testing * deprecation * Trigger CI for leanprover/lean4#7166 * deprecation * chore: adaptations for nightly-2025-03-02 (#22460) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Markus Himmel <markus@lean-fro.org> * chore: adaptations for nightly-2025-03-02 * chore: bump to nightly-2025-03-03 * remove upstreamed * chore: adaptations for nightly-2025-03-03 * Trigger CI for leanprover/lean4#7166 * chore: adaptations for nightly-2025-03-03 (#22493) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> * bump toolchain and dependencies * Trigger CI for leanprover/lean4#7166 * chore: bump to nightly-2025-03-04 * lake update * Trigger CI for leanprover/lean4#7166 * chore: bump to nightly-2025-03-05 * fix? * add adaptation notes to revert _root_ * Update lean-toolchain for testing leanprover/lean4#7358 * chore: bump to nightly-2025-03-06 * chore: adaptations for nightly-2025-03-06 * chore: adaptations for nightly-2025-03-06 * Merge master into nightly-testing * chore: bump to nightly-2025-03-06 * Update lean-toolchain for testing leanprover/lean4#7261 * fixes for leanprover/lean4#7358 * fixes for leanprover/lean4#7358 * fixes for leanprover/lean4#7358 * Trigger CI for leanprover/lean4#7358 * Trigger CI for leanprover/lean4#7261 * fix Mathlib.Linter.getNamesFrom * chore: adaptations for nightly-2025-03-06 * chore: bump to nightly-2025-03-07 * lake update * add_div is protected * Update lean-toolchain for testing leanprover/lean4#7378 * More like that * adapt * Trigger CI for leanprover/lean4#7378 * Fix * fix * chore: bump to nightly-2025-03-08 * lake update * chore: bump to nightly-2025-03-09 * chore(RingTheory/LocalRing/ResidueField/Ideal): increase `simp` prio, analogous to #22215 * process adaptation notes * chore: bump to nightly-2025-03-10 * chore: adaptations for nightly-2025-03-10 * rm upstreamed * rm upstreamed * chore: bump to nightly-2025-03-11 --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>

TwoFX and others added 30 commits February 13, 2025 13:20

lake exe shake --fix

f96a161

Merge master into nightly-testing

5c7de27

Update lean-toolchain for testing leanprover/lean4#7069

822c780

Merge master into nightly-testing

b5178d5

Trigger CI for leanprover/lean4#7069

91278c2

Merge master into nightly-testing

5a3339c

Merge commit '5c7de27570615977f1d1a584a0f695487198d86e' into bump/nig…

e99e0f8

…htly-2025-02-13

chore: adaptations for nightly-2025-02-13

121bad4

Merge branch 'bump/nightly-2025-02-13' into nightly-testing

e5c4e84

Merge master into nightly-testing

0b9e3f8

Merge master into nightly-testing

91771a8

remove upstreamed

64705cf

Merge master into nightly-testing

05645be

Trigger CI for leanprover/lean4#7059

f4051a1

Trigger CI for leanprover/lean4#7059

9b3219f

Merge master into nightly-testing

d14b6e6

chore: bump to nightly-2025-02-14

88e1d18

Merge master into nightly-testing

40ec168

Trigger CI for leanprover/lean4#7069

988e80d

Trigger CI for leanprover/lean4#7069

633b575

Update lean-toolchain for testing leanprover/lean4#7082

43c031d

quite a bit more to go

43d8652

merge 7050

630f76a

lake update

6122733

fix merge

4adc968

fix

394bcaf

Merge master into nightly-testing

ebe69a9

adapt

3d2d6ba

adapt

738c162

Trigger CI for leanprover/lean4#7082

ee5181f

kim-em and others added 16 commits March 1, 2025 10:45

fix

5aee0a1

Merge master into nightly-testing

ff9c515

Merge master into nightly-testing

7294ee2

Merge master into nightly-testing

9f8a02d

chore: bump to nightly-2025-03-01

e105b39

Merge master into nightly-testing

9f7d86b

Merge master into nightly-testing

5ef78bc

Merge master into nightly-testing

06acbbe

Merge master into nightly-testing

b4a2c0a

merge lean-pr-testing-7259

666dd98

Merge master into nightly-testing

523e3bb

chore: bump to nightly-2025-03-02

ccf89ff

Merge master into nightly-testing

e1f18bd

deprecation

f4956b0

Merge branch 'nightly-testing' of github.com:leanprover-community/mat…

f77cdc2

…hlib4 into nightly-testing

chore: adaptations for nightly-2025-03-02

aefa00b

ghost added the ready-to-merge This PR has been sent to bors. label Mar 2, 2025

deprecation

caa8523

mathlib-bors bot changed the title ~~chore: adaptations for nightly-2025-03-02~~ [Merged by Bors] - chore: adaptations for nightly-2025-03-02 Mar 2, 2025

mathlib-bors bot closed this Mar 2, 2025

mathlib-bors bot deleted the bump/nightly-2025-03-02 branch March 2, 2025 22:57

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: adaptations for nightly-2025-03-02#22460

[Merged by Bors] - chore: adaptations for nightly-2025-03-02#22460
kim-em wants to merge 4996 commits intobump/v4.18.0from
bump/nightly-2025-03-02

kim-em commented Mar 2, 2025 •

edited by mathlib-bors bot

Loading

Uh oh!

github-actions bot commented Mar 2, 2025 •

edited

Loading

Declarations diff

Uh oh!

kbuzzard commented Mar 2, 2025

Uh oh!

mathlib-bors bot commented Mar 2, 2025

Uh oh!

kim-em commented Mar 2, 2025

Uh oh!

mathlib-bors bot commented Mar 2, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Conversation

kim-em commented Mar 2, 2025 • edited by mathlib-bors bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Mar 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary caa8523b1b

Import changes for modified files

Declarations diff

Uh oh!

kbuzzard commented Mar 2, 2025

Uh oh!

mathlib-bors bot commented Mar 2, 2025

Uh oh!

kim-em commented Mar 2, 2025

Uh oh!

mathlib-bors bot commented Mar 2, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

kim-em commented Mar 2, 2025 •

edited by mathlib-bors bot

Loading

github-actions bot commented Mar 2, 2025 •

edited

Loading