refactor: reduce omega's dependency on fvar IDs#9723
Merged
Conversation
Contributor
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit ef1cb71. Benchmark Metric Change
================================================================================
- Init.Data.BitVec.Lemmas branches 2.2% (80.5 σ)
- Init.Data.BitVec.Lemmas instructions 2.0% (66.0 σ)
- Init.Data.List.Sublist async branches 1.5% (52.5 σ)
- Init.Data.List.Sublist async instructions 1.1% (34.0 σ)
- Init.Prelude async branches 1.2% (89.3 σ)
- Std.Data.DHashMap.Internal.RawLemmas branches 1.5% (151.7 σ)
+ Std.Data.DHashMap.Internal.RawLemmas task-clock -16.6% (-42.6 σ)
+ Std.Data.DHashMap.Internal.RawLemmas wall-clock -14.6% (-27.1 σ)
- Std.Data.Internal.List.Associative branches 1.5% (103.5 σ)
+ Std.Data.Internal.List.Associative wall-clock -15.4% (-21.5 σ)
- big_do branches 1.1% (133.1 σ)
- big_omega.lean branches 1.2% (221.6 σ)
- big_omega.lean MT branches 1.2% (219.2 σ)
- binarytrees instructions 1.1% (190.5 σ)
- binarytrees.st instructions 1.1% (527.6 σ)
+ bv_decide_inequality.lean task-clock -6.9% (-30.3 σ)
+ bv_decide_inequality.lean wall-clock -6.8% (-21.0 σ)
- bv_decide_large_aig.lean wall-clock 3.9% (30.0 σ)
+ bv_decide_mod task-clock -6.8% (-52.4 σ)
+ bv_decide_mod wall-clock -6.6% (-35.8 σ)
- bv_decide_rewriter.lean branches 1.0% (45.8 σ)
+ channel.lean bounded0_mpsc -9.3% (-58.5 σ)
+ channel.lean bounded1_mpmc -34.8% (-107.0 σ)
+ channel.lean bounded1_mpsc -26.6% (-28.4 σ)
+ channel.lean boundedn_seq -2.7%
+ channel.lean task-clock -22.5% (-30.2 σ)
+ channel.lean wall-clock -22.6% (-26.6 σ)
- grind_bitvec2.lean branches 1.5% (76.7 σ)
- grind_bitvec2.lean instructions 1.3% (57.7 σ)
+ grind_bitvec2.lean task-clock -7.7% (-169.4 σ)
- grind_list2.lean branches 1.6% (79.1 σ)
- grind_list2.lean instructions 1.2% (51.9 σ)
- grind_ring_5.lean branches 2.5% (804.3 σ)
- grind_ring_5.lean instructions 3.1% (1204.3 σ)
- grind_ring_5.lean task-clock 8.0% (24.0 σ)
- grind_ring_5.lean wall-clock 8.0% (23.5 σ)
- hashmap.lean branch-misses 3.5% (28.6 σ)
- hashmap.lean branches 1.6% (941.3 σ)
+ hashmap.lean insertIfNewHit -2.3%
- lake startup instructions 1.0% (22.8 σ)
- language server startup wall-clock 2.3% (37.8 σ)
+ nat_repr branches -5.6% (-805.4 σ)
+ nat_repr instructions -5.5% (-740.4 σ)
- omega_stress.lean async branches 1.7% (45.0 σ)
- omega_stress.lean async instructions 1.7% (40.4 σ)
- phashmap.lean branches 1.3% (720.9 σ)
+ phashmap.lean containsMiss -5.3%
+ phashmap.lean insertHit -4.5%
+ phashmap.lean iterate -2.4%
+ phashmap.lean task-clock -5.1% (-24.8 σ)
+ phashmap.lean wall-clock -5.1% (-24.7 σ)
+ rbmap_1 instructions -1.4% (-478.1 σ)
- rbmap_fbip instructions 1.8% (196.1 σ)
- reduceMatch instructions 2.0% (235.9 σ)
- riscv-ast.lean branches 1.3% (95.1 σ)
- riscv-ast.lean instructions 1.2% (520.4 σ)
- simp_bubblesort_256 branches 1.3% (40.8 σ)
- simp_local branches 1.3% (249.3 σ)
- simp_subexpr branches 1.2% (29.5 σ)
- stdlib attribute application 5.9% (120.0 σ)
- unionfind instructions 1.2% (399.7 σ) |
Collaborator
|
Reference manual CI status:
|
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 5, 2025
ghost
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Aug 5, 2025
|
Mathlib CI status (docs):
|
ef1cb71 to
b0f3f1e
Compare
Contributor
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit b0f3f1e.Found no runs to compare against. |
Contributor
Author
|
No benchmarks have been run for the merge base commit, so here's a comparison against the previous commit: https://speed.lean-lang.org/lean4/compare/c7cfda2e-49a6-4e52-a268-f106880e0cde/to/bab50d33-13a1-40c4-85a0-fda5f93f8b22?hash2=b0f3f1eb42cc228d10c0519b6e5e9cea3c8fa2a2 |
b0f3f1e to
1559cd4
Compare
Contributor
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit 1559cd4. Benchmark Metric Change
=========================================================
- big_omega.lean branches 6.9% (673.6 σ)
- big_omega.lean instructions 7.2% (789.0 σ)
- big_omega.lean MT branches 7.0% (190.8 σ)
- big_omega.lean MT instructions 7.2% (175.6 σ)
- channel.lean boundedn_seq 1.1%
+ omega_stress.lean async branches -2.0% (-30.9 σ)
+ omega_stress.lean async instructions -2.0% (-29.6 σ)
+ treemap.lean containsHit -5.6%
+ treemap.lean containsMiss -4.1% |
omega's dependency on fvar IDsomega's dependency on fvar IDs
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 replaces some
HashSet Expr-typed collections of facts inomega's implementation with plain lists. This change makes someomegacalls faster, some slower, but the advantage is thatomega's performance is more independent the state of the name generator that produces fvar IDs.I've created this PR for discussion and am happy to hear opinions on whether this should be merged or not. A good reason not to merge is that it causes regressions in some places and
grindis expected to supersedeomegaeither way. A good reason to merge is thatomegais used all over the place and its flaky performance increases the noise in future benchmarks.