Skip to content

[Merged by Bors] - chore(RingTheory/LocalRing/ResidueField/Ideal): increase simp prio#22215

Closed
JovanGerb wants to merge 1 commit intomasterfrom
ker_algebraMap_residueField
Closed

[Merged by Bors] - chore(RingTheory/LocalRing/ResidueField/Ideal): increase simp prio#22215
JovanGerb wants to merge 1 commit intomasterfrom
ker_algebraMap_residueField

Conversation

@JovanGerb
Copy link
Copy Markdown
Contributor

@JovanGerb JovanGerb commented Feb 23, 2025

This is to override the more general lemma FaithfulSMul.ker_algebraMap_eq_bot. This is needed to avoid a simpNF timeout seen in #21670.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 23, 2025

PR summary 87242fd2b6

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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.

No changes to technical debt.

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

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Feb 23, 2025
@ghost
Copy link
Copy Markdown

ghost commented Feb 23, 2025

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Feb 23, 2025

Here are the benchmark results for commit 87242fd.
There were no significant changes against commit 745dc1a.

@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 23, 2025

File Instructions %
lint -6.48⬝10⁹ (-0.07%)
CI run

@JovanGerb
Copy link
Copy Markdown
Contributor Author

JovanGerb commented Feb 23, 2025

The only speedup is the simpNF of the lemma itself

@grunweg grunweg mentioned this pull request Feb 26, 2025
Closed
2 tasks
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Mar 4, 2025

Let me nominate this PR for merging: it fixes a simpNF time-out (which blocks further work on the Carleson project, that has sat idle for ~two weeks already). This comment explains a deeper issue underlying this:

this is a more general problem with simp. Discrimination tree lookup gives the result (generally) in order from most general to most specific match. Type class search is smart and traverses this array backwards. simp is not so smart at traverses the array forwards, meaning that more general lemmas are tried before more specific lemmas. In this case that leads to this problem.

I think this is worth looking into, but not worth blocking this PR on (as it would require core changes, for instance). So:
maintainer merge?

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 4, 2025

🚀 Pull request has been placed on the maintainer queue by grunweg.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 4, 2025
@fpvandoorn
Copy link
Copy Markdown
Member

fpvandoorn commented Mar 4, 2025

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Mar 4, 2025
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Mar 4, 2025

Edit: the general issue is discussed on zulip here

mathlib-bors bot pushed a commit that referenced this pull request Mar 4, 2025
@JovanGerb
chore(RingTheory/LocalRing/ResidueField/Ideal): increase simp prio (#…
a90ee34 
…22215)

This is to override the more general lemma `FaithfulSMul.ker_algebraMap_eq_bot`. This is needed to avoid a simpNF timeout seen in #21670.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 4, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(RingTheory/LocalRing/ResidueField/Ideal): increase simp prio [Merged by Bors] - chore(RingTheory/LocalRing/ResidueField/Ideal): increase simp prio Mar 4, 2025
@mathlib-bors mathlib-bors bot closed this Mar 4, 2025
@mathlib-bors mathlib-bors bot deleted the ker_algebraMap_residueField branch March 4, 2025 12:49
JovanGerb added a commit that referenced this pull request Mar 10, 2025
@JovanGerb
chore(RingTheory/LocalRing/ResidueField/Ideal): increase simp prio,…
4955224 
… analogous to #22215
@JovanGerb JovanGerb mentioned this pull request Mar 10, 2025
Closed
Kha pushed a commit that referenced this pull request Mar 10, 2025
@JovanGerb @Kha
chore(RingTheory/LocalRing/ResidueField/Ideal): increase simp prio,…
21ebdb2 
… analogous to #22215
kim-em added a commit that referenced this pull request Mar 10, 2025
@jcommelin @kim-em
@TwoFX @nomeata @kmill @tydeu @jrr6 @kbuzzard @Kha @mattrobball @JovanGerb
chore: adaptations for nightly-2025-03-09 (#22758)
ec93745 
* 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>
mathlib-bors bot pushed a commit that referenced this pull request Mar 10, 2025
@JovanGerb
chore(RingTheory/LocalRing/ResidueField/Ideal): increase simp prio,…
b343161 
… analogous to #22215 (#22753)

This PR increases the `simp` priority of a lemma to avoid a `simpNF` timeout. It is analogous to #22215. It is needed to fix the nightly-with-mathlib build.

Edit: this has been cherry-picked to the nightly-testing branch.
kim-em added a commit that referenced this pull request Mar 12, 2025
@jcommelin @jrr6
@kmill @kim-em @nomeata @kbuzzard @TwoFX @Kha @mattrobball @JovanGerb
chore: adaptations for nightly-2025-03-11 (#22826)
2677da0 
* 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>
tukamilano pushed a commit that referenced this pull request Mar 20, 2025
@JovanGerb @tukamilano
chore(RingTheory/LocalRing/ResidueField/Ideal): increase simp prio,…
fdea0aa 
… analogous to #22215 (#22753)

This PR increases the `simp` priority of a lemma to avoid a `simpNF` timeout. It is analogous to #22215. It is needed to fix the nightly-with-mathlib build.

Edit: this has been cherry-picked to the nightly-testing branch.
idontgetoutmuch pushed a commit to idontgetoutmuch/mathlib4 that referenced this pull request Apr 7, 2025
@JovanGerb @idontgetoutmuch
chore(RingTheory/LocalRing/ResidueField/Ideal): increase simp prio,…
6e11f72 
… analogous to leanprover-community#22215 (leanprover-community#22753)

This PR increases the `simp` priority of a lemma to avoid a `simpNF` timeout. It is analogous to leanprover-community#22215. It is needed to fix the nightly-with-mathlib build.

Edit: this has been cherry-picked to the nightly-testing branch.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@JovanGerb @leanprover-bot @grunweg @fpvandoorn