From cf1654df1f6be8ee5f672bf9e27f9c62f8babfb1 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 22 Jan 2022 14:46:50 +0100
Subject: [PATCH] fix: Nix: precompilation against stdlib, once more

---
 nix/bootstrap.nix        | 16 +++++++++-------
 nix/buildLeanPackage.nix | 10 ++++++----
 2 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix
index e175d2d5b1..712e4f5137 100644
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@@ -89,27 +89,29 @@ rec {
         src = ../src;
         fullSrc = ../.;
         inherit debug;
+        builtin = true;
       } // args);
-      setBuiltin = pkg: pkg // {
-        mods = mapAttrs (_: m: m // { builtin = true; }) pkg.mods;
+      attachSharedLib = sharedLib: pkg: pkg // {
+        inherit sharedLib;
+        mods = mapAttrs (_: m: m // { inherit sharedLib; }) pkg.mods;
       };
     in (all: all // all.lean) rec {
       inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package;
-      Init = setBuiltin (build { name = "Init"; deps = []; });
-      Std  = setBuiltin (build { name = "Std";  deps = [ Init ]; });
-      Lean = setBuiltin (build { name = "Lean"; deps = [ Init Std ]; });
+      Init = attachSharedLib leanshared (build { name = "Init"; deps = []; });
+      Std  = attachSharedLib leanshared (build { name = "Std";  deps = [ Init ]; });
+      Lean = attachSharedLib leanshared (build { name = "Lean"; deps = [ Init Std ]; });
       stdlib = [ Init Std Lean ];
       iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
       Leanpkg = build { name = "Leanpkg"; deps = stdlib; linkFlags = ["-L${gmp}/lib -L${leanshared}"]; };
       extlib = stdlib ++ [ Leanpkg ];
       Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; linkFlags = ["-L${gmp}/lib -L${leanshared}"]; };
       stdlibLinkFlags = "-L${gmp}/lib -L${Init.staticLib} -L${Std.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean";
-      leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; } ''
+      leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
         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++"
             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}
+          -o $out/$libName
       '';
       mods = Init.mods // Std.mods // Lean.mods;
       leanc = writeShellScriptBin "leanc" ''
diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix
index 968a5093fb..b555f4c7c7 100644
--- a/nix/buildLeanPackage.nix
+++ b/nix/buildLeanPackage.nix
@@ -21,6 +21,8 @@ lib.makeOverridable (
   precompilePackage ? precompileModules,
   # Lean plugin dependencies. Each derivation `plugin` should contain a plugin library at path `${plugin}/${plugin.name}`.
   pluginDeps ? [],
+  # set only when compiling the stdlib
+  builtin ? false,
   debug ? false, leanFlags ? [], leancFlags ? [], linkFlags ? [], executableName ? lib.toLower name,
   srcTarget ? "..#stage0", srcArgs ? "(\${args[*]})", lean-final ? lean-final' }:
 with builtins; let
@@ -47,7 +49,7 @@ with builtins; let
   }) buildCommand;
   mkSharedLib = name: args: runBareCommand "${name}-dynlib" {
     buildInputs = [ stdenv.cc ] ++ lib.optional stdenv.isDarwin darwin.cctools;
-    libName = "${name}.${stdenv.hostPlatform.extensions.sharedLibrary}";
+    libName = "${name}${stdenv.hostPlatform.extensions.sharedLibrary}";
   } ''
     mkdir -p $out
     ${leanc}/bin/leanc -fPIC -shared ${lib.optionalString stdenv.isLinux "-Bsymbolic"} ${lib.optionalString stdenv.isDarwin "-Wl,-undefined,dynamic_lookup"} -L ${gmp}/lib \
@@ -85,7 +87,7 @@ with builtins; let
 
   leanPluginFlags = lib.concatStringsSep " " (map (dep: "--plugin=${pathOfSharedLib dep}") pluginDeps);
   pkgLeanLoadDynlibPaths = map pathOfSharedLib allNativeSharedLibs;
-  loadDynlibPathsOfDeps = deps: concatMap (d: lib.optional (d ? sharedLib) (pathOfSharedLib d.sharedLib)) deps;
+  loadDynlibPathsOfDeps = deps: concatMap (d: lib.optional (!builtin && d ? sharedLib) (pathOfSharedLib d.sharedLib)) deps;
 
   fakeDepRoot = runBareCommandLocal "${name}-dep-root" {} ''
     mkdir $out
@@ -144,7 +146,7 @@ with builtins; let
       leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG"}
     '';
   };
-  precompileMod = mod: obj: deps: mkSharedLib mod "${obj}/${obj.oPath} ${lib.concatStringsSep " " (map (d: "${d.sharedLib}/*") (filter (d: !(d ? builtin)) deps))}";
+  precompileMod = mod: obj: deps: mkSharedLib mod "${obj}/${obj.oPath} ${lib.concatStringsSep " " (map (d: "${d.sharedLib}/*") deps)}";
   mkMod = mod: deps:
     let drv = buildMod mod deps;
         obj = compileMod mod drv; in
@@ -189,7 +191,7 @@ with builtins; let
   staticLibArguments = staticLibLinkWrapper ("${staticLib}/* ${lib.concatStringsSep " " (map (d: "${d}/*.a") allStaticLibDeps)}");
 in rec {
   inherit name lean deps staticLibDeps allNativeSharedLibs allLinkFlags allExternalDeps print-lean-deps src objects staticLib;
-  mods = if precompilePackage then mapAttrs (_: m: m // { inherit sharedLib; origShlib = m.sharedLib; }) mods' else mods';
+  mods = if precompilePackage then mapAttrs (_: m: m // { inherit sharedLib; }) mods' else mods';
   modRoot   = depRoot name [ mods.${name} ];
   cTree     = symlinkJoin { name = "${name}-cTree"; paths = map (mod: mod.c) (attrValues mods); };
   oTree     = symlinkJoin { name = "${name}-oTree"; paths = (attrValues objects); };