feat(default.nix,tests/playground): Nix-powered benchmark suite
This commit is contained in:
Sebastian Ullrich
parent
8ab15536a7
commit
e0b45d65f7
7 changed files with 197 additions and 33 deletions
1
.gitignore
vendored
1
.gitignore
vendored
|
|
@ -20,7 +20,6 @@ tasks.json
|
|||
settings.json
|
||||
.gdb_history
|
||||
.vscode
|
||||
/*.nix
|
||||
*.produced.out
|
||||
CMakeSettings.json
|
||||
CppProperties.json
|
||||
|
|
|
|||
27
default.nix
Normal file
27
default.nix
Normal file
|
|
@ -0,0 +1,27 @@
|
|||
{ stdenv, cmake, python, gmp }:
|
||||
|
||||
stdenv.mkDerivation rec {
|
||||
name = "lean-${version}";
|
||||
version = "local";
|
||||
|
||||
# I have way too many untracked files in my checkout
|
||||
src = builtins.fetchGit { url = ./.; };
|
||||
|
||||
nativeBuildInputs = [ cmake python ];
|
||||
buildInputs = [ gmp ];
|
||||
enableParallelBuilding = true;
|
||||
|
||||
preConfigure = ''
|
||||
cd src
|
||||
'';
|
||||
postConfigure = ''
|
||||
patchShebangs ../../bin
|
||||
'';
|
||||
|
||||
meta = with stdenv.lib; {
|
||||
description = "Automatic and interactive theorem prover";
|
||||
homepage = https://leanprover.github.io/;
|
||||
license = licenses.asl20;
|
||||
platforms = platforms.unix;
|
||||
};
|
||||
}
|
||||
|
|
@ -1,49 +1,74 @@
|
|||
#BENCH=./bad_bench
|
||||
BENCH=bench
|
||||
## CONFIG
|
||||
|
||||
BENCH=ulimit -s unlimited && bench
|
||||
CROSS_BENCHES = binarytrees deriv expr_const_folding rbmap
|
||||
|
||||
# basic version usable without Nix
|
||||
#CROSS_CATS = .lean .hs .llvm.hs .ml
|
||||
CROSS_CATS = .lean .gcc.lean .hs .llvm.hs .ml .flambda.ml
|
||||
|
||||
GHC_FLAGS = -O3
|
||||
OCAML_FLAGS = -O3
|
||||
|
||||
## IMPLEMENTATION
|
||||
|
||||
LEAN_BIN ?= ../../bin
|
||||
GHC ?= ghc
|
||||
OCAML ?= ocamlopt.opt
|
||||
|
||||
.PRECIOUS: %.out bench/%
|
||||
.DELETE_ON_ERROR:
|
||||
|
||||
all: report_cross.csv
|
||||
|
||||
# make gets confused by the .cpp files otherwise
|
||||
%.lean: ;
|
||||
|
||||
%.lean.out: %.lean ../compiler/test_flags.sh
|
||||
./compile.sh $<
|
||||
%.lean.cpp: %.lean
|
||||
$(LEAN_BIN)/lean --cpp=$<.cpp $<
|
||||
%.lean.out: %.lean.cpp
|
||||
$(LEAN_BIN)/leanc -o $@ $<
|
||||
# Binaries x.lean.out and x.gcc.lean.out etc. are produced by the
|
||||
# same rules and x.lean source file by copying the latter to
|
||||
# x.gcc.lean. This also avoids conflicts between intermediate
|
||||
# files of the two binaries.
|
||||
%.gcc.lean.out: LEAN_BIN = $(LEAN_GCC_BIN)
|
||||
%.gcc.lean: %.lean; ln $< $@
|
||||
|
||||
%.hs.out: %.hs
|
||||
ghc -fllvm -O3 $< -o $<.out
|
||||
$(GHC) $(GHC_FLAGS) $< -o $@
|
||||
%.llvm.hs.out: GHC_FLAGS += -fllvm
|
||||
%.llvm.hs: %.hs; ln $< $@
|
||||
|
||||
binarytrees.hs: binarytrees.ghc-6.hs; ln $< $@
|
||||
# NOTE: changed `-N4` rtsopt to `-N` to be less system-dependent
|
||||
binarytrees%hs.out: GHC_FLAGS += --make -O2 -XBangPatterns -dynamic -threaded -rtsopts -with-rtsopts='-N -K128M -H'
|
||||
|
||||
%.ml.out: %.ml
|
||||
ocamlopt -O3 $< -o $<.out
|
||||
$(OCAML) $(OCAML_FLAGS) $< -o $@
|
||||
%.flambda.ml.out: OCAML = $(OCAML_FLAMBDA)
|
||||
%.flambda.ml: %.ml; ln $< $@
|
||||
|
||||
binarytrees.hs.out: binarytrees.ghc-6.hs
|
||||
ghc --make -fllvm -O2 -XBangPatterns -dynamic -threaded -rtsopts binarytrees.ghc-6.hs -o binarytrees.hs.out
|
||||
binarytrees.ml: binarytrees.ocaml-2.ml; ln $< $@
|
||||
binarytrees%ml.out: OCAML_FLAGS = -noassert -unsafe -fPIC -nodynlink -inline 100 -O3 unix.cmxa
|
||||
|
||||
run_binarytrees.hs.out: binarytrees.hs.out
|
||||
time ./binarytrees.hs.out +RTS -N4 -K128M -H -RTS 21
|
||||
bench:
|
||||
-@mkdir bench
|
||||
|
||||
binarytrees.ml.out: binarytrees.ocaml-2.ml
|
||||
ocamlopt -noassert -unsafe -fPIC -nodynlink -inline 100 -O3 unix.cmxa binarytrees.ocaml-2.ml -o binarytrees.ml.out
|
||||
bench/%.bench: %.out | bench
|
||||
$(BENCH) "./$< $(BENCH_PARAMS)" --json $@
|
||||
|
||||
run_binarytrees.ml.out: binarytrees.ml.out
|
||||
time ./binarytrees.ml.out 21
|
||||
bench/binarytrees.%.bench: BENCH_PARAMS = 21
|
||||
|
||||
run_binarytrees.lean.out: binarytrees.lean.out
|
||||
time ./binarytrees.lean.out 21
|
||||
bench/rbmap.%.bench: BENCH_PARAMS = 7000000
|
||||
|
||||
bench_deriv: deriv.lean.out deriv.hs.out deriv.ml.out
|
||||
$(BENCH) ./deriv.lean.out ./deriv.hs.out ./deriv.ml.out
|
||||
bench_cross: $(foreach bench,$(CROSS_BENCHES), $(foreach cat, $(CROSS_CATS), bench/$(bench)$(cat).bench))
|
||||
|
||||
bench_binarytrees: binarytrees.lean.out binarytrees.hs.out binarytrees.ml.out
|
||||
$(BENCH) "make run_binarytrees.lean.out" "make run_binarytrees.hs.out" "make run_binarytrees.ml.out"
|
||||
# yes.
|
||||
space = $() $()
|
||||
|
||||
bench_expr_const_folding: expr_const_folding.lean.out expr_const_folding.hs.out expr_const_folding.ml.out
|
||||
$(BENCH) ./expr_const_folding.lean.out ./expr_const_folding.hs.out ./expr_const_folding.ml.out
|
||||
report_cross.csv: bench_cross report.py
|
||||
BENCHES=$(subst $(space),:,$(CROSS_BENCHES)) CATS=$(subst $(space),:,$(CROSS_CATS)) ./report.py > $@
|
||||
|
||||
bench_rbmap: rbmap.lean.out rbmap.hs.out rbmap.ml.out
|
||||
$(BENCH) "./rbmap.lean.out 7000000" "./rbmap.hs.out 7000000" "./rbmap.ml.out 7000000"
|
||||
|
||||
bench_all: bench_deriv bench_binarytrees bench_expr_const_folding bench_rbmap
|
||||
|
||||
run_frontend:
|
||||
cd ../.. && time bin/lean --new-frontend library/init/core.lean
|
||||
|
||||
bench_lean: deriv.lean.out expr_const_folding.lean.out rbmap.lean.out binarytrees.lean.out ../../bin/lean unionfind1.lean.out unionfind2.lean.out
|
||||
$(BENCH) ./deriv.lean.out ./expr_const_folding.lean.out "./rbmap.lean.out 7000000" "./binarytrees.lean.out 21" "make run_frontend" "./unionfind1.lean.out 3000000" "./unionfind2.lean.out 3000000"
|
||||
clean:
|
||||
-rm *.out bench/*
|
||||
|
|
|
|||
50
tests/playground/bench.nix
Normal file
50
tests/playground/bench.nix
Normal file
|
|
@ -0,0 +1,50 @@
|
|||
{ pkgs ? import ./nixpkgs.nix }:
|
||||
|
||||
let
|
||||
lean = { cmakeFlags ? "", stdenv ? pkgs.llvmPackages_7.stdenv }:
|
||||
(pkgs.callPackage ../../default.nix { inherit stdenv; }).overrideAttrs (attrs: {
|
||||
inherit cmakeFlags;
|
||||
# pin Lean commit to avoid rebuilds
|
||||
# 2019-05-12
|
||||
src = builtins.fetchGit { url = ../../.; rev = "de5b68f1262214eecf3d59d7540ed0e9447edf7b"; };
|
||||
});
|
||||
# for binarytrees.hs
|
||||
ghcPackages = p: [ p.parallel ];
|
||||
ghc = (pkgs.haskellPackages.ghcWithPackages ghcPackages).override {
|
||||
ghc = pkgs.haskell.compiler.ghc865;
|
||||
withLLVM = true;
|
||||
};
|
||||
ocaml = pkgs.ocaml-ng.ocamlPackages_4_07.ocaml;
|
||||
# note that this will need to be compiled from source
|
||||
ocamlFlambda = ocaml.override { flambdaSupport = true; };
|
||||
in pkgs.stdenv.mkDerivation rec {
|
||||
name = "bench";
|
||||
LEAN_BIN = "${lean {}}/bin";
|
||||
LEAN_GCC_BIN = "${lean { stdenv = pkgs.gcc9Stdenv; }}/bin";
|
||||
GHC = "${ghc}/bin/ghc";
|
||||
OCAML = "${ocaml}/bin/ocamlopt.opt";
|
||||
OCAML_FLAMBDA = "${ocamlFlambda}/bin/ocamlopt.opt";
|
||||
buildInputs = with pkgs; [ bench gmp python3 ];
|
||||
buildCommand = ''
|
||||
make
|
||||
mkdir $out
|
||||
cp *.csv $out
|
||||
'';
|
||||
#in {
|
||||
# buildLean = { name, src, cmakeFlags ? "", leancFlags ? "-O3" }: pkgs.stdenv.mkDerivation {
|
||||
# inherit name src;
|
||||
# buildCommand = "${lean cmakeFlags}/bin/lean --cpp=$src.cpp $src && ${lean cmakeFlags}/bin/leanc $src.cpp -o $out";
|
||||
# };
|
||||
# buildHs = { name, src, opts, hsPkgs ? (p : []) }: pkgs.stdenv.mkDerivation {
|
||||
# inherit name src;
|
||||
# buildCommand = "${ghc hsPkgs}/bin/ghc ${opts} $src -o $out";
|
||||
# };
|
||||
# buildOCaml = { name, src, opts }: pkgs.stdenv.mkDerivation {
|
||||
# inherit name src;
|
||||
# buildCommand = "${ocaml}/bin/ocamlopt.opt ${opts} $src -o $out";
|
||||
# };
|
||||
# buildOCamlFlambda = { name, src, opts }: pkgs.stdenv.mkDerivation {
|
||||
# inherit name src;
|
||||
# buildCommand = "${ocamlFlambda}/bin/ocamlopt.opt ${opts} $src -o $out";
|
||||
# };
|
||||
}
|
||||
26
tests/playground/build.nix
Normal file
26
tests/playground/build.nix
Normal file
|
|
@ -0,0 +1,26 @@
|
|||
{ pkgs ? import ./nixpkgs.nix }:
|
||||
|
||||
let
|
||||
lean = cmakeFlags: (pkgs.callPackage ../../default.nix { stdenv = pkgs.llvmPackages_7.stdenv; }).overrideAttrs (_: { inherit cmakeFlags; });
|
||||
ghc = hsPkgs: (pkgs.haskellPackages.ghcWithPackages hsPkgs).override { ghc = pkgs.haskell.compiler.ghc865; withLLVM = true; };
|
||||
ocaml = pkgs.ocaml-ng.ocamlPackages_4_07.ocaml;
|
||||
# note that this will need to be compiled from source
|
||||
ocamlFlambda = ocaml.override { flambdaSupport = true; };
|
||||
in {
|
||||
buildLean = { name, src, cmakeFlags ? "", leancFlags ? "-O3" }: pkgs.stdenv.mkDerivation {
|
||||
inherit name src;
|
||||
buildCommand = "${lean cmakeFlags}/bin/lean --cpp=$src.cpp $src && ${lean cmakeFlags}/bin/leanc $src.cpp -o $out";
|
||||
};
|
||||
buildHs = { name, src, opts, hsPkgs ? (p : []) }: pkgs.stdenv.mkDerivation {
|
||||
inherit name src;
|
||||
buildCommand = "${ghc hsPkgs}/bin/ghc ${opts} $src -o $out";
|
||||
};
|
||||
buildOCaml = { name, src, opts }: pkgs.stdenv.mkDerivation {
|
||||
inherit name src;
|
||||
buildCommand = "${ocaml}/bin/ocamlopt.opt ${opts} $src -o $out";
|
||||
};
|
||||
buildOCamlFlambda = { name, src, opts }: pkgs.stdenv.mkDerivation {
|
||||
inherit name src;
|
||||
buildCommand = "${ocamlFlambda}/bin/ocamlopt.opt ${opts} $src -o $out";
|
||||
};
|
||||
}
|
||||
5
tests/playground/nixpkgs.nix
Normal file
5
tests/playground/nixpkgs.nix
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
import (builtins.fetchTarball {
|
||||
name = "nixpkgs-unstable-2019-05-08";
|
||||
url = https://github.com/NixOS/nixpkgs/archive/5964b3a2e21c9d9369b55bbf48dff71ff0671f25.tar.gz;
|
||||
sha256 = "1q3x73gzjm8xz3dxa3dkyb7m69aa75an0mnld62qyi4cyv6qmhw3";
|
||||
}) {}
|
||||
32
tests/playground/report.py
Executable file
32
tests/playground/report.py
Executable file
|
|
@ -0,0 +1,32 @@
|
|||
#!/usr/bin/env python3
|
||||
|
||||
import json
|
||||
import os
|
||||
import sys
|
||||
|
||||
CATBAG = {
|
||||
'.lean': "Lean",
|
||||
'.gcc.lean': "Lean+GCC9",
|
||||
'.hs': "GHC",
|
||||
'.llvm.hs': "GHC -fllvm",
|
||||
'.ml': "OCaml",
|
||||
'.flambda.ml': "OCaml+Flambda"
|
||||
}
|
||||
|
||||
benches = os.environ['BENCHES'].split(':')
|
||||
cats = os.environ['CATS'].split(':')
|
||||
print(";".join(["Benchmark"] + [CATBAG[cat] for cat in cats]))
|
||||
|
||||
def read(bench, cat):
|
||||
result = json.load(open(f"bench/{bench}{cat}.bench", 'r'))[2][0]['reportAnalysis']
|
||||
mean = result['anMean']['estPoint']
|
||||
stddev = result['anStdDev']['estPoint']
|
||||
return (mean, stddev)
|
||||
|
||||
def pp(bench, cat, norm):
|
||||
(mean, stddev) = read(bench, cat)
|
||||
return f"{mean/norm:.3} ± {stddev/norm:.3}"
|
||||
|
||||
for bench in benches:
|
||||
norm = read(bench, '.lean')[0]
|
||||
print(";".join([bench] + [pp(bench, cat, norm) for cat in cats]))
|
||||
Loading…
Add table
Reference in a new issue