diff --git a/tests/bench/Makefile b/tests/bench/Makefile
index 9c0d616081..4bcb36a24d 100644
--- a/tests/bench/Makefile
+++ b/tests/bench/Makefile
@@ -173,11 +173,11 @@ report/cross: ; -@mkdir -p $@
report/lean/%: $(foreach cat, $(LEAN_CATS), bench/%$(cat).bench) | report/lean
cat $^ > $@.tmp
- $(TEMCI) report $@.tmp --reporter html2 --html2_out $@ --html2_force_override --properties etime
+ $(TEMCI) report $@.tmp --settings cross.yaml --reporter html2 --html2_out $@ --html2_force_override --properties etime
report/cross/%: $(foreach cat, $(CROSS_TIME_CATS), bench/%$(cat).bench) | report/cross
cat $^ > $@.tmp
- $(TEMCI) report $@.tmp --reporter html2 --html2_out $@ --html2_force_override --properties etime
+ $(TEMCI) report $@.tmp --settings cross.yaml --reporter html2 --html2_out $@ --html2_force_override --properties etime
report/index.html: $(LEAN_BENCHES:%=report/lean/%) $(CROSS_BENCHES:%=report/cross/%)
echo "Lean variant benchmarks
"> $@
@@ -203,7 +203,7 @@ report_cross.csv: bench_cross
BENCHES=$(subst $(space),:,$(CROSS_BENCHES)) CATS=$(subst $(space),:,$(CROSS_CATS)) ./report.py > $@
column -s';' -t < $@
-TO_TEX = 's/-/---/g;s/%/\\%/g;s/\.$$//g;s/(\([0-9]\)\([0-9]\))//g;s/(\([0-9]\))//g;s/;/ \& /g;s/$$/\\\\/'
+TO_TEX = '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
tail -n +2 $< | head -n -1 | sed 's/^\([^;]\+\)/\\verb!\1!/;'$(TO_TEX) > $@
echo -n '\midrule ' >> $@
diff --git a/tests/bench/default.nix b/tests/bench/default.nix
index 8c4cf759b9..d66a9f0825 100644
--- a/tests/bench/default.nix
+++ b/tests/bench/default.nix
@@ -51,9 +51,7 @@ in pkgs.stdenv.mkDerivation rec {
'';
preBuild = bootstrapChanges;
})}/bin";
- LEAN_NO_ST_BIN = "${lean.overrideAttrs (attrs: { prePatch = ''
- substituteInPlace src/runtime/object.h --replace "c_init_mem_kind = object_memory_kind::STHeap" "c_init_mem_kind = object_memory_kind::MTHeap"
- ''; })}/bin";
+ LEAN_NO_ST_BIN = "${lean.overrideAttrs (attrs: { patches = [ ./disable-st.patch ]; })}/bin";
PARSER_TEST_FILE = lean.src + "/library/Init/Core.lean";
GHC = "${ghc}/bin/ghc";
OCAML = "${ocaml}/bin/ocamlopt.opt";
diff --git a/tests/bench/disable-st.patch b/tests/bench/disable-st.patch
new file mode 100644
index 0000000000..87f8a16f72
--- /dev/null
+++ b/tests/bench/disable-st.patch
@@ -0,0 +1,32 @@
+From bebbd732ac64eefe841ec2da25a67c756dfa0f61 Mon Sep 17 00:00:00 2001
+From: Sebastian Ullrich
+Date: Mon, 11 Nov 2019 18:15:21 +0100
+Subject: [PATCH] disable ST objects
+
+---
+ src/runtime/lean.h | 6 +++---
+ 1 file changed, 3 insertions(+), 3 deletions(-)
+
+diff --git a/src/runtime/lean.h b/src/runtime/lean.h
+index 6b37fd91a..c53137860 100644
+--- a/src/runtime/lean.h
++++ b/src/runtime/lean.h
+@@ -567,13 +567,13 @@ void lean_mark_persistent(lean_object * o);
+
+ static inline void lean_set_st_header(lean_object * o, unsigned tag, unsigned other) {
+ #if defined(LEAN_COMPRESSED_OBJECT_HEADER)
+- o->m_header = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | (1ull << LEAN_ST_BIT) | 1;
++ o->m_header = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | (1ull << LEAN_MT_BIT) | 1;
+ #elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
+- o->m_header = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | ((size_t)LEAN_ST_MEM_KIND << 40) | 1;
++ o->m_header = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | ((size_t)LEAN_MT_MEM_KIND << 40) | 1;
+ #else
+ o->m_rc = 1;
+ o->m_tag = tag;
+- o->m_mem_kind = LEAN_ST_MEM_KIND;
++ o->m_mem_kind = LEAN_MT_MEM_KIND;
+ o->m_other = other;
+ #endif
+ }
+--
+2.23.0
diff --git a/tests/bench/report.py b/tests/bench/report.py
index b43ff41998..773881ce6f 100755
--- a/tests/bench/report.py
+++ b/tests/bench/report.py
@@ -13,7 +13,6 @@ from temci.utils import number, settings
import scipy.stats as st
settings.Settings().load_file("cross.yaml")
-number.FNumber.init_settings(settings.Settings()["report/number"])
def single(bench, cat, prop):
f = f"bench/{bench}{cat}.bench"
@@ -34,16 +33,18 @@ def pp(bench, cat, prop, norm):
norm = norm if prop == 'etime' else 1
mean_by_cat[cat].append(s.mean() / norm)
stddev_by_cat[cat].append(s.std_dev() / norm)
- number.FNumber.settings["min_decimal_places"] = 2 if prop == 'etime' else 0
- number.FNumber.settings["max_decimal_places"] = 2 if prop == 'etime' else 0
- return number.fnumber(s.mean() / norm, abs_deviation=s.std_dev() / norm) + ('%' if prop == 'gc' else '')
+ num = number.FNumber(s.mean() / norm, abs_deviation=s.std_dev() / norm)
+ num.settings["min_decimal_places"] = 2 if prop == 'etime' else 0
+ num.settings["max_decimal_places"] = 2 if prop == 'etime' else 0
+ return num.format() + ('%' if prop == 'gc' else '')
def mean(cat, prop):
mean = st.gmean(mean_by_cat[cat])
stddev = st.gmean(stddev_by_cat[cat])
- number.FNumber.settings["min_decimal_places"] = 2 if prop == 'etime' else 0
- number.FNumber.settings["max_decimal_places"] = 2 if prop == 'etime' else 0
- return number.fnumber(mean, abs_deviation=stddev) + ('%' if prop == 'gc' else '') #if prop == 'etime' else '-'
+ num = number.FNumber(mean, abs_deviation=stddev)
+ num.settings["min_decimal_places"] = 2 if prop == 'etime' else 0
+ num.settings["max_decimal_places"] = 2 if prop == 'etime' else 0
+ return num.format() + ('%' if prop == 'gc' else '') #if prop == 'etime' else '-'
CATBAG = {
'.lean': ("Lean [s]", "etime"),