[Merged by Bors] - chore: adaptations for nightly-2025-05-19 · Pull Request #25017 · leanprover-community/mathlib4

ghost · 2025-05-19T10:30:03Z

No description provided.

* Trigger CI for leanprover/lean4#7971 * WIP * WIP * WIP * Trigger CI for leanprover/lean4#7971 * Update lean-toolchain for testing leanprover/lean4#7975 * Fix * Trigger CI for leanprover/lean4#7971 * remove adaptation notes * Fix * Fix * chore: bump to nightly-2025-04-16 * revert some stuff * Update lean-toolchain for testing leanprover/lean4#7983 * WIP * Part one * Part two * lake update and fix * Fix * Trigger CI for leanprover/lean4#7983 * Shake * chore: bump to nightly-2025-04-17 * lake update * . * chore: bump to nightly-2025-04-18 * Update lean-toolchain for testing leanprover/lean4#8021 * fix * fix: !bench after Lake path changes (#24143) * fix * fix * chore: bump to nightly-2025-04-19 * Merge master into nightly-testing * temporarirly disable sythorder checking for Grind.IsCharP instance * shake * chore: bump to nightly-2025-04-20 * fix * chore: bump to nightly-2025-04-21 * make fix more robust * fix test * chore: bump to nightly-2025-04-22 * . * sorries * sorries * chore: bump to nightly-2025-04-23 * chore: bump to nightly-2025-04-24 * fix * not there yet * comment out * comment out * chore: bump to nightly-2025-04-25 * bump batteries * more * hacky fix? * add comment * fix lint-style * Fix shake: Parser.parseHeader returns TSyntax instead of Syntax after the new module system * Clean up * Update lean-toolchain for testing leanprover/lean4#8000 * Lake update * Fix * Fix * Fix * Fix * fix to Mathlib/Algebra/Homology/Embedding/Connect.lean * Fix * chore: bump to nightly-2025-04-26 * fix MinImports * Update lean-toolchain for testing leanprover/lean4#8114 * lake update * fix * fixes * fix * fix deprecations * remove accidental files * chore: bump to nightly-2025-04-26 * chore: bump to nightly-2025-04-27 * fixes * cleanup adaptation note * shake --fix * cleanup * . * cleanup * cleanup * cleanup * comments * cleanuo * move batteries back to nightly-testing * fix * fix build hopefully? * fix build hopefully? * chore: bump to nightly-2025-04-28 * Update lean-toolchain for testing leanprover/lean4#8144 * lake update * Fix * fix grind instances * shake * Cleanup * shake * chore: bump to nightly-2025-04-29 * fix * deprecation * Update lean-toolchain for testing leanprover/lean4#8161 * shake * fix GrindInstances * basic test for grind +ring * fixes for leanprover/lean4#8161 * fixes * chore: adaptations for nightly-2025-04-29 * Merge master into nightly-testing * chore: bump to nightly-2025-04-30 * lake update * fix * fix merge * fix merge * Drop a few unnecessary changes * fix test * chore: bump to nightly-2025-05-01 * fix --------- 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: github-actions <github-actions@github.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>

…htly-2025-05-03

…htly-2025-05-19

github-actions · 2025-05-19T10:31:12Z

PR summary 8ca9b57317

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
4 files `Mathlib.Dynamics.PeriodicPts.Defs` `Mathlib.GroupTheory.GroupAction.FixedPoints` `Mathlib.GroupTheory.GroupAction.FixingSubgroup` `Mathlib.GroupTheory.Perm.ClosureSwap`	-1

Declarations diff

+ _root_.Fin.val_intCast
- Inv
- coe_neg
- comp_id
- id_comp
- natCast_dvd_natCast
- neg
- neg_def
- npowRec
- nsmulRec
- ofFin_natCast
- ofFin_neg
- toFin_natCast
- val_eq_zero_iff
- val_ne_zero_iff

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) = (2.90, 0.99)

Current number	Change	Type
3	3	backwards compatibility flags
123	-1	adaptation notes

Current commit 8ca9b57317
Reference commit 19337f2bd8

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-05-19T21:17:14Z

scripts/lint-style.lean

+  let opts : LinterOptions := {
+    toOptions := ← getLakefileLeanOptions,
+    linterSets := sets,
+  }


I can't review this part of the PR or the change in MathlibTest/ModuleCasing.lean but other than that LGTM.

bors d+

mathlib-bors · 2025-05-19T21:17:17Z

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

kim-em · 2025-05-20T05:01:49Z

