feat: add bv_omega_bench to run omega and produce goal states + timing inf. #223
+163
−75
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
This reverts commit 3bc84e2.
|
pennyannn
reviewed
Oct 7, 2024
|
Cool! LGTM modulo that CI is failing. |
This is insane, the macOS file system is case insensitive?! WTAF.
|
@pennyannn thanks, this was crazy, I didn't know that the MacOS filesystem is case insensitive (!) I spent an hour going crazy, only to realize that my file used to be called |
|
I've started porting the extracted examples into the lean4 benchmark suite, at leanprover/lean4#5622. We can run the bench suite locally, to get output such as: (venv) ➜ bench git:(omega-benchmarks) ✗ temci exec --config speedcenter.yaml --included_blocks omega --out base.yaml --runner time
Benchmark 3 out of 3 to 3 [####################################] 100%
Report for single runs
omega1 ( 3 single benchmarks)
etime mean = 3.(503), deviation = 13.95525%
maxrss mean = 369459200.0(00), deviation = 0.82300%Note that this needs one to setup ~ $ python3 -m venv venv
~ $ source venv/bin/activate
(venv) ~ $ git clone https://github.com/Kha/temci.git
(venv) ~ $ cd temci
(venv) ~/temci $ pip3 install .
(venv) ~/temci $ which temci
/Users/sidbhatz/work/lean4/venv/bin/temci
(venv) ~/temci $ brew install gnu-time # no perf on macOS, fallback to the bare minimum benching we can have.
(venv) ~/temci $ cd ~/lean4/tests/bench
(venv) ~/lean4/tests/bench $ temci exec --config speedcenter.yaml --included_blocks omega --out base.yaml --runner time
Benchmark 3 out of 3 to 3 [####################################] 100%
Report for single runs
omega1 ( 3 single benchmarks)
etime mean = 3.(503), deviation = 13.95525%
maxrss mean = 369459200.0(00), deviation = 0.82300%
|
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.
Description:
This PR replaces
bv_omegawithbv_omega_bench, which is used to write benchmarking results into a user-specified filepath. This enables us to extract out benchmarks to be upstreamed, as begun in leanprover/lean4#5622.We make the file path, whether the benchmark run is enabled or not, and the minimum time necessary to be added to the benchmark all user-configurable parameters.
Testing:
What tests have been run? Did
make allsucceed for your changes? Wasconformance testing successful on an Aarch64 machine?
License:
By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.