From 1dedafa1732a0d01043c6d08dcdc17b17fea79a3 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 17 Nov 2020 17:49:50 +0100
Subject: [PATCH] fix: Nix: use current stage for files outside of source root

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

diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix
index a8ac5bd9ec..57426d6af5 100644
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@@ -42,10 +42,10 @@ rec {
       ln -s ${../stage0/stdlib} ../stdlib
     '';
   };
-  stage = { stage, prevStage }:
+  stage = { stage, prevStage, self }:
     let
       desc = "stage${toString stage}";
-      build = buildLeanPackage.override { lean = prevStage; };
+      build = buildLeanPackage.override { lean = prevStage; lean-final = self; };
     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; }; };
@@ -77,7 +77,7 @@ rec {
         '';
       };
     };
-  stage1 = stage { stage = 1; prevStage = stage0; };
-  stage2 = stage { stage = 2; prevStage = stage1; };
-  stage3 = stage { stage = 3; prevStage = stage2; };
+  stage1 = stage { stage = 1; prevStage = stage0; self = stage1; };
+  stage2 = stage { stage = 2; prevStage = stage1; self = stage2; };
+  stage3 = stage { stage = 3; prevStage = stage2; self = stage3; };
 }
diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix
index 65ec05be06..8da881935c 100644
--- a/nix/buildLeanPackage.nix
+++ b/nix/buildLeanPackage.nix
@@ -1,4 +1,4 @@
-{ debug ? false, stdenv, lib, coreutils, gnused, lean, leanc ? lean, writeScriptBin, bash, lean-emacs }:
+{ debug ? false, stdenv, lib, coreutils, gnused, lean, leanc ? lean, lean-final ? lean, writeScriptBin, bash, lean-emacs }:
 with builtins; let
   # "Init.Core" ~> "Init/Core.lean"
   modToLean = mod: replaceStrings ["."] ["/"] mod + ".lean";
@@ -102,7 +102,7 @@ in
     lean-package = writeScriptBin "lean" ''
       #!${bash}/bin/bash
       set -euo pipefail
-      LEAN_PATH=${modRoot} ${lean}/bin/lean $@
+      LEAN_PATH=${modRoot} ${lean-final}/bin/lean $@
     '';
     lean-dev = writeScriptBin "lean" ''
       #!${bash}/bin/bash