Skip to content

fix: reduce priorities of CommRing parent projections#7975

Merged
kim-em merged 3 commits intomasterfrom
commring_parents
Apr 15, 2025
Merged

fix: reduce priorities of CommRing parent projections#7975
kim-em merged 3 commits intomasterfrom
commring_parents

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Apr 15, 2025 •
edited
Loading

This PR reduces the priority of the parent projections of Lean.Grind.CommRing, to avoid these being used in typeclass inference in Mathlib.

@kim-em kim-em enabled auto-merge April 15, 2025 13:24
mattrobball
mattrobball reviewed Apr 15, 2025
View reviewed changes
src/Init/Grind/CommRing/Basic.lean

-- We reduce the priority of these parent instances,
-- so that in downstream libraries with their own `CommRing` class,
-- the path `CommRing -> Add` is found before `CommRing -> Lean.Grind.CommRing -> Add`.
Copy link
Copy Markdown
Contributor

@mattrobball mattrobball Apr 15, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there/will there be a CommRing -> Lean.Grind.CommRing path?

Copy link
Copy Markdown
Collaborator Author

@kim-em kim-em Apr 15, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it's already there in nightly-testing.

Copy link
Copy Markdown
Collaborator Author

@kim-em kim-em Apr 15, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The path that this PR avoids is still defeq, but that still managed to trip up the move_add tactic.

@kim-em kim-em added language changelog-language Language features and metaprograms and removed language labels Apr 15, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 15, 2025 13:44 Inactive
@kim-em kim-em added this pull request to the merge queue Apr 15, 2025
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 15, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 15, 2025
Update lean-toolchain for testing leanprover/lean4#7975
cae1557
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 15, 2025
Update lean-toolchain for testing leanprover/lean4#7975
0eae0bd
Merged via the queue into master with commit 525fd26 Apr 15, 2025
25 of 27 checks passed
@ghost ghost added the builds-mathlib CI has verified that Mathlib builds against this PR label Apr 15, 2025
@ghost
Copy link
Copy Markdown

ghost commented Apr 15, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

kmill added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 19, 2025
@kmill @kim-em
@TwoFX @Rob23oba @digama0 @jcommelin
chore: adaptations for nightly-2025-04-16 (#24202)
f0b7487 
* fixes

* fix test

* fix

* chore: adaptations for leanprover/lean4#7797

* stricter rfl check

* fix merge

* Trigger CI for leanprover/lean4#7797

* Trigger CI for leanprover/lean4#7797

* Trigger CI for leanprover/lean4#7797

* inverse construction

* Update lean-toolchain for testing leanprover/lean4#7791

* lake update

* Fix

* Fix

* Fix

* chore: bump to nightly-2025-04-03

* more fixes

* merge lean-pr-testing-6325

* bump proofwidgets

* Update lean-toolchain for testing leanprover/lean4#7812

* shake

* fix shake

* fix tests

* import mathlib.init

* Update lean-toolchain for testing leanprover/lean4#7816

* Trigger CI for leanprover/lean4#7816

* Update lean-toolchain for testing leanprover/lean4#7802

* Fix

* fixes

* Fix (pending upstream changes)

* Trigger CI for leanprover/lean4#7802

* fix

* chore: bump to nightly-2025-04-04

* Fix

* Fix

* Fix

* Fix

* Fix

* Fix

* Update lean-toolchain for testing leanprover/lean4#7818

* Fix

* Fix

* Fix

* Merge master into nightly-testing

* Fix

* Fix comments

* fixes

* Trigger CI for leanprover/lean4#7816

* fix

* fix

* missing doc-string?

* chore: bump to nightly-2025-04-05

* chore: bump to nightly-2025-04-06

* move Batteries to nightly-testing

* lake update

* lint

* fix

* chore: bump to nightly-2025-04-07

* sprinkle noncomputable

* fix: relativize file paths

fix for leanprover/lean4#7822

* chore: reset cache

* chore: bump to nightly-2025-04-07

* shake

* fix: relativize more

* Update lean-toolchain for testing leanprover/lean4#7856

* Update lean-toolchain for testing leanprover/lean4#7851

* Fix

* Fix

* Fix

* Fix

* chore: bump to nightly-2025-04-08

* Update lean-toolchain for testing leanprover/lean4#7870

* Trigger CI for leanprover/lean4#7870

* Trigger CI for leanprover/lean4#7870

* Trigger CI for leanprover/lean4#7870

* wip

* Trigger CI for leanprover/lean4#7870

* .

* chore: bump to nightly-2025-04-09

* Trigger CI for leanprover/lean4#7870

* .

* bump

* lake update

* fixes for leanprover/lean4#7873

* fixes

* deprecations

* chore: bump to nightly-2025-04-10

* chore: `Option.zipWith` -> `Option.merge`

* lake update

* toolchain

* fix

* fix

* Update lean-toolchain for testing leanprover/lean4#7897

* Trigger CI for leanprover/lean4#7897

* fix

* lake update and fix

* Fix

* Fix

* Trigger CI for leanprover/lean4#7897

* fix merge

* chore: adaptations for nightly-2025-04-10

* chore: bump to nightly-2025-04-14

* fix

* .

* annotate changed goal state

* fixes (adaptation notes)

* cleanup imports

* cleanup

* Update lean-toolchain for testing leanprover/lean4#7933

* Fix

* Fix

* Update lean-toolchain for testing leanprover/lean4#7975

* remove adaptation notes

* chore: bump to nightly-2025-04-16

---------

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: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: github-actions <github-actions@github.com>
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request May 2, 2025
@kim-em @TwoFX
@Rob23oba @Kha @kmill @joelriou @Ruben-VandeVelde @jcommelin
chore: adaptations for nightly-2025-05-01 (#24524)
0ec9062 
* 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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@mattrobball mattrobball mattrobball left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@kim-em @mattrobball