From 5a4309e599e6356942cb7ebaa38ced197cffc4f4 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 22 Sep 2021 14:09:00 +0200
Subject: [PATCH] refactor: bootstrap.nix

---
 nix/bootstrap.nix | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix
index 171aa10105..b191be1dc3 100644
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@@ -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`