Skip to content

feat: use realizeConst for all equation, unfold, induction, and partial fixpoint theorems #7261

Merged
Kha merged 4 commits intoleanprover:masterfrom
Kha:push-mmmvwovluvul
Mar 6, 2025
Merged

feat: use realizeConst for all equation, unfold, induction, and partial fixpoint theorems #7261
Kha merged 4 commits intoleanprover:masterfrom
Kha:push-mmmvwovluvul

Conversation

@Kha
Copy link
Copy Markdown
Member

@Kha Kha commented Feb 27, 2025 •
edited
Loading

This PR ensures all equation, unfold, induction, and partial fixpoint theorem generators in core are compatible with parallelism.

Stacked on #7247

@Kha Kha added the changelog-language Language features and metaprograms label Feb 27, 2025
@Kha Kha requested a review from tydeu as a code owner February 27, 2025 20:31
@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 Feb 27, 2025
@ghost
Copy link
Copy Markdown

ghost commented Feb 27, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2e66341f69a0db9ef8b8e5255d0f0cfa73cdadc1 --onto 727c696d9f132bc2701b9755f8819bd36335cd26. (2025-02-27 21:00:11)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ad5a746cdd6c29a47952fc38d6e256ad4071f57e --onto 727c696d9f132bc2701b9755f8819bd36335cd26. (2025-02-28 16:24:17)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ad5a746cdd6c29a47952fc38d6e256ad4071f57e --onto a86145b6bb2669e8864b04ef3f286dc57a4aaef0. (2025-03-02 13:51:18)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ad5a746cdd6c29a47952fc38d6e256ad4071f57e --onto e3c6909ad593e5a966a449df5e92abb1f0dbc317. (2025-03-03 10:35:25)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e7a411a66df1c3f83d3499891616770851e4e5be --onto e3c6909ad593e5a966a449df5e92abb1f0dbc317. (2025-03-03 12:42:10)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0a55f4bf363843b262ea04cdc0137f125d616ff4 --onto e3c6909ad593e5a966a449df5e92abb1f0dbc317. (2025-03-03 13:17:46)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a244b0688244a0b9036fc2f14e63c1368bbdd94c --onto e3c6909ad593e5a966a449df5e92abb1f0dbc317. (2025-03-03 13:47:39)
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-03-05 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-05 16:52:36)
  • 💥 Mathlib branch lean-pr-testing-7261 build failed against this PR. (2025-03-06 10:32:05) View Log
  • 💥 Mathlib branch lean-pr-testing-7261 build failed against this PR. (2025-03-06 13:25:47) View Log
  • ✅ Mathlib branch lean-pr-testing-7261 has successfully built against this PR. (2025-03-06 15:36:45) View Log

@Kha Kha force-pushed the push-mmmvwovluvul branch from 0933ec6 to bc66ac0 Compare February 28, 2025 09:28
@Kha Kha added this pull request to the merge queue Feb 28, 2025
@Kha Kha removed this pull request from the merge queue due to a manual request Feb 28, 2025
@Kha Kha force-pushed the push-mmmvwovluvul branch 2 times, most recently from a998c79 to 7670c44 Compare February 28, 2025 15:57
@Kha Kha requested a review from leodemoura as a code owner February 28, 2025 15:57
@Kha Kha changed the title feat: use realizeConst for all equation theorems feat: use realizeConst for all equation, unfold, induction, and partial fixpoint theorems Feb 28, 2025
@Kha Kha force-pushed the push-mmmvwovluvul branch 9 times, most recently from 748c828 to c4c1325 Compare March 6, 2025 10:02
@Kha Kha force-pushed the push-mmmvwovluvul branch from c4c1325 to fcd0349 Compare March 6, 2025 10:03
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 6, 2025
Update lean-toolchain for testing leanprover/lean4#7261
2927f18
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 6, 2025
Update lean-toolchain for testing leanprover/lean4#7261
cac081e
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 6, 2025
@Kha Kha force-pushed the push-mmmvwovluvul branch from fcd0349 to b1d9ef0 Compare March 6, 2025 12:52
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 6, 2025
Trigger CI for leanprover/lean4#7261
67ea15e
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 6, 2025
Trigger CI for leanprover/lean4#7261
c727132
@ghost ghost added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Mar 6, 2025
@Kha Kha added this pull request to the merge queue Mar 6, 2025
Merged via the queue into leanprover:master with commit 24db5b5 Mar 6, 2025
19 checks passed
kim-em added a commit to leanprover-community/mathlib4 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>
kim-em added a commit to leanprover-community/mathlib4 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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tydeu tydeu Awaiting requested review from tydeu

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

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.

1 participant

@Kha