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

chore: Nix: set up LEAN_SYSROOT automatically in server

Browse source
This commit is contained in:
Sebastian Ullrich 2021-01-20 15:22:09 +01:00
parent 67c78ef1b7
commit b2c609c3ac
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
nix/buildLeanPackage.nix
View file

@ -111,10 +111,10 @@ with builtins; let
modMap' = lib.foldr buildModAndDeps modMap deps;
in modMap' // { ${mod} = buildMod mod (map (dep: if modMap' ? ${dep} then modMap'.${dep} else externalModMap.${dep}) deps); };
makeEmacsWrapper = name: lean: writeShellScriptBin name ''
LEAN_SYSROOT=${lean} ${lean-emacs}/bin/emacs --eval "(progn (setq lean4-rootdir \"${lean}\") (require 'lean4-mode))" "$@"
${lean-emacs}/bin/emacs --eval "(progn (setq lean4-rootdir \"${lean}\") (require 'lean4-mode))" "$@"
'';
makeVSCodeWrapper = name: lean: writeShellScriptBin name ''
LEAN_SYSROOT=${lean} PATH=${lean}/bin:$PATH ${lean-vscode}/bin/code "$@"
PATH=${lean}/bin:$PATH ${lean-vscode}/bin/code "$@"
'';
printPaths = deps: writeShellScriptBin "print-paths" ''
echo "${depRoot "print-paths" deps}"

2
nix/lean-dev.in
View file

@ -9,4 +9,4 @@ args=(-- "$@")
# HACK: use stage 0 instead of 1 inside Lean's own `src/`
[[ -d Lean && -f ../flake.nix ]] && target="@srcTarget@" && args=@srcArgs@
@nix@/bin/nix run "$target" ${args[*]}
LEAN_SYSROOT="$(dirname "$0")/.." @nix@/bin/nix run "$target" ${args[*]}