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

chore: fix cross bench suite

Browse source
This commit is contained in:
Sebastian Ullrich 2019-11-15 16:19:37 +01:00
parent a961e1314a
commit 425230abc4
4 changed files with 44 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/bench/Makefile
View file

@ -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 "<html><h1>Lean variant benchmarks</h1><ul>"> $@
@ -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 ' >> $@

4
tests/bench/default.nix
View file

@ -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";

32
tests/bench/disable-st.patch Normal file
View file

@ -0,0 +1,32 @@
From bebbd732ac64eefe841ec2da25a67c756dfa0f61 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
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

15
tests/bench/report.py
View file

@ -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"),