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

fix: Nix: use current stage for files outside of source root

Browse source
This commit is contained in:
Sebastian Ullrich 2020-11-17 17:49:50 +01:00
parent 6845d18119
commit 1dedafa173
2 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
nix/bootstrap.nix
View file

@ -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; };
}

4
nix/buildLeanPackage.nix
View file

@ -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