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

chore: Nix: include orphan modules like lean.mk does

Browse source
This commit is contained in:
Sebastian Ullrich 2022-08-27 17:41:46 +02:00
parent fb408c024b
commit 4562fcfbd7
2 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
nix/bootstrap.nix
View file

@ -88,6 +88,7 @@ rec {
leanFlags = [ "-DwarningAsError=true" ];
} ({
src = ../src;
roots = [ { mod = args.name; glob = "andSubmodules"; } ];
fullSrc = ../.;
srcPrefix = "src";
inherit debug;
@ -108,7 +109,7 @@ rec {
modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) (stdlib ++ [ Leanc ]); };
iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
extlib = stdlib; # TODO: add Lake
Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; };
Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
stdlibLinkFlags = "-L${Init.staticLib} -L${Std.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean";
leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
mkdir $out

2
nix/buildLeanPackage.nix
View file

@ -208,7 +208,7 @@ with builtins; let
if typeOf g == "string" then [g]
else if g.glob == "one" then [g.mod]
else if g.glob == "submodules" then submodules g.mod
else if g.glob == "andSubmodules" then [g] ++ submodules g.mod
else if g.glob == "andSubmodules" then [g.mod] ++ submodules g.mod
else throw "unknown glob kind '${g}'";
mods' = lib.foldr buildModAndDeps {} (concatMap expandGlob roots);
allLinkFlags = lib.foldr (shared: acc: acc ++ [ "-L${shared}" "-l${shared.linkName or shared.name}" ]) linkFlags allNativeSharedLibs;