lean-dev.in

#!@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@"

# use Lean w/ package unless in server mode (which has its own LEAN_PATH logic)
target="$root#lean-package"
for arg in "$@"; do
    case $arg in
        --server | --worker | -v | --version)
            target="$root#lean"
            ;;
    esac
done

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")/.." exec @nix@/bin/nix ${LEAN_NIX_ARGS:-} run "$target" ${args[*]}