perf: avoid mkEqMP and mkEqMPR in simp#7690
Merged
leodemoura merged 4 commits intomasterfrom Mar 27, 2025
Merged
Conversation
Member
Author
|
bench! |
Member
Author
|
!bench |
Member
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit 799cd05. |
Collaborator
|
Here are the benchmark results for commit 9c083c3. |
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Mar 26, 2025
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Mar 26, 2025
|
Mathlib CI status (docs):
|
Misleading name and docstring. The function can be applied to types that are not propositions.
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Mar 26, 2025
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Mar 26, 2025
Member
Author
|
!bench |
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Mar 26, 2025
Collaborator
|
Here are the benchmark results for commit 158f078. Benchmark Metric Change
===============================================================================
- Std.Data.DHashMap.Internal.RawLemmas maxrss 4.1% (37.9 σ)
+ ilean roundtrip compress -7.5% (-12.0 σ)
+ lake config elab task-clock -4.7% (-16.5 σ)
+ lake config elab wall-clock -4.7% (-14.2 σ)
+ language server startup task-clock -2.6% (-15.4 σ)
+ language server startup wall-clock -2.6% (-12.3 σ)
+ liasolver task-clock -8.4% (-49.6 σ)
+ liasolver wall-clock -8.4% (-46.1 σ)
+ nat_repr task-clock -8.0% (-14.3 σ)
+ nat_repr wall-clock -8.0% (-17.4 σ)
+ omega_stress.lean async branch-misses -1.4% (-43.3 σ)
+ qsort task-clock -11.2% (-20.2 σ)
+ qsort wall-clock -11.2% (-21.0 σ)
+ rbmap_fbip task-clock -7.7% (-15.7 σ)
+ rbmap_fbip wall-clock -7.8% (-15.0 σ)
+ stdlib blocked (unaccounted) -3.3% (-48.5 σ)
+ stdlib fix level params -4.0% (-14.9 σ)
+ stdlib maxrss -3.7% (-18.8 σ)
+ stdlib task-clock -3.0% (-27.1 σ)
+ stdlib type checking -3.1% (-30.4 σ)
+ stdlib wall-clock -2.7% (-42.0 σ) |
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Mar 26, 2025
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Mar 31, 2025
* fix * fix again * chore: bump to nightly-2025-03-15 * fix * harden script * chore: bump to nightly-2025-03-16 * Update lean-toolchain for testing leanprover/lean4#7516 * lake update * fixes for leanprover/lean4#7516 * fixes for leanprover/lean4#7516 * partial test fixes * fix stacks * "fix" eqns test * Remove neg instance, there is one upstream now * chore: bump to nightly-2025-03-17 * lake update * lake update * lint * Update lean-toolchain for testing leanprover/lean4#7522 * Update lean-toolchain for testing leanprover/lean4#5182 * Bump batteries for leanprover/lean4#5182 * simp works * Fewer unseal * Trigger CI for leanprover/lean4#5182 * max heartbeats * update test * Update lean-toolchain for testing leanprover/lean4#7519 * Update lean-toolchain for testing leanprover/lean4#7302 * Fix * fixes * Trigger CI for leanprover/lean4#5182 * chore: bump to nightly-2025-03-18 * Less rfl abuse * fix `compile_inductive%` regression * Trigger CI for leanprover/lean4#5182 * Trigger CI for leanprover/lean4#5182 * Trigger CI for leanprover/lean4#5182 * Adapt * process deprecations * Update lean-toolchain for testing leanprover/lean4#7558 * Adapt * deprecations * chore: bump to nightly-2025-03-19 * chore: fixes for leanprover/lean4#7519 * Update lean-toolchain for testing leanprover/lean4#7544 * lake update * fixes for leanprover/lean4#7544 * fixes for leanprover/lean4#7544 * fixes for leanprover/lean4#7544 * fixes for leanprover/lean4#7544 * Trigger CI for leanprover/lean4#7544 * . * cleaning up * chore: bump to nightly-2025-03-20 * update * deprecation/note about upstreamed version * fix * Update lean-toolchain for testing leanprover/lean4#7614 * chore: bump to nightly-2025-03-21 * Adapt back * fix test output * chore: bump to nightly-2025-03-22 * Merge master into nightly-testing * chore: adaptations for nightly-2025-03-22 * fix * Merge master into nightly-testing * protected * chore: bump to nightly-2025-03-24 * update batteries and aesop * fixes for count_cons_of_ne * fix fix to Sym.inhabitedSym' (need `default`, not the `a` that happens to be in context) * bump heartbeats in MathlibTest/observe * fix, deprecated * fix merge * Update lean-toolchain for testing leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * update batteries * fixes for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * update batteries * fixes * chore: bump to nightly-2025-03-25 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * update batteries * Trigger CI for leanprover/lean4#7672 * one fix * fixes * maxheartbeats * fixes for leanprover/lean4#7672 * fixes for leanprover/lean4#7672 * fixes for leanprover/lean4#7672 * fixes for leanprover/lean4#7672 * cleanups * . * chore: bump to nightly-2025-03-26 * update aesop * Update lean-toolchain for testing leanprover/lean4#7690 * Trigger CI for leanprover/lean4#7690 * Trigger CI for leanprover/lean4#7690 * maxHeartbeats * max heartbeats * invalidate cache * another heartbeats * bump batteries * deprecation * Update lean-toolchain for testing leanprover/lean4#7692 * Delete * chore: bump to nightly-2025-03-27 * update batteries * bump batteries * many more maxHeartbeats * chore: bump leantar v0.1.15 * invalidate cache * cache flush, take 2 * feat(Cache): root hash generation counter * 1-line fix * chore: bump to nightly-2025-03-28 * update deps * remove upstreamed * remove all adaptation notes, hooray * merge lean-pr-testing-7692 * fixes from Kevin's review --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com>
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Apr 3, 2025
* chore: bump to nightly-2025-03-22 * Merge master into nightly-testing * chore: adaptations for nightly-2025-03-22 * fix * Merge master into nightly-testing * protected * chore: bump to nightly-2025-03-24 * update batteries and aesop * fixes for count_cons_of_ne * fix fix to Sym.inhabitedSym' (need `default`, not the `a` that happens to be in context) * bump heartbeats in MathlibTest/observe * fix, deprecated * fix merge * Update lean-toolchain for testing leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * update batteries * fixes for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * update batteries * fixes * chore: bump to nightly-2025-03-25 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * update batteries * Trigger CI for leanprover/lean4#7672 * one fix * fixes * maxheartbeats * fixes for leanprover/lean4#7672 * fixes for leanprover/lean4#7672 * fixes for leanprover/lean4#7672 * fixes for leanprover/lean4#7672 * cleanups * . * chore: bump to nightly-2025-03-26 * update aesop * Update lean-toolchain for testing leanprover/lean4#7690 * Trigger CI for leanprover/lean4#7690 * Trigger CI for leanprover/lean4#7690 * maxHeartbeats * max heartbeats * invalidate cache * another heartbeats * bump batteries * deprecation * Update lean-toolchain for testing leanprover/lean4#7692 * Delete * chore: bump to nightly-2025-03-27 * update batteries * bump batteries * many more maxHeartbeats * chore: bump leantar v0.1.15 * invalidate cache * cache flush, take 2 * feat(Cache): root hash generation counter * 1-line fix * chore: bump to nightly-2025-03-28 * update deps * remove upstreamed * remove all adaptation notes, hooray * merge lean-pr-testing-7692 * chore: bump to nightly-2025-03-29 * Update lean-toolchain for testing leanprover/lean4#7717 * fix * Trigger CI for leanprover/lean4#7717 * Trigger CI for leanprover/lean4#7717 * fixes * fixes * Trigger CI for leanprover/lean4#7717 * fixes * fixes * fixes * fixes * got through all of mathlib * missing space * fix tests * Trigger CI for leanprover/lean4#7717 * Trigger CI for leanprover/lean4#7717 * Merge master into nightly-testing * chore: bump to nightly-2025-03-30 * Update lean-toolchain for testing leanprover/lean4#7710 * Trigger CI for leanprover/lean4#7710 * Trigger CI for leanprover/lean4#7710 * Merge master into nightly-testing * Trigger CI for leanprover/lean4#7717 * chore: remove fragile tests * chore: remove fragile tests * Trigger CI for leanprover/lean4#7710 * Update lean-toolchain for testing leanprover/lean4#7736 * how did this get dropped? * Trigger CI for leanprover/lean4#7710 * Trigger CI for leanprover/lean4#7736 * deprecations in Cache * fix * chore: bump to nightly-2025-03-31 * update batteries * merge fixes * fix * fixes * Update lean-toolchain for testing leanprover/lean4#7756 * fix * Update lean-toolchain for testing leanprover/lean4#7764 * eliminate some 7717 adaptation notes * Start fixing, upstream changes needed * Trigger CI for leanprover/lean4#7756 * Fix * Fix * Fix * Fix * Trigger CI for leanprover/lean4#7756 * Trigger CI for leanprover/lean4#7756 * chore: bump to nightly-2025-04-01 * lake update * Trigger CI for leanprover/lean4#7756 * Fix * Fix * Update batteries * Fix * Fix * Trigger CI for leanprover/lean4#7756 * lake update * Fix * Fix * fix for auxlemma detection * remove mention of aux proof in Mathlib.Control.Fix * fix whatsnew * better fix * argh * unfold aux lemmas before transforming aux decls * fixes * optimization: abstract nested proofs in toadditive * docstring * revert change * fix merge * deprecations in shake * fixes * fixes * chore: bump to nightly-2025-04-02 * lake update * fixes * fix test * fix * fix merge --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR avoids
mkEqMPandmkEqMPRinsimp. It creates the proof term without relying on unification.