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

chore: Nix: fix update-stage0

Browse source
This commit is contained in:
Sebastian Ullrich 2024-06-21 22:02:10 +02:00
parent 073b2cfc83
commit e665a0d716
1 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
nix/bootstrap.nix
View file

@ -154,9 +154,7 @@ rec {
};
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
Init.oTree Std.oTree Lean.oTree Lake.oTree
];
] ++ map (lib: lib.oTree) stdlib;
test = buildCMake {
name = "lean-test-${desc}";
realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
@ -179,7 +177,7 @@ rec {
'';
};
update-stage0 =
let cTree = symlinkJoin { name = "cs"; paths = [ Init.cTree Lean.cTree Lake.cTree ]; }; in
let cTree = symlinkJoin { name = "cs"; paths = map (lib: lib.cTree) stdlib; }; in
writeShellScriptBin "update-stage0" ''
CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
'';