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

test: update Lean variant benchmarks

Browse source
This commit is contained in:
Sebastian Ullrich 2023-01-20 12:45:37 +01:00
parent 2a7ae7b28a
commit 1f41b91206
6 changed files with 91 additions and 67 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/bench/Makefile
View file

@ -103,7 +103,7 @@ bench:
bench/%.bench: %.out | bench
ulimit -s unlimited && $(TEMCI) short exec $(TEMCI_FLAGS) -d $< "./$< $(BENCH_PARAMS)" --out $@
bench/parser.%.bench: BENCH_PARAMS = $(PARSER_TEST_FILE) 100
bench/parser.%.bench: BENCH_PARAMS = $(PARSER_TEST_FILE) 10
bench/binarytrees.%.bench: BENCH_PARAMS = 21
bench/binarytrees.ml.bench: BENCH_PARAMS = $$(nproc) 21
@ -130,7 +130,7 @@ bench/unionfind.%.bench: BENCH_PARAMS = 3000000
bench/%gc.lean.bench: %lean.out | bench
ulimit -s unlimited && $(TEMCI) short exec $(TEMCI_FLAGS)\
-d $< "perf record -o $@.tmp ./$< $(BENCH_PARAMS) >/dev/null && perf report -i $@.tmp -t ';' --stdio -S 'lean_dec_ref_cold,lean_del_core,lean_free_small' | ./lean-gc.py"\
-d $< "perf record -o $@.tmp ./$< $(BENCH_PARAMS) >/dev/null && perf report -i $@.tmp -t ';' --stdio -S 'lean_inc_ref_cold,lean_inc_ref_n_cold,lean_dec_ref_cold,lean_del_core,lean_free_small' | ./lean-gc.py"\
--runner output --out $@
bench/%gc.hs.bench: %hs.out | bench
@ -201,12 +201,12 @@ report: report/index.html
# yes.
space = $() $()
report_lean.csv: bench_lean
BENCHES=$(subst $(space),:,$(LEAN_BENCHES)) CATS=$(subst $(space),:,$(LEAN_CATS)) ./report.py > $@
report_lean.csv report_lean_rbmap.csv: bench_lean
BENCHES=$(subst $(space),:,$(LEAN_BENCHES)) CATS=$(subst $(space),:,$(LEAN_CATS)) ./report.py report_lean
column -s';' -t < $@
report_cross.csv: bench_cross
BENCHES=$(subst $(space),:,$(CROSS_BENCHES)) CATS=$(subst $(space),:,$(CROSS_CATS)) ./report.py > $@
report_cross.csv report_cross_rbmap.csv: bench_cross
BENCHES=$(subst $(space),:,$(CROSS_BENCHES)) CATS=$(subst $(space),:,$(CROSS_CATS)) ./report.py report_cross
column -s';' -t < $@
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/$$/\\\\/'

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

@ -1,32 +0,0 @@
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/include/lean/lean.h | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index 6b37fd91a..c53137860 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/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

25
tests/bench/flake.lock generated
View file

