diff --git a/tests/playground/Makefile b/tests/playground/Makefile index ca13477e58..a05adc3670 100644 --- a/tests/playground/Makefile +++ b/tests/playground/Makefile @@ -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 diff --git a/tests/playground/bench.nix b/tests/playground/bench.nix index d8e0bb95df..a5857c57d8 100644 --- a/tests/playground/bench.nix +++ b/tests/playground/bench.nix @@ -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 .