perf: simp_arith: faster denote through Lean.RArray
#6068
Merged
Conversation
This file contains 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
|
!bench |
github-actions
bot
added
the
changes-stage0
nomeata
changed the title
denote through RArrraydenote through RArrray
nomeata
changed the title
denote through RArrraydenote through Lean.RArray
nomeata
changed the title
denote through Lean.RArraydenote through Lean.RArray
|
Here are the benchmark results for commit 90138d8. Benchmark Metric Change
============================================================
- big_omega.lean branch-misses 1.4% (14.8 σ)
- language server startup branches 1.0% (26.4 σ)
- language server startup instructions 1.0% (23.0 σ)
+ simp_arith1 branches -23.9% (-3750.6 σ)
+ simp_arith1 instructions -25.1% (-4892.6 σ)
- unionfind task-clock 11.0% (10.8 σ)
- unionfind wall-clock 11.0% (10.8 σ) |
Merged
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Nov 13, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 13, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Nov 13, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 13, 2024
|
Mathlib CI status (docs):
|
leanprover-community-bot
added
the
builds-mathlib
nomeata
changed the base branch from
joachim/Poly.norm
to
nightly-with-mathlib
nomeata
force-pushed
the
joachim/RArray
branch
from
b79c887
to
ce64f81
Compare
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Nov 13, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 13, 2024
github-merge-queue bot
pushed a commit
that referenced
this pull request
Nov 14, 2024
This PR adds the Lean.RArray data structure. This data structure is equivalent to `Fin n → α` or `Array α`, but optimized for a fast kernel-reduction `get` operation. It is not suitable as a general-purpose data structure. The primary intended use case is the “denote” function of a typical proof by reflection proof, where only the `get` operation is necessary, and where using `List.get` unnecessarily slows down proofs with more than a hand-full of atomic expressions. There is no well-formedness invariant attached to this data structure, to keep it concise; it's semantics is given through `RArray.get`. In that way one can also view an `RArray` as a decision tree implementing `Nat → α`. In #6068 this data structure is used in `simp_arith`.
nomeata
added a commit
that referenced
this pull request
Nov 14, 2024
This PR prepares #6068 by using the `RArray` data structure in `simp_arith` the simp-arith meta code. After the subsequent stage0 we can change the simp-arith theorems in `Init`.
nomeata
added a commit
that referenced
this pull request
Nov 14, 2024
This PR makes `simp_arith` use `RArray` for the context of the reflection proofs, which scales better when there are many variables.
nomeata
force-pushed
the
joachim/RArray
branch
from
065820c
to
a652e9c
Compare
nomeata
added
the
release-ci
nomeata
added a commit
that referenced
this pull request
Nov 14, 2024
This PR makes `simp_arith` use `RArray` for the context of the reflection proofs, which scales better when there are many variables. On our synthetic benchmark: ``` simp_arith1 instructions -25.1% (-4892.6 σ) ``` No effect on mathlib, though, guess it’s not used much on large goals there: http://speed.lean-fro.org/mathlib4/compare/873b982b-2038-462a-9b68-0c0fc457f90d/to/56e66691-2f1f-4947-a922-37b80680315d
nomeata
force-pushed
the
joachim/RArray
branch
from
a652e9c
to
59ee1ac
Compare
This PR prepares #6068 by using the `RArray` data structure in `simp_arith` the simp-arith meta code. After the subsequent stage0 we can change the simp-arith theorems in `Init`.
This PR makes `simp_arith` use `RArray` for the context of the reflection proofs, which scales better when there are many variables. On our synthetic benchmark: ``` simp_arith1 instructions -25.1% (-4892.6 σ) ``` No effect on mathlib, though, guess it’s not used much on large goals there: http://speed.lean-fro.org/mathlib4/compare/873b982b-2038-462a-9b68-0c0fc457f90d/to/56e66691-2f1f-4947-a922-37b80680315d
nomeata
force-pushed
the
joachim/RArray
branch
from
59ee1ac
to
725d59e
Compare
Kha
pushed a commit
that referenced
this pull request
Nov 14, 2024
This PR prepares #6068 by using the `RArray` data structure in `simp_arith` the simp-arith meta code. After the subsequent stage0 we can change the simp-arith theorems in `Init`.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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 improves the asymptotic performance of
simp_arithwhen there are many variables to consider.On our synthetic benchmark:
No effect on mathlib, though, guess it’s not used much on large goals there:
http://speed.lean-fro.org/mathlib4/compare/873b982b-2038-462a-9b68-0c0fc457f90d/to/56e66691-2f1f-4947-a922-37b80680315d