forked from coq/coq
coq dev bench
28 files

bench.sh
benchUtil.ml
benchUtil.mli
dune
gitlab-bench.yml
htmloutput.ml
htmloutput.mli
plotter
profparser.ml
profparser.mli
README.md
render_line_results.ml
render_line_results.mli
render_results.ml
render_results.mli
rocqtimelog2html.ml
rocqtimelog2html.mli
sort-by-deps
sort-by-deps.sh
sourcehandler.ml
sourcehandler.mli
table.ml
table.mli
timelog2html.ml
timelog2html.mli
timelogparser.ml
timelogparser.mli
wrapper.sh
README.md

Rocq Bench Scripts #

Path and Global Environment Setup #

The bench script will create a $workdir/.bin folder and place binaries it owns there. As of today, this is mainly the opam binary, so the script can easily control which version of opam is being used.

This is fixed for a single bench invocation.

Local Environment Setup #

Local environment setup is done by creating opam switches, see the bench.sh:create_opam function.

Timing #

Timing of package builds is done by instrumenting opam to wrap build commands, using the wrap-build-commands: field to point to wrapper.sh, which in turn calls time and perf.

This is not perfect, but seems like a good enough approximation.