nix: Avoid adding search path symlinks to the nix store

This fixes leanprover#2508

nix/bootstrap.nix

@@ -116,7 +116,6 @@ rec {
       };
       stdlib = [ Init Lean Lake ];
       modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) (stdlib ++ [ Leanc ]); };
-      depRoots = symlinkJoin { name = "depRoots"; paths = map (l: l.depRoots) stdlib; };
       iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
       Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
       stdlibLinkFlags = "-L${Init.staticLib} -L${Lean.staticLib} -L${Lake.staticLib} -L${leancpp}/lib/lean";
@@ -151,7 +150,7 @@ rec {
         meta.mainProgram = "lean";
       };
       cacheRoots = linkFarmFromDrvs "cacheRoots" [
-        stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
+        stage0 lean leanc lean-all iTree modDepsFiles Lean.modRoot Leanc.src
         # .o files are not a runtime dependency on macOS because of lack of thin archives
         Lean.oTree Lake.oTree
       ];

nix/buildLeanPackage.nix

@@ -67,18 +67,11 @@ with builtins; let
   '';
   depRoot = name: deps: mkBareDerivation {
     name = "${name}-depRoot";
-    inherit deps;
-    depRoots = map (drv: drv.LEAN_PATH) deps;
-
-    passAsFile = [ "deps" "depRoots" ];
+    buildInputs = [ symlinkSearchPath ];
+    depList = lib.concatLines deps;
+    passAsFile = [ "depList" ];
     buildCommand = ''
-      mkdir -p $out
-      for i in $(cat $depRootsPath); do
-        cp -dru --no-preserve=mode $i/. $out
-      done
-      for i in $(cat $depsPath); do
-        cp -drsu --no-preserve=mode $i/. $out
-      done
+      symlinkSearchPath $out $depListPath
     '';
   };
   srcRoot = src;
@@ -88,9 +81,9 @@ with builtins; let
   allNativeSharedLibs =
     lib.unique (lib.flatten (nativeSharedLibs ++ (map (dep: dep.allNativeSharedLibs or []) allExternalDeps)));
 
-  # A flattened list of all static library dependencies: this and every dep module's explicitly provided `staticLibDeps`, 
+  # A flattened list of all static library dependencies: this and every dep module's explicitly provided `staticLibDeps`,
   # plus every dep module itself: `dep.staticLib`
-  allStaticLibDeps = 
+  allStaticLibDeps =
     lib.unique (lib.flatten (staticLibDeps ++ (map (dep: [dep.staticLib] ++ dep.staticLibDeps or []) allExternalDeps)));
 
   pathOfSharedLib = dep: dep.libPath or "${dep}/${dep.libName or dep.name}";
@@ -142,24 +135,29 @@ with builtins; let
   # TODO: make `rec` parts override-compatible?
   buildMod = mod: deps: maybeOverrideAttrs overrideBuildModAttrs (mkBareDerivation rec {
     name = "${mod}";
-    LEAN_PATH = depRoot mod deps;
     LEAN_ABORT_ON_PANIC = "1";
     relpath = modToPath mod;
-    buildInputs = [ lean ];
+    buildInputs = [ lean symlinkSearchPath ];
     leanPath = relpath + ".lean";
     # should be either single .lean file or directory directly containing .lean file plus dependencies
     src = copyToStoreSafe srcRoot ("/" + leanPath);
     outputs = [ "out" "ilean" "c" ];
     oleanPath = relpath + ".olean";
     ileanPath = relpath + ".ilean";
     cPath = relpath + ".c";
+    # this will be part of the output as lean-deps.txt
+    depList = lib.concatLines deps;
+    passAsFile = [ "depList" ];
     inherit leanFlags leanPluginFlags;
     leanLoadDynlibFlags = map (p: "--load-dynlib=${pathOfSharedLib p}") (loadDynlibsOfDeps deps);
     buildCommand = ''
       dir=$(dirname $relpath)
       mkdir -p $dir $out/$dir $ilean/$dir $c/$dir
+      symlinkSearchPath imports $depListPath
+      export LEAN_PATH=imports
       if [ -d $src ]; then cp -r $src/. .; else cp $src $leanPath; fi
       lean -o $out/$oleanPath -i $ilean/$ileanPath -c $c/$cPath $leanPath $leanFlags $leanPluginFlags $leanLoadDynlibFlags
+      cp $depListPath $out/lean-deps.txt
     '';
   }) // {
     inherit deps;
@@ -203,6 +201,7 @@ with builtins; let
   makeVSCodeWrapper = name: lean: writeShellScriptBin name ''
     PATH=${lean}/bin:$PATH ${lean-vscode}/bin/code "$@"
   '';
+  symlinkSearchPath = writeShellScriptBin "symlinkSearchPath" (readFile ./symlinkSearchPath.sh);
   printPaths = deps: writeShellScriptBin "print-paths" ''
     echo '${toJSON {
       oleanPath = [(depRoot "print-paths" deps)];
@@ -241,7 +240,6 @@ in rec {
       lib.optionalAttrs precompilePackage { propagatedLoadDynlibs = [sharedLib]; })
     mods';
   modRoot   = depRoot name (attrValues mods);
-  depRoots  = linkFarmFromDrvs "depRoots" (map (m: m.LEAN_PATH) (attrValues mods));
   cTree     = symlinkJoin { name = "${name}-cTree"; paths = map (mod: mod.c) (attrValues mods); };
   oTree     = symlinkJoin { name = "${name}-oTree"; paths = (attrValues objects); };
   iTree     = symlinkJoin { name = "${name}-iTree"; paths = map (mod: mod.ilean) (attrValues mods); };

nix/symlinkSearchPath.sh

@@ -0,0 +1,36 @@
+#!/usr/bin/env bash
+
+# Given a target directory and one (or more) `lean-deps.txt` file, as built by buildLeanPackage,
+# recursively traverses it and symlinks the contents into one big directory.
+
+set -e
+
+# first argument: directory to create
+dest="$1"
+shift
+
+# remaining arguments: lean-dep.txt files
+# read their lines into the todo array
+declare -a todo
+for file in "$@"
+do
+    readarray -t -O ${#todo[@]} todo < "$file"
+done
+
+mkdir "$dest"
+
+# simple work-list algorithm
+declare -A seen
+while [ ${#todo[@]} -gt 0 ]
+do
+  n=$((${#todo[@]}-1))
+  dir="${todo[n]}"
+  unset "todo[$n]"
+  if ! [[ -v "seen[$dir]" ]]
+  then
+    seen[$dir]="seen"
+    cp -rs --no-preserve=mode "$dir"/. "$dest"
+    rm "$dest"/lean-deps.txt
+    readarray -t -O ${#todo[@]} todo < "$dir"/lean-deps.txt
+  fi
+done