From 195f59790d1f280bd001503bdb6acbb24c1574af Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 21 Sep 2023 14:29:06 +0200 Subject: [PATCH] nix: Avoid adding search path symlinks to the nix store This fixes #2508 --- nix/bootstrap.nix | 3 +-- nix/buildLeanPackage.nix | 30 ++++++++++++++---------------- nix/symlinkSearchPath.sh | 36 ++++++++++++++++++++++++++++++++++++ 3 files changed, 51 insertions(+), 18 deletions(-) create mode 100644 nix/symlinkSearchPath.sh diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index ddf2046537fc..a8f09f73073e 100644 --- a/nix/bootstrap.nix +++ b/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 ]; diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix index 4ae908836d63..5b9a91cf439f 100644 --- a/nix/buildLeanPackage.nix +++ b/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,10 +135,9 @@ 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); @@ -153,13 +145,19 @@ with builtins; let 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); }; diff --git a/nix/symlinkSearchPath.sh b/nix/symlinkSearchPath.sh new file mode 100644 index 000000000000..26040bedecb1 --- /dev/null +++ b/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