bors merge

Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

mathlib-bors · 2025-05-20T05:08:15Z

Pull request successfully merged into bump/v4.21.0.

Build succeeded:

* Update lean-toolchain for testing leanprover/lean4#8347 * fixes for leanprover/lean4#8347 * Update lean-toolchain for testing leanprover/lean4#8397 * deprecations for leanprover/lean4#8397 * chore: bump to nightly-2025-05-19 * chore: adaptations for nightly-2025-05-19 * Trigger CI for leanprover/lean4#8347 * Update the style linter to use LinterOptions * Fix test * chore: adaptations for nightly-2025-05-19 (#25017) Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> * chore: bump to nightly-2025-05-20 * Merge master into nightly-testing * feat: a `grind` test case (#25037) Adds a test case for `grind` that was previously failing in the presence of Mathlib's typeclass shortcuts. Let's just keep it in Mathlib as a regression test. Note that this is a PR to `bump/v4.21.0`, as it requires a recent nightly toolchain. (It can still be reviewed and bors'd as any other PR.) * lake update * fixes * fixes * fixes * fixes * fix * fixes * fixes * shake --update * chore: bump to nightly-2025-05-21 * Update lean-toolchain for testing leanprover/lean4#7352 * lake update * Trigger CI for leanprover/lean4#7352 * chore: adaptations for nightly-2025-05-21 * chore: adaptations for nightly-2025-05-21 (#25079) Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> * chore: adaptations for nightly-2025-05-21 * fix for leanprover/lean4#7352 * remove unneeded List.ofFn_succ from simp sets * Merge master into nightly-testing * Merge master into nightly-testing * Revert "fix for leanprover/lean4#7352" This reverts commit 38ca408. * chore: fix some defeq abuse in theorem statements around the `Id` monad (#25098) Follows on from leanprover/lean4#7352. This also deprecates: * `id.mk`, which looks like a porting error * `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere. * chore: bump to nightly-2025-05-22 * update batteries * chore: bump to nightly-2025-05-23 * Update lean-toolchain for testing leanprover/lean4#8449 * chore: adaptations for nightly-2025-05-22 (#25110) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: github-actions <github-actions@github.com> * remove now upstreamed `clear_value` * Update lean-toolchain for testing leanprover/lean4#8457 * chore: update tests for `Format` bug fix * Trigger CI for leanprover/lean4#8457 * lake update * lake update * fixes * Merge master into nightly-testing * chore: bump to nightly-2025-05-24 * fix * chore: adaptations for nightly-2025-05-24 (#25147) Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: github-actions <github-actions@github.com> * chore: adaptations for nightly-2025-05-24 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8470 * chore: bump to nightly-2025-05-25 * chore: adaptations for nightly-2025-05-25 * chore: adaptations for nightly-2025-05-25 (#25184) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: github-actions <github-actions@github.com> * unsimp `List.getElem?_length` This is solved using `getElem?_neg` now. * chore: adaptations for nightly-2025-05-25 * Trigger CI for leanprover/lean4#8470 * chore: bump to nightly-2025-05-26 * lake update * deprecations * Trigger CI for leanprover/lean4#8449 * Merge master into nightly-testing * chore: bump to nightly-2025-05-27 * chore: adaptations for nightly-2025-05-27 * Update lean-toolchain for testing leanprover/lean4#8504 * chore: bump to nightly-2025-05-28 * chore: adaptations for nightly-2025-05-27 (#25234) Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * fix * fix merge * fix merge again * deprecations * deprecations * fix Archive * comment out test * Fix and re-enable directory dependency lint test. * chore: bump to nightly-2025-05-29 * Use the formatting from the master branch. (Seems to have been a merge that went wrong.) * lake update * chore: adaptations for nightly-2025-05-28 (#25295) 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: github-actions <github-actions@github.com> * fix * Trigger CI for leanprover/lean4#8337 * fixes * Merge master into nightly-testing * chore: bump to nightly-2025-05-30 * chore: adaptations for nightly-2025-05-29 (#25306) 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: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Rob23oba <robin.arnez@web.de> * chore: bump to nightly-2025-05-31 * chore: bump to nightly-2025-06-01 * fix Archive * chore: adaptations for nightly-2025-06-01 (#25355) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> * chore: bump to nightly-2025-06-02 * chore: adaptations for nightly-2025-06-02 (#25360) Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: github-actions <github-actions@github.com> * Update lean-toolchain for testing leanprover/lean4#8584 * chore: adaptations for nightly-2025-06-02 * chore: bump to nightly-2025-06-03 * fix * fix * Update lean-toolchain for testing leanprover/lean4#8610 * fix * chore: bump to nightly-2025-06-04 * bump toolchain --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>

