{ pkgs, lib, config, inputs, ... }:

{
  packages = with pkgs; [
    cargo
    git
    lean4
    rustc
  ];

  scripts.build.exec = ''
    lake build
  '';

  scripts.run.exec = ''
    set -euo pipefail

    binary=".lake/build/bin/mlang"
    repl_manifest="native/mlang_repl/Cargo.toml"
    repl_binary="native/mlang_repl/target/release/mlang_repl"
    needs_build=0

    if [ ! -x "$binary" ]; then
      needs_build=1
    elif find Main.lean Mlang Mlang.lean lakefile.lean lean-toolchain native \
      -type f -newer "$binary" | grep -q .; then
      needs_build=1
    fi

    if [ "$needs_build" -eq 1 ]; then
      lake build
    fi

    if [ "$#" -eq 0 ]; then
      if [ ! -x "$repl_binary" ] || find "$repl_manifest" native/mlang_repl/src \
        -type f -newer "$repl_binary" | grep -q .; then
        cargo build --release --manifest-path "$repl_manifest"
      fi
      exec "$repl_binary"
    fi

    exec "$binary" "$@"
  '';

  enterShell = ''
    echo "mlang devenv ready"
    lean --version
    lake --version
  '';

  enterTest = ''
    lean --version
    lake --version
  '';
}