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

chore: Nix: reduce doc/doc-test sources

Browse source
This commit is contained in:
Sebastian Ullrich 2021-08-06 13:21:32 +02:00
parent 14177fbaf6
commit e79d52d2ce
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
nix/packages.nix
View file

@ -78,16 +78,16 @@ let
});
doc = stdenv.mkDerivation {
name ="lean-doc";
src = ../.;
src = ../doc;
buildInputs = [ lean-mdbook ];
buildCommand = ''
mdbook build -d $out $src/doc
mdbook build -d $out $src
'';
};
# We use a separate derivation instead of `checkPhase` so we can push it but not `doc` to the binary cache
doc-test = stdenv.mkDerivation {
name ="lean-doc-test";
src = ../.;
src = lib.sourceByRegex ../. ["doc.*" "tests(/lean(/beginEndAsMacro.lean)?)?"];
buildInputs = [ lean-mdbook lean.stage1.Leanpkg.lean-package strace ];
patchPhase = ''
cd doc