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

chore: Nix: linkFarm, not symlinkJoin

Browse source
This commit is contained in:
Sebastian Ullrich 2022-12-21 20:06:02 +01:00
parent 443c1a08e5
commit cbf1b433d7
1 changed files with 11 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
nix/bootstrap.nix
View file

@ -1,5 +1,5 @@
{ debug ? false, stage0debug ? false, extraCMakeFlags ? [],
stdenv, lib, cmake, gmp, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages,
stdenv, lib, cmake, gmp, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
... } @ args:
with builtins;
rec {
@ -53,11 +53,7 @@ rec {
mv runtime/libleanrt_initial-exec.a runtime/lean.h.bc $out/lib
'';
};
# rename derivation so `nix run` uses the right executable name but we still see the stage in the build log
wrapStage = stage: runCommand "lean" {} ''
ln -s ${stage} $out
'';
stage0 = wrapStage (args.stage0 or (buildCMake {
stage0 = args.stage0 or (buildCMake {
name = "lean-stage0";
realSrc = ../stage0/src;
debug = stage0debug;
@ -76,7 +72,8 @@ rec {
done
otool -L $out/bin/lean
'';
}));
meta.mainProgram = "lean";
});
stage = { stage, prevStage, self }:
let
desc = "stage${toString stage}";
@ -128,7 +125,7 @@ rec {
${leanc}/bin/leanc ${leancpp}/lib/lean.cpp.o ${leanshared}/* -o $out/bin/lean
'';
# derivation following the directory layout of the "basic" setup, mostly useful for running tests
lean-all = wrapStage(stdenv.mkDerivation {
lean-all = stdenv.mkDerivation {
name = "lean-${desc}";
buildCommand = ''
mkdir -p $out/bin $out/lib/lean
@ -138,15 +135,13 @@ rec {
# NOTE: `lndir` will not override existing `bin/leanc`
${lndir}/bin/lndir -silent ${lean-bin-tools-unwrapped} $out
'';
});
cacheRoots = symlinkJoin {
name = "cacheRoots";
paths = [
stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
# .o files are not a runtime dependency on macOS because of lack of thin archives
Lean.oTree
];
meta.mainProgram = "lean";
};
cacheRoots = linkFarmFromDrvs "cacheRoots" [
stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
# .o files are not a runtime dependency on macOS because of lack of thin archives
Lean.oTree
];
test = buildCMake {
name = "lean-test-${desc}";
realSrc = lib.sourceByRegex ../. [ "src.*" "tests.*" ];