sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore: update benchmark suite

Browse Source
This commit is contained in:
Sebastian Ullrich
2022-05-25 13:35:23 +02:00
parent 794877c0c8
commit 4a1885f997
14 changed files with 311 additions and 142 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
.github/workflows/ci.yml vendored
View File

@@ -211,7 +211,8 @@ jobs:
run: |
echo -1 | sudo tee /proc/sys/kernel/perf_event_paranoid
export BUILD=$PWD/build PATH=$PWD/build/stage1/bin:$PATH
nix-shell -A with-temci --run "cd tests/bench; temci exec --config speedcenter.yaml --included_blocks fast --runs 1"
cd tests/bench
nix shell .#temci -c temci exec --config speedcenter.yaml --included_blocks fast --runs 1
if: matrix.test-speedcenter
- name: Check rebootstrap
run: |

27
doc/flake.lock generated
View File

@@ -38,12 +38,11 @@
"lean-stage0": "lean-stage0",
"lean4-mode": "lean4-mode",
"nix": "nix",
"nixpkgs": "nixpkgs_2",
"temci": "temci"
"nixpkgs": "nixpkgs_2"
},
"locked": {
"lastModified": 0,
"narHash": "sha256-zrFCATQSmNX0u+2R2wnizOigxGOiaRzfplhKu9c1MgA=",
"narHash": "sha256-AfBkKX6Ahb9YbZke+eWLmsUk1Z9BwdJ1CpIoPY8Msx8=",
"path": "../.",
"type": "path"
},
@@ -183,11 +182,11 @@
},
"nixpkgs_2": {
"locked": {
"lastModified": 1647350163,
"narHash": "sha256-OcMI+PFEHTONthXuEQNddt16Ml7qGvanL3x8QOl2Aao=",
"lastModified": 1648219316,
"narHash": "sha256-Ctij+dOi0ZZIfX5eMhgwugfvB+WZSrvVNAyAuANOsnQ=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "3eb07eeafb52bcbf02ce800f032f18d666a9498d",
"rev": "30d3d79b7d3607d56546dd2a6b49e156ba0ec634",
"type": "github"
},
"original": {
@@ -208,22 +207,6 @@
"leanInk-src": "leanInk-src",
"mdBook": "mdBook"
}
},
"temci": {
"flake": false,
"locked": {
"lastModified": 1638195132,
"narHash": "sha256-1DSg4Qr5h54wLrKpZfpkArhFXDFLdO57PiYUMk+7FSc=",
"owner": "parttimenerd",
"repo": "temci",
"rev": "a8d78cb52c248f1ae3f2469bbd0916b14ac9ea84",
"type": "github"
},
"original": {
"owner": "parttimenerd",
"repo": "temci",
"type": "github"
}
}
},
"root": "root",

19
flake.lock generated
View File

@@ -134,24 +134,7 @@
"lean-stage0": "lean-stage0",
"lean4-mode": "lean4-mode",
"nix": "nix",
"nixpkgs": "nixpkgs_2",
"temci": "temci"
}
},
"temci": {
"flake": false,
"locked": {
"lastModified": 1638195132,
"narHash": "sha256-1DSg4Qr5h54wLrKpZfpkArhFXDFLdO57PiYUMk+7FSc=",
"owner": "parttimenerd",
"repo": "temci",
"rev": "a8d78cb52c248f1ae3f2469bbd0916b14ac9ea84",
"type": "github"
},
"original": {
"owner": "parttimenerd",
"repo": "temci",
"type": "github"
"nixpkgs": "nixpkgs_2"
}
}
},

9
flake.nix
View File

@@ -3,10 +3,6 @@
inputs.nixpkgs.url = github:NixOS/nixpkgs/nixpkgs-unstable;
inputs.flake-utils.url = github:numtide/flake-utils;
inputs.temci = {
url = github:parttimenerd/temci;
flake = false;
};
inputs.nix.url = github:NixOS/nix;
inputs.lean4-mode = {
url = github:leanprover/lean4-mode;
@@ -17,19 +13,18 @@
url = github:leanprover/lean4;
inputs.nixpkgs.follows = "nixpkgs";
inputs.flake-utils.follows = "flake-utils";
inputs.temci.follows = "temci";
inputs.nix.follows = "nix";
inputs.lean4-mode.follows = "lean4-mode";
};
outputs = { self, nixpkgs, flake-utils, temci, nix, lean4-mode, lean-stage0 }: flake-utils.lib.eachDefaultSystem (system:
outputs = { self, nixpkgs, flake-utils, nix, lean4-mode, lean-stage0 }: flake-utils.lib.eachDefaultSystem (system:
let
pkgs = import nixpkgs {
inherit system;
# for `vscode-with-extensions`
config.allowUnfree = true;
};
lean-packages = pkgs.callPackage (./nix/packages.nix) { inherit nix temci lean4-mode; };
lean-packages = pkgs.callPackage (./nix/packages.nix) { inherit nix lean4-mode; };
in {
packages = lean-packages // rec {
debug = lean-packages.override { debug = true; };

3
nix/packages.nix
View File

@@ -1,4 +1,4 @@
{ pkgs, nix, temci, ... } @ args:
{ pkgs, nix, ... } @ args:
with pkgs;
let
nix-pinned = writeShellScriptBin "nix" ''
@@ -72,7 +72,6 @@ in {
stage0print-paths = lean.stage1.Lean.print-paths;
HEAD-as-stage0 = (lean.stage1.Lean.overrideArgs { srcTarget = "..#stage0-from-input.stage0"; srcArgs = "(--override-input lean-stage0 ..\?rev=$(git rev-parse HEAD) -- -Dinterpreter.prefer_native=false \"$@\")"; });
HEAD-as-stage1 = (lean.stage1.Lean.overrideArgs { srcTarget = "..\?rev=$(git rev-parse HEAD)#stage0"; });
temci = (import temci {}).override { doCheck = false; };
nix = nix-pinned;
nixpkgs = pkgs;
ciShell = writeShellScriptBin "ciShell" ''

3
shell.nix
View File

@@ -21,8 +21,5 @@ in { pkgs ? flakePkgs.nixpkgs, pkgsDist ? pkgs }:
GLIBC_DEV = pkgsDist.glibc.dev;
ZLIB = pkgsDist.zlib;
});
with-temci = shell.overrideAttrs (old: {
buildInputs = old.buildInputs ++ [ flakePkgs.temci ];
});
nix = flake.devShell.${builtins.currentSystem};
}

4
tests/bench/README.md
View File

@@ -40,7 +40,7 @@ We recommend using [Nix](https://nixos.org/nix/) for building/obtaining all Lean
compilers in a reproducible way. After installing Nix, running the benchmarks is as easy as
```
nix-shell cross.nix --pure --run make
nix shell -c make
```
This will record 50 runs for each benchmark configuration (this can be changed with `runs` in `cross.yaml`),
@@ -51,7 +51,7 @@ In order to reduce noise in the benchmarking data, you may instead want to try c
temci shell:
```
nix-shell cross.nix --pure --run "temci short shell --sudo --preset usable --cpuset_active make"
nix shell -c temci short shell --sudo --preset usable --cpuset_active make
```
Using root powers, this will temporarily configure your machine similarly to the

74
tests/bench/cross.nix
View File

@@ -1,74 +0,0 @@
{ pkgs ? import ./nixpkgs.nix }:
let
# pin Lean commit to avoid rebuilds
# 2020-08-18
lean = import (builtins.fetchGit { url = ../../.; rev = "d059d28c220247d51310c4ea437807c3446d36d7"; }) {};
# for binarytrees.hs
ghcPackages = p: [ p.parallel ];
ghc = pkgs.haskell.packages.ghc884.ghcWithPackages ghcPackages; #.override { withLLVM = true; };
ocaml = pkgs.ocaml-ng.ocamlPackages_4_11.ocaml;
# note that this will need to be compiled from source
ocamlFlambda = ocaml.override { flambdaSupport = true; };
mlton = pkgs.mlton;
mlkit = pkgs.stdenv.mkDerivation {
name = "mlkit";
src = builtins.fetchTarball {
url = "https://github.com/melsman/mlkit/releases/download/v4.5.0/mlkit_bin_dist.tgz";
sha256 = "1nrk2klhrr2xcm83y601w6dffl756qfk4kgvn3rkjlp7b2i8r8mr";
};
buildInputs = [ pkgs.makeWrapper ];
dontBuild = true;
installPhase = ''
mkdir $out
cp -R . $out
'';
preFixup = ''
wrapProgram $out/bin/mlkit --set PATH ${pkgs.binutils}/bin:${pkgs.gcc}/bin\
--set SML_LIB $out/lib/mlkit
'';
};
swift = pkgs.swift;
temci = import (builtins.fetchGit { url = http://github.com/parttimenerd/temci.git; rev = "64eca12970e8096aa20557c35fd089dd6c668e1b"; }) { inherit pkgs; };
in pkgs.stdenv.mkDerivation rec {
name = "bench";
src = pkgs.lib.sourceFilesBySuffices ./. ["Makefile" "temci.yaml" ".py" ".lean" ".hs" ".ml" ".sml"];
LEAN_BIN = "${lean}/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 = lean.src + "/src/Init/Core.lean";
GHC = "${ghc}/bin/ghc";
OCAML = "${ocaml}/bin/ocamlopt.opt";
#OCAML_FLAMBDA = "${ocamlFlambda}/bin/ocamlopt.opt";
MLTON_BIN = "${mlton}/bin";
MLKIT = "${mlkit}/bin/mlkit";
SWIFTC = "${swift}/bin/swiftc";
TEMCI = "${temci}/bin/temci";
buildInputs = with pkgs; [
gmp # needed by leanc
(python37.withPackages (ps: [ temci ps.numpy ps.pyyaml ]))
temci
pkgs.linuxPackages.perf time unixtools.column
];
patchPhase = ''
patchShebangs .
'';
installPhase = ''
mkdir $out
cp -r report *.csv $out
'';
}

230
tests/bench/flake.lock generated Normal file
View File

@@ -0,0 +1,230 @@
{
"nodes": {
"flake-utils": {
"locked": {
"lastModified": 1644229661,
"narHash": "sha256-1YdnJAsNy69bpcjuoKdOYQX0YxZBiCYZo4Twxerqv7k=",
"owner": "numtide",
"repo": "flake-utils",
"rev": "3cecb5b042f7f209c56ffd8371b2711a290ec797",
"type": "github"
},
"original": {
"owner": "numtide",
"repo": "flake-utils",
"type": "github"
}
},
"flake-utils_2": {
"locked": {
"lastModified": 1652776076,
"narHash": "sha256-gzTw/v1vj4dOVbpBSJX4J0DwUR6LIyXo7/SuuTJp1kM=",
"owner": "numtide",
"repo": "flake-utils",
"rev": "04c1b180862888302ddfb2e3ad9eaa63afc60cf8",
"type": "github"
},
"original": {
"owner": "numtide",
"repo": "flake-utils",
"type": "github"
}
},
"lean": {
"inputs": {
"flake-utils": "flake-utils",
"lean-stage0": "lean-stage0",
"lean4-mode": "lean4-mode",
"nix": "nix",
"nixpkgs": "nixpkgs_2"
},
"locked": {
"lastModified": 0,
"narHash": "sha256-nq2EfMIMM60Gn/Q9YWXynLPWf2S/cHqmqFPUyFyoyJA=",
"path": "/nix/store/p76zgzp8v8fih1xgkiv6s36y86jjhfd3-source",
"type": "path"
},
"original": {
"path": "/nix/store/p76zgzp8v8fih1xgkiv6s36y86jjhfd3-source",
"type": "path"
}
},
"lean-stage0": {
"locked": {
"lastModified": 0,
"narHash": "sha256-3K/43lSW4WIHNG+HHVKCD1odS63mHuaQ4ueHyTIkcls=",
"owner": "leanprover",
"repo": "lean4",
"rev": "0000000000000000000000000000000000000000",
"type": "github"
},
"original": {
"owner": "leanprover",
"repo": "lean4",
"type": "github"
}
},
"lean4-mode": {
"flake": false,
"locked": {
"lastModified": 1647694750,
"narHash": "sha256-0rV61KhevG9IAjZDN2Ts2VS65fiUAPAezbf282u7yy8=",
"owner": "leanprover",
"repo": "lean4-mode",
"rev": "c016c7aeee92564836355083664c49ed57024427",
"type": "github"
},
"original": {
"owner": "leanprover",
"repo": "lean4-mode",
"type": "github"
}
},
"lowdown-src": {
"flake": false,
"locked": {
"lastModified": 1633514407,
"narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
"owner": "kristapsdz",
"repo": "lowdown",
"rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
"type": "github"
},
"original": {
"owner": "kristapsdz",
"repo": "lowdown",
"type": "github"
}
},
"nix": {
"inputs": {
"lowdown-src": "lowdown-src",
"nixpkgs": "nixpkgs",
"nixpkgs-regression": "nixpkgs-regression"
},
"locked": {
"lastModified": 1648022028,
"narHash": "sha256-HtwmifW6STPcym+3uJ4YavgTKTYVIoiQHg3f0wXOm+Q=",
"owner": "NixOS",
"repo": "nix",
"rev": "98ce1a21b7d959c5575fac566c8699e91703a9f7",
"type": "github"
},
"original": {
"owner": "NixOS",
"repo": "nix",
"type": "github"
}
},
"nixpkgs": {
"locked": {
"lastModified": 1632864508,
"narHash": "sha256-d127FIvGR41XbVRDPVvozUPQ/uRHbHwvfyKHwEt5xFM=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "82891b5e2c2359d7e58d08849e4c89511ab94234",
"type": "github"
},
"original": {
"id": "nixpkgs",
"ref": "nixos-21.05-small",
"type": "indirect"
}
},
"nixpkgs-regression": {
"locked": {
"lastModified": 1643052045,
"narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
"type": "github"
},
"original": {
"id": "nixpkgs",
"rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
"type": "indirect"
}
},
"nixpkgs_2": {
"locked": {
"lastModified": 1652840887,
"narHash": "sha256-gEK4NNa4GwIgTZE63kt/4WTFAWRTJVSa30+h4ZjFh9U=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "52dc75a4fee3fdbcb792cb6fba009876b912bfe0",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixpkgs-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs_3": {
"locked": {
"lastModified": 1652840887,
"narHash": "sha256-gEK4NNa4GwIgTZE63kt/4WTFAWRTJVSa30+h4ZjFh9U=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "52dc75a4fee3fdbcb792cb6fba009876b912bfe0",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixpkgs-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"root": {
"inputs": {
"flake-utils": [
"lean",
"flake-utils"
],
"lean": "lean",
"swiftPkgs": "swiftPkgs",
"temci": "temci"
}
},
"swiftPkgs": {
"locked": {
"lastModified": 1647381949,
"narHash": "sha256-wMoRFm2siM1+6T2J6wczAbICmhQojBGZL2LJM15/Sj4=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "007ccf2f4f1da567903ae392cbf19966eb30cf20",
"type": "github"
},
"original": {
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "007ccf2f4f1da567903ae392cbf19966eb30cf20",
"type": "github"
}
},
"temci": {
"inputs": {
"flake-utils": "flake-utils_2",
"nixpkgs": "nixpkgs_3"
},
"locked": {
"lastModified": 1653036219,
"narHash": "sha256-l57O/lEUUhkw1cPv4LO7hOXFdJb44ulcipnKzM4XgIU=",
"owner": "Kha",
"repo": "temci",
"rev": "b096730b510fc5520cb9de90f854202ffb62a315",
"type": "github"
},
"original": {
"owner": "Kha",
"repo": "temci",
"type": "github"
}
}
},
"root": "root",
"version": 7
}

65
tests/bench/flake.nix Normal file
View File

@@ -0,0 +1,65 @@
{
inputs.lean.url = "../..";
inputs.flake-utils.url = github:numtide/flake-utils;
inputs.flake-utils.follows = "lean/flake-utils";
inputs.temci.url = github:Kha/temci;
inputs.swiftPkgs.url = github:NixOS/nixpkgs/007ccf2f4f1da567903ae392cbf19966eb30cf20;
outputs = inputs: inputs.flake-utils.lib.eachDefaultSystem (system: { packages = rec {
leanPkgs = inputs.lean.packages.${system};
pkgs = leanPkgs.nixpkgs;
# for binarytrees.hs
ghcPackages = p: [ p.parallel ];
ghc = pkgs.haskell.packages.ghc921.ghcWithPackages ghcPackages; #.override { withLLVM = true; };
ocaml = pkgs.ocaml; # pkgs.ocaml-ng.ocamlPackages_latest.ocaml;
# note that this will need to be compiled from source
ocamlFlambda = ocaml.override { flambdaSupport = true; };
mlton = pkgs.mlton;
mlkit = pkgs.mlkit;
swift = inputs.swiftPkgs.legacyPackages.${system}.swift; # pkgs.swift;
temci = inputs.temci.packages.${system}.default.override { doCheck = false; };
default = pkgs.stdenv.mkDerivation rec {
name = "bench";
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";
MLTON_BIN = "${mlton}/bin";
MLKIT = "${mlkit}/bin/mlkit";
SWIFTC = "${swift}/bin/swiftc";
TEMCI = "${temci}/bin/temci";
buildInputs = with pkgs; [
(python3.withPackages (ps: [ temci ps.numpy ps.pyyaml ]))
temci
pkgs.linuxPackages.perf time unixtools.column
];
patchPhase = ''
patchShebangs .
'';
makeFlags = [ "report_cross.csv" ];
installPhase = ''
mkdir $out
cp -r report *.csv $out
'';
};
};});
}

7
tests/bench/nixpkgs.nix
View File

@@ -1,7 +0,0 @@
import (builtins.fetchTarball {
name = "nixpkgs-unstable-2020-08-18";
# Commit hash from `git ls-remote https://github.com/NixOS/nixpkgs-channels nixpkgs-unstable`
url = https://github.com/nixos/nixpkgs/archive/c5815280e92112a25d958a2ec8b3704d7d90c506.tar.gz;
# Hash obtained using `nix-prefetch-url --unpack <url>`
sha256 = "09ic4s9s7w3lm0gmcxszm5j20cfv4n5lfvhdvgi7jzdbbbdps1nh";
}) {}

2
tests/bench/perf.py
View File

@@ -2,7 +2,7 @@
import sys
[misses, wall_secs] = sys.stdin.readlines()
[misses, wall_secs] = sys.stdin.readlines()[-2:]
misses = int(misses.split(';')[0])
wall_secs = float(wall_secs)
print(f"cache-misses: {misses*1e-6/wall_secs}")

5
tests/bench/qsort.hs
View File

@@ -74,9 +74,6 @@ main = do
forM_ [0..n-1] $ \_ ->
forM_ [0..n-1] $ \i -> do
let xs = mkRandomArray (toEnum i) i
let xs' = runSTArray (do
mxs <- thaw xs
qsort mxs
pure mxs)
let xs' = runSTArray (do mxs <- thaw xs; qsort mxs; pure mxs)
--print xs'
checkSortedAux xs' 0

2
tests/bench/report.py
View File

@@ -17,7 +17,7 @@ settings.Settings().load_file("cross.yaml")
def single(bench, cat, prop):
f = f"bench/{bench}{cat}.bench"
with open(f, "r") as f:
runs = yaml.load(f)
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]