kim-em and others added 30 commits May 1, 2025 21:36

Merge remote-tracking branch 'origin/master' into bump/v4.20.0

786bdc3

chore: adaptations for nightly-2025-05-01

1b64f60

Merge branch 'bump/nightly-2025-05-01' into nightly-testing

0ef83ca

Merge master into nightly-testing

d506c8e

Merge master into nightly-testing

1fbbc90

Merge master into nightly-testing

5c2ab8c

chore: bump to nightly-2025-05-02

9609f78

Merge master into nightly-testing

2e4df63

Merge master into nightly-testing

3d59a1b

Merge master into nightly-testing

75dfe88

Merge master into nightly-testing

f890daf

Merge master into nightly-testing

38e6302

Merge master into nightly-testing

104233e

chore: bump to nightly-2025-05-03

f023f89

Merge master into nightly-testing

af3f7e5

Merge remote-tracking branch 'origin/master' into bump/v4.20.0

12d2469

Merge commit 'af3f7e59787eba900eb6489ddf6631eb87099d3f' into bump/nig…

313d95c

…htly-2025-05-03

chore: adaptations for nightly-2025-05-03

197dd72

Merge master into nightly-testing

6b5e0ff

Update lean-toolchain for testing leanprover/lean4#8216

778537b

Trigger CI for leanprover/lean4#8216

f66e9f6

Merge master into nightly-testing

7c0e93a

Merge master into nightly-testing

d80654e

Merge master into nightly-testing

fa1d0d9

chore: bump to nightly-2025-05-04

f061ec1

Merge master into nightly-testing

584f4b5

Merge master into nightly-testing

42f0d63

Merge master into nightly-testing

0b1d10b

Merge master into nightly-testing

fb7f898

leanprover-community-mathlib4-bot and others added 14 commits May 18, 2025 12:43

Merge master into nightly-testing

d1c6356

Merge master into nightly-testing

007f700

Merge master into nightly-testing

13ba4ea

Merge master into nightly-testing

251b8b5

Merge master into nightly-testing

42ae9ee

Update lean-toolchain for testing leanprover/lean4#8397

c3fbade

Merge master into nightly-testing

8bd49bc

deprecations for leanprover/lean4#8397

bfa433c

Merge master into nightly-testing

5402292

chore: bump to nightly-2025-05-19

7d3a2d5

merge lean-pr-testing-8397

4ce1ed9

Merge master into nightly-testing

f27355c

Merge commit 'f27355c1aed94df0bcbaf74b72d86c1daebfda6e' into bump/nig…

52ced6b

…htly-2025-05-19

chore: adaptations for nightly-2025-05-19

6069d9e

Update the style linter to use LinterOptions

5cef263

github-actions bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 19, 2025

Fix test

8ca9b57

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 19, 2025

kbuzzard reviewed May 19, 2025

View reviewed changes

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

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

mathlib-bors bot changed the title ~~chore: adaptations for nightly-2025-05-19~~ [Merged by Bors] - chore: adaptations for nightly-2025-05-19 May 20, 2025

mathlib-bors bot closed this May 20, 2025

mathlib-bors bot deleted the bump/nightly-2025-05-19 branch May 20, 2025 05:08

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: adaptations for nightly-2025-05-19#25017

[Merged by Bors] - chore: adaptations for nightly-2025-05-19#25017
ghost wants to merge 6531 commits intobump/v4.21.0from
bump/nightly-2025-05-19

ghost commented May 19, 2025 •

edited by mathlib-bors bot

Loading

Uh oh!

github-actions bot commented May 19, 2025 •

edited

Loading

Declarations diff

Uh oh!

kbuzzard May 19, 2025

Uh oh!

mathlib-bors bot commented May 19, 2025

Uh oh!

kim-em commented May 20, 2025

Uh oh!

mathlib-bors bot commented May 20, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

9 participants

Conversation

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

Uh oh!

PR summary 8ca9b57317

Import changes for modified files

Declarations diff

Uh oh!

kbuzzard May 19, 2025

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented May 19, 2025

Uh oh!

kim-em commented May 20, 2025

Uh oh!

mathlib-bors bot commented May 20, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

9 participants

ghost commented May 19, 2025 •

edited by mathlib-bors bot

Loading

github-actions bot commented May 19, 2025 •

edited

Loading