@ -1,5 +1,17 @@
{
"nodes": {
"disable-st": {
"flake": false,
"locked": {
"narHash": "sha256-8Wlf9O+YRInYJdN9ydBGh5vaYAqESpZ4Kn0BvxivYog=",
"type": "file",
"url": "https://github.com/Kha/lean4/commit/no-st.patch"
},
"original": {
"type": "file",
"url": "https://github.com/Kha/lean4/commit/no-st.patch"
}
},
"flake-utils": {
"locked": {
"lastModified": 1656928814,
@ -38,14 +50,14 @@
"nixpkgs": "nixpkgs_2"
},
"locked": {
"lastModified": 0,
"narHash": "sha256-BfyPrBC8uxFmK08pnWd6+fSOl8MAct4mpi0rTypoyrU=",
"path": "/nix/store/y2cgjkc355yma96gjrai3lhbi18klgwx-source",
"type": "path"
"lastModified": 1674199151,
"narHash": "sha256-IASus2xsMhew5BIm54h1DOL57t/VS0/OszWUWTRfU9A=",
"type": "git",
"url": "file:../.."
},
"original": {
"path": "/nix/store/y2cgjkc355yma96gjrai3lhbi18klgwx-source",
"type": "path"
"type": "git",
"url": "file:../.."
}
},
"lean4-mode": {
@ -182,6 +194,7 @@
},
"root": {
"inputs": {
"disable-st": "disable-st",
"flake-utils": [
"lean",
"flake-utils"

60
tests/bench/flake.nix
View file

@ -1,9 +1,11 @@
{
inputs.lean.url = "../..";
inputs.lean.url = "git+file:../..";
inputs.flake-utils.url = github:numtide/flake-utils;
inputs.flake-utils.follows = "lean/flake-utils";
inputs.temci.url = github:Kha/temci;
inputs.nixpkgs.url = github:NixOS/nixpkgs/nixpkgs-unstable;
inputs.disable-st.url = https://github.com/Kha/lean4/commit/no-st.patch;
inputs.disable-st.flake = false;
outputs = inputs: inputs.flake-utils.lib.eachDefaultSystem (system: { packages = rec {
leanPkgs = inputs.lean.packages.${system};
@ -40,22 +42,6 @@
src = ./.;
LEAN_BIN = "${leanPkgs.lean-all}/bin";
#LEAN_GCC_BIN = "${lean { stdenv = pkgs.gcc9Stdenv; }}/bin";
#LEAN_NO_REUSE_BIN = "${lean.overrideAttrs (attrs: {
# prePatch = ''
#substituteInPlace src/Lean/Compiler/IR.lean --replace "decls.map Decl.insertResetReuse" "decls"
# '';
# buildFlags = [ "stage1.5" ];
# installFlags = [ "-C stage1.5" ];
#})}/bin";
#LEAN_NO_BORROW_BIN = "${lean.overrideAttrs (attrs: {
# prePatch = ''
#substituteInPlace src/Lean/Compiler/IR.lean --replace "inferBorrow" "pure"
# '';
# buildFlags = [ "stage1.5" ];
# installFlags = [ "-C stage1.5" ];
#})}/bin";
#LEAN_NO_ST_BIN = "${lean.overrideAttrs (attrs: { patches = [ ./disable-st.patch ]; })}/bin";
PARSER_TEST_FILE = ../../src/Init/Core.lean;
GHC = "${ghc}/bin/ghc";
OCAML = "${ocaml}/bin/ocamlopt.opt";
#OCAML_FLAMBDA = "${ocamlFlambda}/bin/ocamlopt.opt";
@ -80,5 +66,45 @@
cp -r report *.csv $out
'';
};
lean-variants = pkgs.stdenv.mkDerivation rec {
name = "lean_bench";
src = ./.;
LEAN_BIN = "${leanPkgs.lean-all}/bin";
LEAN_NO_REUSE_BIN = "${(leanPkgs.override (args: {
src = pkgs.runCommand "lean-no-reuse-src" {} ''
cp -r ${args.src} $out
substituteInPlace $out/src/Lean/Compiler/IR.lean --replace "decls.map Decl.insertResetReuse" "decls"
'';
})).stage2.lean-all}/bin";
LEAN_NO_BORROW_BIN = "${(leanPkgs.override (args: {
src = pkgs.runCommand "lean-no-borrow-src" {} ''
cp -r ${args.src} $out
substituteInPlace $out/src/Lean/Compiler/IR.lean --replace "inferBorrow" "pure"
'';
})).stage2.lean-all}/bin";
LEAN_NO_ST_BIN = "${(leanPkgs.override (args: {
src = pkgs.runCommand "lean-no-st-src" {} ''
cp -r ${args.src} $out
chmod -R u+w $out
cd $out
patch -p1 < ${inputs.disable-st}
'';
})).lean-all}/bin";
PARSER_TEST_FILE = ../../src/Init/Prelude.lean;
buildInputs = with pkgs; [
((builtins.elemAt temci.nativeBuildInputs 0).withPackages (ps: [ temci ps.numpy ps.pyyaml ]))
temci
pkgs.linuxPackages.perf time unixtools.column
];
patchPhase = ''
patchShebangs .
'';
makeFlags = [ "report_lean.csv" ];
installPhase = ''
mkdir $out
cp -r report *.csv $out
'';
};
};});
}

8
tests/bench/parser.lean Normal file
View file

@ -0,0 +1,8 @@
import Lean.Parser.Module
def main : List String → IO Unit
| [fname, n] => do
let env ← Lean.mkEmptyEnvironment
for _ in [0:n.toNat!] do
discard $ Lean.Parser.testParseFile env fname
| _ => throw $ IO.userError "give file"

21
tests/bench/report.py
View file

@ -20,7 +20,10 @@ def single(bench, cat, prop):
runs = yaml.load(f, Loader=yaml.CLoader)
stats_helper = rundata.RunDataStatsHelper.init_from_dicts(runs)
stat = stats.TestedPairsAndSingles(stats_helper.valid_runs())
return stat.singles[0].properties[prop]
if stat.singles:
return stat.singles[0].properties[prop]
else:
raise Exception(f"failed to parse {f}")
mean_by_cat = collections.defaultdict(list)
stddev_by_cat = collections.defaultdict(list)
@ -71,10 +74,16 @@ CATBAG = {
benches = os.environ['BENCHES'].split(':')
cats = os.environ['CATS'].split(':')
print(";".join(["Benchmark"] + [f'{CATBAG[cat][0]};{CATBAG[cat][0]} std' for cat in cats]))
for bench in benches:
norm = single('rbmap' if bench.startswith('rbmap') else bench, '.lean', 'etime').mean()
print(";".join([bench] + [pp(bench, cat, CATBAG[cat][1], norm) for cat in cats]))
# create one file without rbmap_ benchmarks, one without only rbmap and normed by rbmap_1
for sfx in ['', '_rbmap']:
f = open(sys.argv[1] + sfx + '.csv', 'w')
print(";".join(["Benchmark"] + [f'{CATBAG[cat][0]};{CATBAG[cat][0]} std' for cat in cats]), file=f)
print(";".join(["geom. mean"] + [mean(cat, CATBAG[cat][1]) for cat in cats]))
for bench in benches:
if sfx == '' and bench.startswith('rbmap_') or sfx == '_rbmap' and not bench.startswith('rbmap'):
continue
norm = single('rbmap_1' if bench.startswith('rbmap') and sfx == '_rbmap' else bench, '.lean', 'etime').mean()
print(";".join([bench] + [pp(bench, cat, CATBAG[cat][1], norm) for cat in cats]), file=f)
print(";".join(["geom. mean"] + [mean(cat, CATBAG[cat][1]) for cat in cats]), file=f)