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

kim-em · 2025-02-26T23:42:28Z

No description provided.

…hlib4 into nightly-testing

github-actions · 2025-02-26T23:43:25Z

PR summary 106b30b09d

Import changes exceeding 2%

%	File
+3.12%	`Mathlib.Data.String.Lemmas`

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
- 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_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 106b30b09d
Reference commit 6b00c05d2a

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

bors d+

Mathlib/Data/List/Cycle.lean

mathlib-bors · 2025-02-26T23:48:31Z

✌️ kim-em can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

kim-em · 2025-02-27T03:02:53Z

bors merge

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>

mathlib-bors · 2025-02-27T03:49:30Z

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>

kim-em and others added 30 commits February 11, 2025 21:20

update

619a1eb

Merge master into nightly-testing

d7c0a3d

chore: adaptations for nightly-2025-02-11

de8a5a2

Auto-resolved conflicts in lean-toolchain and lake-manifest.json

57cc905

Merge master into nightly-testing

4c9ceb7

Merge master into nightly-testing

a194b2b

Merge master into nightly-testing

52d74eb

Merge master into nightly-testing

9816453

Merge master into nightly-testing

e18fa28

Merge master into nightly-testing

e5b0b5f

Update lean-toolchain for testing leanprover/lean4#7046

0105da2

Trigger CI for leanprover/lean4#7046

7b57251

Switch from mk to ofBitVec

00b14c3

Merge master into nightly-testing

8bae919

Merge master into nightly-testing

10080a1

chore: bump to nightly-2025-02-12

6dacc8d

Update lean-toolchain for testing leanprover/lean4#7050

ba3ca97

lake update

6d7d448

Merge master into nightly-testing

e75a805

Merge master into nightly-testing

ff234e2

lake update

07788b5

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

f6aa132

…hlib4 into nightly-testing

fixes

1b76eb4

another maxheartbeats

d046f2c

fix tests

5eae4dc

Update lean-toolchain for testing leanprover/lean4#7059

94c9ece

Merge master into nightly-testing

062587a

chore: adaptations for nightly-2025-02-12

3caf9ec

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

9569552

Merge master into nightly-testing

ba970d5

kim-em and others added 15 commits February 26, 2025 08:44

revert Mathlib/Data/Multiset/Basic, and refix

a429f61

chore: adaptations for nightly-2025-02-25

301c29f

Merge master into nightly-testing

bced3d0

Merge master into nightly-testing

acad01c

Merge master into nightly-testing

5195271

chore: bump to nightly-2025-02-26

255c497

remove upstreamed

5d88f64

Merge master into nightly-testing

c937e04

Merge master into nightly-testing

1353c6c

Merge master into nightly-testing

7342ab8

Merge master into nightly-testing

896bbcf

Merge master into nightly-testing

c1fd7b2

fix

bc7d9eb

fix tests

aaaee15

chore: adaptations for nightly-2025-02-26

d46caa0

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 26, 2025

kbuzzard approved these changes Feb 26, 2025

View reviewed changes

Mathlib/Data/List/Cycle.lean Outdated Show resolved Hide resolved

Mathlib/Data/List/Cycle.lean Outdated Show resolved Hide resolved

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 26, 2025

Apply suggestions from code review

106b30b

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

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

mathlib-bors bot pushed a commit that referenced this pull request Feb 27, 2025

chore: adaptations for nightly-2025-02-26 (#22347)

edfd1ab

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>

mathlib-bors bot changed the title ~~chore: adaptations for nightly-2025-02-26~~ [Merged by Bors] - chore: adaptations for nightly-2025-02-26 Feb 27, 2025

mathlib-bors bot closed this Feb 27, 2025

mathlib-bors bot deleted the bump/nightly-2025-02-26 branch February 27, 2025 03:49

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: adaptations for nightly-2025-02-26#22347

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

kim-em commented Feb 26, 2025 •

edited by mathlib-bors bot

Loading

Uh oh!

github-actions bot commented Feb 26, 2025 •

edited

Loading

Declarations diff

Uh oh!

kbuzzard left a comment

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Feb 26, 2025

Uh oh!

kim-em commented Feb 27, 2025

Uh oh!

mathlib-bors bot commented Feb 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

Conversation

kim-em commented Feb 26, 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 Feb 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 106b30b09d

Import changes for modified files

Declarations diff

Uh oh!

kbuzzard left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Feb 26, 2025

Uh oh!

kim-em commented Feb 27, 2025

Uh oh!

mathlib-bors bot commented Feb 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

kim-em commented Feb 26, 2025 •

edited by mathlib-bors bot

Loading

github-actions bot commented Feb 26, 2025 •

edited

Loading