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

refactor: bootstrap.nix

Browse source
This commit is contained in:
Sebastian Ullrich 2021-09-22 14:09:00 +02:00
parent ad7c5b26a7
commit 5a4309e599
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
nix/bootstrap.nix
View file

@ -77,22 +77,24 @@ rec {
# use same stage for retrieving dependencies
lean-leanDeps = stage0;
lean-final = self;
} (args // {
} ({
src = ../src;
fullSrc = ../.;
inherit debug;
});
} // args);
in (all: all // all.lean) rec {
inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package;
Init = build { name = "Init"; deps = []; };
Std = build { name = "Std"; deps = [ Init ]; };
Lean = build { name = "Lean"; deps = [ Init Std ]; };
Leanpkg = build { name = "Leanpkg"; deps = [ Init Std Lean ]; linkFlags = ["-L${gmp}/lib -L${leanshared}"]; };
stdlib = [ Init Std Lean ];
Leanpkg = build { name = "Leanpkg"; deps = stdlib; linkFlags = ["-L${gmp}/lib -L${leanshared}"]; };
extlib = stdlib ++ [ Leanpkg ];
stdlibLinkFlags = "-L${gmp}/lib -L${Init.staticLib} -L${Std.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean";
leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; } ''
mkdir $out
LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Bsymbolic"} \
${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Std.staticLib}/libStd.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
${if stdenv.isDarwin then "${lib.concatMapStringsSep " " (l: "-Wl,-force_load,${l.staticLib}/*") stdlib} -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
else "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++"} -lm ${stdlibLinkFlags} \
-o $out/libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}
'';
@ -110,7 +112,7 @@ rec {
name = "lean-${desc}";
buildCommand = ''
mkdir -p $out/bin $out/lib/lean
ln -sf ${leancpp}/lib/lean/* ${Leanpkg.modRoot}/* ${Lean.staticLib}/* ${Lean.modRoot}/* ${Std.staticLib}/* ${Std.modRoot}/* ${Init.staticLib}/* ${Init.modRoot}/* $out/lib/lean/
ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList extlib)} $out/lib/lean/
# put everything in a single final derivation so `IO.appDir` references work
cp ${lean}/bin/lean ${leanpkg}/bin/leanpkg $out/bin
# NOTE: first `bin/leanc` wins in case of `lndir`