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

chore: Nix: expose vscode & extension without lean-dev wrapper

Browse source
This commit is contained in:
Sebastian Ullrich 2021-05-28 15:31:20 +02:00
parent 9f72ebe29b
commit fdad29770b
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
nix/packages.nix
View file

@ -101,7 +101,7 @@ let
dontInstall = true;
};
in {
inherit cc lean4-mode buildLeanPackage llvmPackages;
inherit cc lean4-mode buildLeanPackage llvmPackages vscode-lean4;
lean = lean.stage1;
stage0print-paths = lean.stage1.Leanpkg.print-paths;
HEAD-as-stage0 = (lean.stage1.Lean.overrideArgs { srcTarget = "..#stage0-from-input.stage0"; srcArgs = "(--override-input lean-stage0 ..\?rev=$(git rev-parse HEAD) -- -Dinterpreter.prefer_native=false \"$@\")"; });
@ -116,5 +116,6 @@ in {
"$@" |& ts -i "(%.S)]" | ts -s "[%M:%S"
'';
mdbook = lean-mdbook;
vscode = lean-vscode;
inherit doc doc-test;
} // lean.stage1.Lean // lean.stage1 // lean