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

fix: Nix: lean-dev outside package

Browse source
This commit is contained in:
Sebastian Ullrich 2021-01-20 14:11:47 +01:00
parent 79107a2316
commit a131924797
2 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
nix/bootstrap.nix
View file

@ -74,14 +74,16 @@ rec {
lean-leanDeps = stage0;
lean-final = self;
} (args // {
src = ../src;
fullSrc = ../.;
inherit debug;
leanFlags = [ "-Dinterpreter.prefer_native=false" ];
});
in (all: all // all.lean) rec {
Init = build { name = "Init"; src = ../src; deps = []; };
Std = build { name = "Std"; src = ../src; deps = [ Init ]; };
Lean = build { name = "Lean"; src = ../src; deps = [ Init Std ]; };
Leanpkg = build { name = "Leanpkg"; src = ../src; deps = [ Init Std Lean ]; };
Init = build { name = "Init"; deps = []; };
Std = build { name = "Std"; deps = [ Init ]; };
Lean = build { name = "Lean"; deps = [ Init Std ]; };
Leanpkg = build { name = "Leanpkg"; deps = [ Init Std Lean ]; };
inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package;
mods = Init.mods // Std.mods // Lean.mods;
leanc = writeShellScriptBin "leanc" ''

5
nix/buildLeanPackage.nix
View file

@ -2,7 +2,7 @@
stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, lean-emacs, lean-vscode, nix, substituteAll, symlinkJoin, linkFarmFromDrvs,
... }:
let lean-final' = lean-final; in
{ name, src, deps ? [ lean.Lean ],
{ name, src, fullSrc ? src, deps ? [ lean.Lean ],
debug ? false, leanFlags ? [], leancFlags ? [], executableName ? lib.toLower name,
srcTarget ? "..#stage0", srcArgs ? "(\${args[*]})", lean-final ? lean-final' }:
with builtins; let
@ -151,7 +151,8 @@ in rec {
dir = "bin";
src = ./lean-dev.in;
isExecutable = true;
inherit bash nix srcRoot srcTarget srcArgs;
srcRoot = fullSrc; # use root flake.nix in case of Lean repo
inherit bash nix srcTarget srcArgs;
};
leanpkg-dev = substituteAll {
name = "leanpkg";