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

fix: Nix: use interpreter.prefer_native=false during bootstrap

Browse source
This commit is contained in:
Sebastian Ullrich 2020-11-27 19:30:46 +01:00
parent 3a4b61f8c7
commit e250e8e433
2 changed files with 13 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
nix/bootstrap.nix
View file

@ -53,7 +53,12 @@ rec {
stage = { stage, prevStage, self }:
let
desc = "stage${toString stage}";
build = buildLeanPackage.override { lean = prevStage; lean-final = self; inherit debug; };
build = buildLeanPackage.override {
lean = prevStage;
lean-final = self;
inherit debug;
leanFlags = [ "-Dinterpreter.prefer_native=false" ];
};
in (all: all // all.lean) rec {
Init = build { name = "Init"; src = ../src; srcDir = "/src"; deps = {}; };
Std = build { name = "Std"; src = ../src; srcDir = "/src"; deps = { inherit Init; }; };

10
nix/buildLeanPackage.nix
View file

@ -1,4 +1,6 @@
{ debug ? false, stdenv, lib, coreutils, gnused, lean, leanc ? lean, lean-final ? lean, writeShellScriptBin, bash, lean-emacs, nix, substituteAll, symlinkJoin, linkFarmFromDrvs }:
{ debug ? false, leanFlags ? [], leancFlags ? [],
lean, leanc ? lean, lean-final ? lean,
stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, lean-emacs, nix, substituteAll, symlinkJoin, linkFarmFromDrvs }:
with builtins; let
# "Init.Core" ~> "Init/Core"
modToPath = mod: replaceStrings ["."] ["/"] mod;
@ -68,10 +70,11 @@ in
outputs = [ "out" "c" ];
oleanPath = relpath + ".olean";
cPath = relpath + ".c";
inherit leanFlags;
buildCommand = ''
mkdir -p $(dirname $relpath) $out/$(dirname $relpath) $c/$(dirname $relpath)
cp $src $leanPath
lean -o $out/$oleanPath -c $c/$cPath $leanPath
lean -o $out/$oleanPath -c $c/$cPath $leanPath $leanFlags
'';
} // {
inherit deps;
@ -81,11 +84,12 @@ in
buildInputs = [ leanc ];
hardeningDisable = [ "all" ];
oPath = drv.relpath + ".o";
inherit leancFlags;
buildCommand = ''
mkdir -p $out/$(dirname ${drv.relpath})
# make local "copy" so `drv`'s Nix store path doesn't end up in ccache's hash
ln -s ${drv.c}/${drv.cPath} src.c
leanc -c -o $out/$oPath src.c ${if debug then "-g" else "-O3 -DNDEBUG"}
leanc -c -o $out/$oPath src.c $leancFlags ${if debug then "-g" else "-O3 -DNDEBUG"}
'';
};
singleton = name: value: listToAttrs [ { inherit name value; } ];