18 lines
513 B
Bash
18 lines
513 B
Bash
#!@bash@/bin/bash
|
|
|
|
set -euo pipefail
|
|
|
|
root="."
|
|
# find package root
|
|
while [[ "$root" != / ]]; do
|
|
[ -f "$root/flake.nix" ] && break
|
|
root="$(realpath "$root/..")"
|
|
done
|
|
# fall back to initial package if not in package
|
|
[[ ! -f "$root/flake.nix" ]] && root="@srcRoot@"
|
|
target="$root#lean"
|
|
args=(-- "$@")
|
|
# HACK: use stage 0 instead of 1 inside Lean's own `src/`
|
|
[[ -d Lean && -f ../flake.nix ]] && target="@srcTarget@" && args=@srcArgs@
|
|
|
|
LEAN_SYSROOT="$(dirname "$0")/.." @nix@/bin/nix run "$target" ${args[*]}
|