feat: add options for more control over benchmarking and better profiling support - Githubissues

leanprover / LNSym

Armv8 Native Code Symbolic Simulator in Lean

Apache License 2.0

62 stars 18 forks source link

feat: add options for more control over benchmarking and better profiling support #204

Closed alexkeizer closed 1 month ago

alexkeizer commented 1 month ago

Description:

This PR gives more fine-grained control over benchmarrking:

It adds an option to control how many runs we do
We change the makefile to invoke Lean directly, instead of using Lake. This is needed to ensure we don't get cached data
We've moved the driving of the benchmarks/profiling to a shell script (which is called from the makefile), and ensured benchmarking / profiling data gets logged to files automatically.

Testing:

What tests have been run? Did make all succeed for your changes? Was conformance testing successful on an Aarch64 machine? Yes

License:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

alexkeizer commented 1 month ago

@shigoel merged main and all comments addressed, this should be ready to merge