feat: make equational theorems of non-exposed defs private #8519

nomeata · 2025-05-28T16:07:04Z

This PR makes the equational theorems of non-exposed defs private. If the author of a module chose not to expose the body of their function, then they likely don't want that implementation to leak through equational theorems. Helps with #8419.

There is some amount of incidential complexity due to how private works in lean, by mangling the name: lots of code paths that need now do the right thing™ about private and non-private names, including the whole reserved name machinery.

So this includes a number of refactorings:

The logic for calculating an equational theorem name (or similar) is now done by a single function, mkEqLikeNameFor, rather than all over the place.
Since the name of the equational theorem now depends on the current context (in particular whether it’s a proper module, or a non-module file), the forward map from declaration to equational theorem doesn’t quite work anymore. This map is deleted; the list of equational theorems are now always found by looking for declaration of the expected names (`alreadyGenerated). If users define such theorems themselves (and make it past the “do not allow reserved names to be declared”) they get to keep both pieces.
Because this map was deleted, mathlib’s eqns command can no longer easily warn if equational lemmas have already been generated too early (adaption branch exists). But in general I think lean could provide a more principled way of supporting custom unfold lemmas, and ideally the whole equational theorem machinery is just using that.
The ReservedNamePredicate is used by resolveExact, so we need to make sure that it returns the right name, including privateness. It is not ok to just reserve both the private and non-private name but then later in the ReservedNameAction produce just one of the two.
We create foo.def_eq eagerly for well-founded recursion. This is needed because we need feed in the proof of the rewriting done by wf_preprocess. But if foo.def_eq is private in a module, then a non-module importing it will still expect a non-private foo.def_eq to exist. To patch that, we install a copyPrivateUnfoldTheorem : GetUnfoldEqnFn that declares a theorem aliasing the private one. Seems to work.

This PR makes the equational theorems of non-exposed defs private. If the author of a module chose not to expose the body of their function, then they likely don't want that implementation to leak through equational theorems. Helps with #8419. With some luck doesn't even cause breakage for users outside the module system (e.g. mathlib), as they'll just create their own copy of the theorems if needed.

leanprover-community-bot · 2025-05-28T17:19:07Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-8519 has successfully built against this PR. (2025-05-28 17:19:05) View Log
✅ Mathlib branch lean-pr-testing-8519 has successfully built against this PR. (2025-05-30 00:05:02) View Log
✅ Mathlib branch lean-pr-testing-8519 has successfully built against this PR. (2025-06-02 22:25:16) View Log
💥 Mathlib branch lean-pr-testing-8519 build failed against this PR. (2025-06-04 10:22:18) View Log
🟡 Mathlib branch lean-pr-testing-8519 build against this PR was cancelled. (2025-06-04 11:03:16) View Log
✅ Mathlib branch lean-pr-testing-8519 has successfully built against this PR. (2025-06-04 11:47:47) View Log

nomeata · 2025-05-29T11:08:47Z

!bench

leanprover-bot · 2025-05-29T11:35:21Z

Here are the benchmark results for commit 0b36e36.
There were significant changes against commit 3af9ab6:

  Benchmark          Metric                 Change
  ==========================================================
- Init size          bytes .olean             2.1%
+ Init size          bytes .olean.private    -1.4%
- stdlib             blocked                  1.9% (112.1 σ)
- stdlib             task-clock               1.0%  (22.0 σ)
+ stdlib size        bytes .olean.private    -1.4%
+ workspaceSymbols   task-clock              -6.9% (-33.7 σ)
+ workspaceSymbols   wall-clock              -6.9% (-34.3 σ)

leanprover-bot · 2025-06-04T09:07:37Z

Here are the benchmark results for commit a13df08.
There were significant changes against commit 3af9ab6:

  Benchmark                            Metric                  Change
  =============================================================================
- Init size                            bytes .olean              1.7%
+ Init size                            bytes .olean.private     -1.0%
- Init.Data.BitVec.Lemmas              wall-clock                8.6%  (25.1 σ)
- Init.Data.List.Sublist re-elab -j4   wall-clock               13.8% (753.1 σ)
- bv_decide_inequality.lean            task-clock                4.6%  (40.9 σ)
- bv_decide_inequality.lean            wall-clock                4.6%  (34.8 σ)
- stdlib                               blocked (unaccounted)    30.1%  (59.0 σ)
+ stdlib size                          bytes .olean.private     -1.0%

nomeata · 2025-06-04T09:35:04Z

!bench

nomeata · 2025-06-04T09:41:20Z

!bench

leanprover-bot · 2025-06-04T10:21:19Z

Here are the benchmark results for commit da2132e.
There were significant changes against commit 3af9ab6:

  Benchmark                              Metric                    Change
  ====================================================================================
- Init size                              bytes .olean                1.6%
+ Init size                              bytes .olean.private       -3.7%
+ Init.Data.BitVec.Lemmas                branches                   -3.2%   (-468.2 σ)
+ Init.Data.BitVec.Lemmas                instructions               -3.2%   (-438.8 σ)
+ Init.Data.BitVec.Lemmas                maxrss                    -16.5%    (-21.9 σ)
+ Init.Data.BitVec.Lemmas                task-clock                 -9.9%    (-35.8 σ)
- Init.Data.BitVec.Lemmas                wall-clock                  5.6%     (26.2 σ)
+ Init.Data.BitVec.Lemmas re-elab        branch-misses              -7.1%   (-375.0 σ)
+ Init.Data.BitVec.Lemmas re-elab        branches                   -3.3%    (-99.9 σ)
+ Init.Data.BitVec.Lemmas re-elab        instructions               -3.5%   (-108.8 σ)
+ Init.Data.BitVec.Lemmas re-elab        maxrss                     -8.0%    (-30.7 σ)
+ Init.Data.BitVec.Lemmas re-elab        task-clock                -12.3%    (-83.5 σ)
- Init.Data.List.Sublist async           branches                    1.7%     (31.9 σ)
+ Init.Data.List.Sublist async           task-clock                -12.7%    (-24.9 σ)
- Init.Data.List.Sublist async           wall-clock                 65.2%     (73.6 σ)
- Init.Data.List.Sublist re-elab -j4     branches                    1.7%     (76.4 σ)
- Init.Data.List.Sublist re-elab -j4     instructions                1.0%     (62.0 σ)
+ Init.Data.List.Sublist re-elab -j4     task-clock                -10.0% (-18199.9 σ)
- Init.Data.List.Sublist re-elab -j4     wall-clock                 59.2%    (290.5 σ)
+ Init.Prelude async                     branches                   -3.7%    (-91.1 σ)
+ Init.Prelude async                     instructions               -3.8%    (-82.6 σ)
+ Std.Data.DHashMap.Internal.RawLemmas   branches                   -3.6%   (-584.5 σ)
+ Std.Data.DHashMap.Internal.RawLemmas   instructions               -3.9%   (-564.0 σ)
+ Std.Data.Internal.List.Associative     branches                   -3.1%   (-741.2 σ)
+ Std.Data.Internal.List.Associative     instructions               -3.0%   (-628.3 σ)
+ big_do                                 branches                   -1.7%   (-155.1 σ)
+ big_do                                 instructions               -1.8%   (-127.4 σ)
+ big_omega.lean                         branches                   -4.9%   (-162.0 σ)
+ big_omega.lean                         instructions               -3.9%   (-155.0 σ)
+ big_omega.lean MT                      branches                   -5.0%   (-417.6 σ)
+ big_omega.lean MT                      instructions               -4.0%   (-396.5 σ)
- lake build no-op                       maxrss                      6.4%     (49.8 σ)
+ lake config elab                       instructions               -1.6%    (-93.4 σ)
+ omega_stress.lean async                branches                   -3.0%   (-173.0 σ)
+ omega_stress.lean async                instructions               -2.9%   (-168.2 σ)
- rbmap_library                          task-clock                  8.5%     (28.7 σ)
- rbmap_library                          wall-clock                  8.5%     (28.9 σ)
+ reduceMatch                            instructions               -5.3%    (-85.7 σ)
+ riscv-ast.lean                         branches                   -2.9%   (-145.6 σ)
+ riscv-ast.lean                         instructions               -3.4%   (-184.3 σ)
+ simp_arith1                            branches                   -3.2%    (-33.9 σ)
+ simp_arith1                            instructions               -3.1%    (-30.2 σ)
- stdlib                                 blocked                    14.0%     (99.5 σ)
- stdlib                                 blocked (unaccounted)      23.3%     (29.1 σ)
+ stdlib                                 instructions               -1.5%   (-392.1 σ)
+ stdlib                                 process pre-definitions    -9.1%    (-32.1 σ)
+ stdlib                                 tactic execution           -7.2%    (-33.0 σ)
+ stdlib                                 type checking              -6.6%   (-847.3 σ)
- stdlib size                            bytes .olean                1.9%
+ stdlib size                            bytes .olean.private       -3.7%
- stdlib size                            lines                       1.7%
- unionfind                              task-clock                 13.7%     (31.1 σ)
- unionfind                              wall-clock                 13.7%     (31.1 σ)

leanprover-bot · 2025-06-04T10:45:07Z

Here are the benchmark results for commit 7fa58a8.
There were significant changes against commit 3af9ab6:

  Benchmark                              Metric                    Change
  ==================================================================================
- Init size                              bytes .olean                1.6%
+ Init size                              bytes .olean.private       -3.7%
+ Init.Data.BitVec.Lemmas                branches                   -3.2%  (-74.4 σ)
+ Init.Data.BitVec.Lemmas                instructions               -3.2%  (-68.6 σ)
+ Init.Data.BitVec.Lemmas                maxrss                    -18.9%  (-76.7 σ)
+ Init.Data.BitVec.Lemmas                task-clock                 -9.7%  (-20.7 σ)
+ Init.Data.BitVec.Lemmas re-elab        branch-misses              -9.2% (-867.4 σ)
+ Init.Data.BitVec.Lemmas re-elab        branches                   -3.5%  (-40.2 σ)
+ Init.Data.BitVec.Lemmas re-elab        instructions               -3.7%  (-47.6 σ)
+ Init.Data.BitVec.Lemmas re-elab        maxrss                     -9.7%  (-38.8 σ)
+ Init.Data.BitVec.Lemmas re-elab        task-clock                -13.7%  (-71.4 σ)
- Init.Data.List.Sublist async           branches                    1.6%   (40.7 σ)
- Init.Data.List.Sublist async           instructions                1.0%   (23.0 σ)
+ Init.Data.List.Sublist async           maxrss                    -16.2%  (-21.2 σ)
- Init.Data.List.Sublist async           wall-clock                 45.3%   (23.4 σ)
+ Init.Data.List.Sublist re-elab -j4     branch-misses              -6.0% (-126.5 σ)
+ Init.Data.List.Sublist re-elab -j4     task-clock                -11.8%  (-22.9 σ)
- Init.Data.List.Sublist re-elab -j4     wall-clock                 40.2%   (34.4 σ)
+ Init.Prelude async                     branches                   -3.7% (-145.5 σ)
+ Init.Prelude async                     instructions               -3.8% (-133.1 σ)
+ Std.Data.DHashMap.Internal.RawLemmas   branches                   -3.6% (-715.8 σ)
+ Std.Data.DHashMap.Internal.RawLemmas   instructions               -3.9% (-669.0 σ)
+ Std.Data.Internal.List.Associative     branches                   -3.1% (-404.0 σ)
+ Std.Data.Internal.List.Associative     instructions               -3.0% (-348.4 σ)
+ big_do                                 branches                   -1.7%  (-77.6 σ)
+ big_do                                 instructions               -1.8%  (-69.6 σ)
+ big_omega.lean                         branches                   -4.9% (-138.4 σ)
+ big_omega.lean                         instructions               -3.9% (-148.9 σ)
+ big_omega.lean MT                      branches                   -5.0% (-334.8 σ)
+ big_omega.lean MT                      instructions               -4.0% (-381.0 σ)
+ lake config elab                       instructions               -1.6%  (-63.7 σ)
+ omega_stress.lean async                branches                   -3.0% (-226.4 σ)
+ omega_stress.lean async                instructions               -2.9% (-208.6 σ)
+ reduceMatch                            instructions               -5.3% (-127.5 σ)
+ riscv-ast.lean                         branches                   -2.8%  (-29.9 σ)
+ riscv-ast.lean                         instructions               -3.3%  (-35.1 σ)
+ simp_arith1                            branches                   -3.1%  (-48.3 σ)
+ simp_arith1                            instructions               -3.0%  (-40.1 σ)
+ stdlib                                 blocked (unaccounted)     -38.9%  (-87.2 σ)
+ stdlib                                 instructions               -1.5% (-326.6 σ)
+ stdlib                                 process pre-definitions    -7.5%  (-50.9 σ)
- stdlib size                            bytes .olean                1.9%
+ stdlib size                            bytes .olean.private       -3.7%
- stdlib size                            lines                       1.7%

nomeata · 2025-06-04T10:56:27Z

!bench

leanprover-bot · 2025-06-04T10:56:56Z

Here are the benchmark results for commit 7fa58a8.
There were significant changes against commit 0f4459b:

  Benchmark   Metric                  Change
  ======================================================
+ nat_repr    branches                 -4.7% (-1797.8 σ)
+ nat_repr    instructions             -7.0% (-2206.3 σ)
+ stdlib      blocked (unaccounted)   -34.7%   (-72.8 σ)

* 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 * Update lean-toolchain for testing leanprover/lean4#8519 * 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 * Trigger CI for leanprover/lean4#8519 * 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 * chore: remove simp attribute when value of argument can not be inferred by simp * 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 * change phrasing of comments * chore(Geometry/Manifold): two simp-lemmas can be proven by simp * fix two lint problems * Trigger CI for leanprover/lean4#8519 * chore: bump to nightly-2025-06-03 * fix * fix * Update lean-toolchain for testing leanprover/lean4#8610 * fix * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * cleanup lakefile --------- 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: Kim Morrison <kim@tqft.net> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

@Kha

* Update lean-toolchain for testing leanprover/lean4#8584 * chore: adaptations for nightly-2025-06-02 * change phrasing of comments * chore(Geometry/Manifold): two simp-lemmas can be proven by simp * fix two lint problems * Trigger CI for leanprover/lean4#8519 * chore: bump to nightly-2025-06-03 * fix * fix * Update lean-toolchain for testing leanprover/lean4#8610 * fix * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests --------- 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: Johan Commelin <johan@commelin.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com>

nomeata added the changelog-language Language features, tactics, and metaprograms label May 28, 2025

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 28, 2025

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 28, 2025

Update lean-toolchain for testing leanprover/lean4#8519

d1b903e

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 28, 2025

Update lean-toolchain for testing leanprover/lean4#8519

cbe49fd

nomeata added the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label May 28, 2025

leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label May 28, 2025

Sanity restored to some extend, stage2 builds

0b36e36

Undo change to message

9e33111

nomeata added 3 commits May 29, 2025 15:07

Theorem-copying hack for wfrec.eq_def handling outside the module system

cbe3af0

Forgot to add test file

3f74615

Use copyPrivateUnfoldTheorem also in the module system

a9dd56e

nomeata force-pushed the joachim/private-eqns branch from d93fb0a to a9dd56e Compare May 29, 2025 13:16

nomeata added 3 commits May 29, 2025 16:11

Fix eager eqns for non-rec defs (sigh)

533bd3b

Off by one

2812fe4

Use realizeConst

1e5a38e

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 29, 2025

Trigger CI for leanprover/lean4#8519

26f248c

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request < 8000 relative-time datetime="2025-05-29T23:20:42Z" class="no-wrap">May 29, 2025

Trigger CI for leanprover/lean4#8519

5c8c4b2

nomeata changed the base branch from master to nightly-with-mathlib June 1, 2025 19:46

nomeata changed the base branch from nightly-with-mathlib to joachim/private-eqns-base June 1, 2025 21:15

nomeata closed this Jun 1, 2025

nomeata reopened this Jun 1, 2025

github-actions bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Jun 1, 2025

more whack-a-mole with FunInd

c1509fa

nomeata force-pushed the joachim/private-eqns branch from cdc8873 to 7156f97 Compare June 2, 2025 20:47

More likely to work

c5c10b6

nomeata force-pushed the joachim/private-eqns branch from 7156f97 to 8db6e8d Compare June 2, 2025 21:02

nomeata requested review from digama0, kim-em, Vtec234, kmill, Kha, zwarich and tydeu as code owners June 4, 2025 09:03

github-actions bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Jun 4, 2025

Try env.containsOnBranch

7fa58a8

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 4, 2025

Trigger CI for leanprover/lean4#8519

7204029

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 4, 2025

Trigger CI for leanprover/lean4#8519

c819cdc

leanprover-community-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Jun 4, 2025

nomeata changed the base branch from joachim/private-eqns-base to master June 4, 2025 10:56

leanprover-community-bot 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 Jun 4, 2025

nomeata changed the title ~~feat: equational theorems of non-exposed defs should be private~~ feat: make equational theorems of non-exposed defs private Jun 4, 2025

nomeata enabled auto-merge June 4, 2025 11:51

nomeata added this pull request to the merge queue Jun 4, 2025

Merged via the queue into master with commit b9243e1 Jun 4, 2025
37 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat: make equational theorems of non-exposed defs private #8519

feat: make equational theorems of non-exposed defs private #8519

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

feat: make equational theorems of non-exposed defs private #8519

feat: make equational theorems of non-exposed defs private #8519

Uh oh!

Conversation

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!