nix/lake-dev.in

#!@bash@/bin/bash

set -euo pipefail

function pebkac() {
    echo 'This is just a simple Nix adapter for `lake print-paths|serve`.'
    exit 1
}

[[ $# -gt 0 ]] || pebkac
case $1 in
    --version)
        # minimum version for `lake serve` with fallback
        echo 3.1.0
        ;;
    print-paths)
        shift
        deps="$@"
        root=.
        # fall back to initial package if not in package
        [[ ! -f "$root/flake.nix" ]] && root="@srcRoot@"
        target="$root#print-paths"
        args=()
        # HACK: use stage 0 instead of 1 inside Lean's own `src/`
        [[ -d Lean && -f ../flake.nix ]] && target="@srcTarget@print-paths" && args=@srcArgs@
        for dep in $deps; do
            target="$target.\"$dep\""
        done
        echo "Building dependencies..." >&2
        # -v only has "built ...", but "-vv" is a bit too verbose
        exec @nix@/bin/nix run "$target" ${args[*]} -v
        ;;
    serve)
        shift
        [[ ${1:-} == "--" ]] && shift
        # `link-ilean` puts them there
        LEAN_PATH=${LEAN_PATH:+$LEAN_PATH:}$PWD/build/lib exec $(dirname $0)/lean --server "$@"
        ;;
    *)
        pebkac
        ;;
esac