Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

perf: speed up bv_decide reflection using Lean.RArray #6288

Merged
merged 1 commit into from
Dec 2, 2024

Conversation

hargoniX
Copy link
Contributor

@hargoniX hargoniX commented Dec 2, 2024

This PR uses Lean.RArray in bv_decide's reflection proofs. Giving speedups on problems with lots of variables.

Implement like #6068, speedup:

# before
λ hyperfine "lean +nightly-2024-12-02 tests/lean/run/bv_reflection_stress.lean"
Benchmark 1: lean +nightly-2024-12-02 tests/lean/run/bv_reflection_stress.lean
  Time (mean ± σ):      1.939 s ±  0.007 s    [User: 1.549 s, System: 0.104 s]
  Range (min … max):    1.928 s …  1.947 s    10 runs
# after
λ hyperfine "lean tests/lean/run/bv_reflection_stress.lean"                                                                                                                                                                                                                        
Benchmark 1: lean tests/lean/run/bv_reflection_stress.lean
  Time (mean ± σ):      1.409 s ±  0.006 s    [User: 1.058 s, System: 0.073 s]
  Range (min … max):    1.401 s …  1.419 s    10 runs

@hargoniX hargoniX added the changelog-language Language features, tactics, and metaprograms label Dec 2, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc December 2, 2024 15:45 Inactive
@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 Dec 2, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0b8f50f78d9bb94c5034a5044e662b0b8e37e7ca --onto 3c5e612dc54733cd707becb929457d2f9d8ca6fd. (2024-12-02 16:00:26)

@hargoniX hargoniX added this pull request to the merge queue Dec 2, 2024
Merged via the queue into master with commit b2336fd Dec 2, 2024
20 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants