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

chore: Nix: expose benchmarks as flake attributes for convenience

Browse source
This commit is contained in:
Sebastian Ullrich 2021-07-24 16:36:05 +02:00
parent 43190e0e63
commit 60e6130ece
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
nix/bootstrap.nix
View file

@ -1,6 +1,7 @@
{ debug ? false, stage0debug ? false, extraCMakeFlags ? [],
stdenv, lib, cmake, gmp, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir,
... } @ args:
with builtins;
rec {
inherit stdenv;
buildCMake = args: stdenv.mkDerivation ({
@ -130,6 +131,14 @@ rec {
${update-stage0}/bin/update-stage0
git commit -m "chore: update stage0"
'';
benchmarks =
let
entries = attrNames (readDir ../tests/bench);
leanFiles = map (n: elemAt n 0) (filter (n: n != null) (map (match "(.*)\.lean") entries));
in lib.genAttrs leanFiles (n: (buildLeanPackage {
name = n;
src = filterSource (e: _: baseNameOf e == "${n}.lean") ../tests/bench;
}).executable);
};
stage1 = stage { stage = 1; prevStage = stage0; self = stage1; };
stage2 = stage { stage = 2; prevStage = stage1; self = stage2; };