This repository has no description
1{ pkgs, lib, config, inputs, ... }:
2
3{
4 packages = with pkgs; [
5 cargo
6 git
7 lean4
8 rustc
9 ];
10
11 scripts.build.exec = ''
12 lake build
13 '';
14
15 scripts.run.exec = ''
16 set -euo pipefail
17
18 binary=".lake/build/bin/mlang"
19 repl_manifest="native/mlang_repl/Cargo.toml"
20 repl_binary="native/mlang_repl/target/release/mlang_repl"
21 needs_build=0
22
23 if [ ! -x "$binary" ]; then
24 needs_build=1
25 elif find Main.lean Mlang Mlang.lean lakefile.lean lean-toolchain native \
26 -type f -newer "$binary" | grep -q .; then
27 needs_build=1
28 fi
29
30 if [ "$needs_build" -eq 1 ]; then
31 lake build
32 fi
33
34 if [ "$#" -eq 0 ]; then
35 if [ ! -x "$repl_binary" ] || find "$repl_manifest" native/mlang_repl/src \
36 -type f -newer "$repl_binary" | grep -q .; then
37 cargo build --release --manifest-path "$repl_manifest"
38 fi
39 exec "$repl_binary"
40 fi
41
42 exec "$binary" "$@"
43 '';
44
45 enterShell = ''
46 echo "mlang devenv ready"
47 lean --version
48 lake --version
49 '';
50
51 enterTest = ''
52 lean --version
53 lake --version
54 '';
55}