From e250e8e433ded1f4e121450b9aa4a2ca58131c2d Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 27 Nov 2020 19:30:46 +0100
Subject: [PATCH] fix: Nix: use interpreter.prefer_native=false during
 bootstrap

---
 nix/bootstrap.nix        |  7 ++++++-
 nix/buildLeanPackage.nix | 10 +++++++---
 2 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix
index 0dd173a8a4..ca9b3dc5c8 100644
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@@ -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; }; };
diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix
index 4a45e0365c..ebd716b0c1 100644
--- a/nix/buildLeanPackage.nix
+++ b/nix/buildLeanPackage.nix
@@ -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; } ];