max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/playground/Makefile): output tables after benchmarking

Browse source
This commit is contained in:
Sebastian Ullrich 2019-05-29 09:59:57 +02:00
parent 9e22ae1f12
commit adc462789a
2 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/playground/Makefile
View file

@ -174,9 +174,11 @@ space = $() $()
report_lean.csv: bench_lean
BENCHES=$(subst $(space),:,$(LEAN_BENCHES)) CATS=$(subst $(space),:,$(LEAN_CATS)) ./report.py > $@
column -s';' -t < $@
report_cross.csv: bench_cross
BENCHES=$(subst $(space),:,$(CROSS_BENCHES)) CATS=$(subst $(space),:,$(CROSS_CATS)) ./report.py > $@
column -s';' -t < $@
TO_TEX = 's/expr_const_folding/const_fold/;s/rbmap_checkpoint/rbmap/;s/rbmap_shared/rbmap_1/;s/-/---/g;s/%/\\%/g;s/\.$$//g;s/(\([0-9]\)\([0-9]\))/\\ensuremath{\\tilde{\1}\\tilde{\2}}/g;s/(\([0-9]\))/\\ensuremath{\\tilde{\1}}/g;s/;/ \& /g;s/$$/\\\\/'
report_%.tex: report_%.csv

2
tests/playground/bench.nix
View file

@ -71,7 +71,7 @@ in pkgs.stdenv.mkDerivation rec {
gmp # needed by leanc
(python3.withPackages (ps: [ temci ]))
temci
pkgs.linuxPackages.perf time
pkgs.linuxPackages.perf time unixtools.column
];
patchPhase = ''
patchShebangs .