[Merged by Bors] - feat: a `grind` test case by kim-em · Pull Request #25037 · leanprover-community/mathlib4

kim-em · 2025-05-20T07:28:00Z

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

github-actions · 2025-05-20T07:29:09Z

PR summary dac27d1bdf

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 dac27d1bdf
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).

b-mehta · 2025-05-20T20:52:03Z

failing in the presence of Mathlib's typeclass shortcuts

Is this a sign that mathlib has too many typeclass shortcuts? Or that we should be adding them more carefully?

bors merge

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

mathlib-bors · 2025-05-20T21:56:50Z

Pull request successfully merged into bump/v4.21.0.

Build succeeded:

kim-em · 2025-05-21T00:02:59Z

failing in the presence of Mathlib's typeclass shortcuts

Is this a sign that mathlib has too many typeclass shortcuts? Or that we should be adding them more carefully?

bors merge

No, I think it's fine, it was a genuine reducibility settings bug in grind that induced us to add this test case.

* 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 added 2 commits May 20, 2025 17:25

feat: a small grind test case

dfad307

copy paste

dac27d1

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 20, 2025

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 20, 2025

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

mathlib-bors bot changed the title ~~feat: a grind test case~~ [Merged by Bors] - feat: a grind test case May 20, 2025

mathlib-bors bot closed this May 20, 2025

mathlib-bors bot deleted the grind_trig_2 branch May 20, 2025 21:56

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: a `grind` test case#25037

[Merged by Bors] - feat: a `grind` test case#25037
kim-em wants to merge 2 commits intobump/v4.21.0from
grind_trig_2

kim-em commented May 20, 2025

Uh oh!

github-actions bot commented May 20, 2025

Declarations diff

Uh oh!

b-mehta commented May 20, 2025

Uh oh!

mathlib-bors bot commented May 20, 2025

Uh oh!

kim-em commented May 21, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

kim-em commented May 20, 2025

Uh oh!

github-actions bot commented May 20, 2025

PR summary dac27d1bdf

Import changes for modified files

Declarations diff

Uh oh!

b-mehta commented May 20, 2025

Uh oh!

mathlib-bors bot commented May 20, 2025

Uh oh!

kim-em commented May 21, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants