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

chore: Nix: cleanup

Browse source
This commit is contained in:
Sebastian Ullrich 2021-05-21 17:17:54 +02:00
parent 429a450a1b
commit 41cf306788
2 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
nix/buildLeanPackage.nix
View file

@ -185,7 +185,6 @@ in rec {
isExecutable = true;
srcRoot = fullSrc; # use root flake.nix in case of Lean repo
inherit bash nix srcTarget srcArgs;
leanpkg = lean;
};
lean-dev = symlinkJoin { name = "lean-dev"; paths = [ lean-bin-dev leanpkg-dev ]; };
emacs-dev = makeEmacsWrapper "emacs-dev" lean-dev;

4
nix/leanpkg-dev.in
View file

@ -2,7 +2,7 @@
set -euo pipefail
[[ $# -gt 0 && "$1" == print-paths && ( -f flake.nix || -d Lean && -f ../flake.nix || ! -f leanpkg.toml ) ]] || exec @leanpkg@/bin/leanpkg "$@"
[[ $# -gt 0 && "$1" == print-paths ]] || { echo "This is just a simple Nix adapter for `leanpkg print-paths`. Please use the `leanpkg` attribute for the real thing."; exit 1; }
shift
deps="$@"
root=.
@ -15,6 +15,6 @@ args=()
for dep in $deps; do
target="$target.\"$dep\""
done
# -v only has "built ...", but "-vv" is a bit too verbose
echo "Building dependencies..." >&2
# -v only has "built ...", but "-vv" is a bit too verbose
@nix@/bin/nix run "$target" ${args[*]} -v