single file benchmarks #1937
single file benchmarks #1937
Conversation
We add some dune rules to benchmark the compilation of single .v files. It works by writing (theories/file/to/bench.v) in a file called `file_to_bench` and running `dune build @bench`. This uses a program called `hyperfine` which must be available for this to work. After the bench is run it outputs a bench report. Typical output: ``` [ali@allosaurus:~/HoTT]$ dune build @bench Starting bench. This may take a while. Bench finished, report at bench_report: Benchmark 1: /nix/store/v97xkrdzqhwrz8305w05vfix32y5qifa-coq-8.19.1/bin/coqc -R ./theories HoTT -noinit -indices-matter benched_file.v Time (mean ± σ): 6.421 s ± 0.024 s [User: 6.202 s, System: 0.195 s] Range (min … max): 6.364 s … 6.461 s 10 runs ``` Signed-off-by: Ali Caglayan <alizter@gmail.com> <!-- ps-id: 9ddbc823-231a-471c-9eb2-ec07405c0998 -->
There was a problem hiding this comment.
So there isn't a way to pass the name of the file on the command line? With make, we can tell it to do timing by setting some variables, and then use the usual mechanism to just build certain files: make TIMED=1 TIMING=1 path/to/file.vo
BTW, our make set-up has lots of timing options via the scripts in the coq-scripts repo. E.g. before and after comparisons of the whole library. And the line-by-line timing like at the link above. Can those things be done via dune? Currently I rebuild using make when I want to do timing.
|
Dune isn't aware of the The timing makefile scripts are cool but they only really work for make. The same could be adapted to Dune but I don't see the point since it would be a lot of work. In those cases I would just use make. We could make some dune rules that run the makefile in an isolated environment so that it doesn't litter the source directory however. |
|
Oh, and I couldn't work out a way to pass the name via the command line, at least via the dune cli. If you like I can make a bash script in etc/ that takes in the name and updates the file dune is checking before running it. |
|
Also here is hyperfine: https://github.com/sharkdp/hyperfine |
|
It's fine to merge this as is. And I don't mind using make for the older timing scripts. |
We add some dune rules to benchmark the compilation of single .v files. It works by writing
(theories/file/to/bench.v)in a file calledfile_to_benchand runningdune build @bench. This uses a program calledhyperfinewhich must be available for this to work. After the bench is run it outputs a bench report.Typical output: