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

refactor: Nix: move out lean-dev script

Browse source
This commit is contained in:
Sebastian Ullrich 2020-11-18 17:22:30 +01:00
parent 092d5d67b4
commit 73e9b96cdc
2 changed files with 42 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
nix/buildLeanPackage.nix
View file

@ -1,4 +1,4 @@
{ debug ? false, stdenv, lib, coreutils, gnused, lean, leanc ? lean, lean-final ? lean, writeScriptBin, bash, lean-emacs, nix }:
{ debug ? false, stdenv, lib, coreutils, gnused, lean, leanc ? lean, lean-final ? lean, writeScriptBin, bash, lean-emacs, nix, substituteAll }:
with builtins; let
# "Init.Core" ~> "Init/Core.lean"
modToLean = mod: replaceStrings ["."] ["/"] mod + ".lean";
@ -104,42 +104,14 @@ in
set -euo pipefail
LEAN_PATH=${modRoot} ${lean-final}/bin/lean $@
'';
lean-dev = writeScriptBin "lean" ''
#!${bash}/bin/bash
set -euo pipefail
PATH=${nix}/bin:$PATH
lean-dev = substituteAll {
name = "lean";
dir = "bin";
src = ./lean-dev.in;
isExecutable = true;
inherit lean bash nix srcDir;
};
call() {
if [[ $json == 1 ]]; then
$@ 2>&1 | awk '/{/ { print $0; next } { gsub(/"/, "\\\"", $0); gsub(/\n/, "\\n", $0); printf "{\"severity\": \"warning\", \"pos_line\": 0, \"pos_col\": 0, \"file_name\": \"<stdin>\", \"text\": \"%s\"}\n", $0 }'
else
$@
fi
}
json=0
input=
for p in "$@"; do
[[ "$p" == --json ]] && json=1
[[ "$p" != -* ]] && input="$(realpath "$p")"
done
root="$(dirname "''${input:-/}")"
while [[ "$root" != / ]]; do
[ -f "$root/flake.nix" ] && break
root="$(realpath "$root/..")"
done
if [[ "$root" == / ]]; then
call ${lean}/bin/lean $@
elif [[ "$input" != "$root${srcDir}/"* ]]; then
call nix run "$root#lean-package" -- $@
else
input="$(realpath --relative-to="$root${srcDir}" "$input")"
input="''${input%.lean}"
input="''${input//\//.}"
call nix develop "$root#mods.\"$input\"" -c lean $@
fi
'';
emacs-package = writeScriptBin "run-emacs-package" ''
#!${bash}/bin/bash
${lean-emacs}/bin/emacs --eval '(setq lean4-rootdir "${lean-package}")' $@

34
nix/lean-dev.in Normal file
View file

@ -0,0 +1,34 @@
#!@bash@/bin/bash
set -euo pipefail
PATH=@nix@/bin:$PATH
call() {
if [[ $json == 1 ]]; then
$@ 2>&1 | awk '/{/ { print $0; next } { gsub(/"/, "\\\"", $0); gsub(/\n/, "\\n", $0); printf "{\"severity\": \"warning\", \"pos_line\": 0, \"pos_col\": 0, \"file_name\": \"<stdin>\", \"text\": \"%s\"}\n", $0 }'
else
$@
fi
}
json=0
input=
for p in "$@"; do
[[ "$p" == --json ]] && json=1
[[ "$p" != -* ]] && input="$(realpath "$p")"
done
root="$(dirname "${input:-/}")"
while [[ "$root" != / ]]; do
[ -f "$root/flake.nix" ] && break
root="$(realpath "$root/..")"
done
if [[ "$root" == / ]]; then
call @lean@/bin/lean $@
elif [[ "$input" != "$root@srcDir@/"* ]]; then
call nix run "$root#lean-package" -- $@
else
input="$(realpath --relative-to="$root@srcDir@" "$input")"
input="${input%.lean}"
input="${input//\//.}"
call nix develop "$root#mods.\"$input\"" -c lean $@
fi