Something went wrong. Try again.
The Monad language. Dependent types, functional programming compiled with LLVM. Hobby project. monad-lang.org
dependent-types language compiler programming-language functional-programming
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295// IO is ambient (init/io.mo, always a loaded root) -- no `use` needed.use lib::io {}open IO {current_time_nano, file_exists_native, read_file_native}#[native "exec_cmd"]pub def exec_cmd (cmd : String) (args : List String) : IO I64#[native "process_id"]pub def process_id : I64// ── Piped subprocesses (agent-skills.md Phase 4 / Design 6) ────────────//// `exec_cmd` and `Proc.capture` (below) wait for the child and return// only what it already wrote; a PROTOCOL peer -- an MCP server on// stdio -- needs the opposite: write its stdin while it runs, read its// stdout line by line, keep stderr separate, and be able to kill it.// That needs child state to OUTLIVE a single call, which no// composition of `exec_cmd` can hold, so unlike `Proc.capture` these// ARE natives -- the one place in this file the "deliberately not a// native" rule below gives way, for the reason that rule states: the// wiring cost buys a capability nothing else here can express.//// Four natives, not six: the former read/read-stderr and wait/kill// twins are merged behind I64 flags -- `proc_read`'s second argument// picks the stream, `proc_wait`'s picks plain reap vs// SIGKILL-then-reap. The natives return `RawIO _`, the raw payload// layer; the `IO.mk` wrap happens HERE, in the pub wrappers -- the// same split `IO.pure`/`RawIO.pure` use, so the Rust and C sides stay// raw payload producers while every user-facing operation is `IO _`.// The wrappers are the public API; the natives are `priv` so no other// module can reach past them.//// `Child` is opaque the way `Socket` is (std/src/io.mo): the// constructor exists so the checker can see a type; the runtime value// is a registry handle, never a constructor. Nothing may pattern-match,// compare or print one. It is `pub` because `motes/mcp_client`// (a separate mote) holds children.//// stdout and stderr stay SEPARATE pipes here on purpose. `Proc.// capture` merges them, which is right for toolchain probes (see its// own doc) and wrong for a protocol stream: a server's log line on// stderr must not land inside the JSON-RPC framing. `read_stderr_line`// exists so a caller can drain those logs without touching the frame// stream.pub type Child { child}/// `proc_read`'s stream flag: 0 = stdout. Named so the wrappers read/// as intent rather than as a magic number, and dotted so the/// whole-program bare-name table does not gain a `stdout`.priv def Proc.stdout_flag : I64 := 0/// `proc_read`'s stream flag: 1 = stderr.priv def Proc.stderr_flag : I64 := 1/// `proc_wait`'s kill flag: 0 = plain reap.priv def Proc.reap_flag : I64 := 0/// `proc_wait`'s kill flag: 1 = SIGKILL first, then reap.priv def Proc.kill_flag : I64 := 1/// Fork+exec `cmd args` with all three standard streams piped./// Payload is `Result.err` (with the OS message) rather than a native/// failure when the child could not be spawned -- a caller composes/// the error through `ResultT` like every other failure here.#[native "proc_spawn"]priv def proc_spawn (cmd : String) (args : List String) : RawIO (Result String Child)/// Write `s` to the child's stdin and flush. Payload is `Result.err`/// when the child is gone (a dead peer's EPIPE surfaces here -- that/// is the signal to stop talking to it), `Result.ok` with the byte/// count otherwise.#[native "proc_write"]priv def proc_write (c : Child) (s : String) : RawIO (Result String U64)/// One line of the child's chosen stream (`stream`: 0 = stdout, 1 =/// stderr) WITHOUT its trailing newline (any `\r` stays -- toolkit's/// framing trims it, keeping one definition of "line" per concern)./// Payload's `Option.none` is end of stream; a final line truncated by/// EOF is DISCARDED rather than half-delivered, because a JSON-RPC/// frame without its newline is a truncated message, not a message./// A line is BOUNDED: content beyond 1048576 bytes (one mebibyte) is/// `Result.err` -- a peer that withholds its newline must fail the/// read rather than grow it without limit. Both backends carry the/// same number; the caller should treat the peer as broken.#[native "proc_read"]priv def proc_read (c : Child) (stream : I64) : RawIO (Result String (Option String))/// Close the pipes, reap the child, and free its slot, returning the/// exit status -- or -1 if it died on a signal, `exec_cmd`'s own/// convention. With `kill` set, SIGKILL first, so one call is the whole/// "kill, then reap" teardown. Killing an already-exited child is not/// an error either way -- a disposer must be idempotent. The handle/// dies with the child: nothing may use it after `proc_wait`.#[native "proc_wait"]priv def proc_wait (c : Child) (kill : I64) : RawIO I64/// Fork+exec `cmd args` with all three standard streams piped./// `Result.err` (with the OS message) rather than a native failure/// when the child could not be spawned -- a caller composes the error/// through `ResultT` like every other failure here.pub def Proc.spawn (cmd : String) (args : List String) : IO (Result String Child) := IO.mk (proc_spawn cmd args)/// Write `s` to the child's stdin and flush. `Result.err` when the/// child is gone (a dead peer's EPIPE surfaces here -- that is the/// signal to stop talking to it), `Result.ok` with the byte count/// otherwise.pub def Proc.write (c : Child) (s : String) : IO (Result String U64) := IO.mk (proc_write c s)/// One line of the child's stdout WITHOUT its trailing newline (any/// `\r` stays -- toolkit's framing trims it, keeping one definition of/// "line" per concern). `Option.none` is end of stream; a final line/// truncated by EOF is DISCARDED rather than half-delivered, because/// a JSON-RPC frame without its newline is a truncated message, not a/// message. A line whose content exceeds one mebibyte is `Result.err`/// (see `proc_read`'s own contract for the bound).pub def Proc.read_line (c : Child) : IO (Result String (Option String)) := IO.mk (proc_read c Proc.stdout_flag)/// `Proc.read_line`'s contract, over the child's stderr -- the log/// stream a server writes while its protocol stream stays clean.pub def Proc.read_stderr_line (c : Child) : IO (Result String (Option String)) := IO.mk (proc_read c Proc.stderr_flag)/// Close the pipes, reap the child, and return its exit status -- or/// -1 if it died on a signal, `exec_cmd`'s own convention. The handle/// dies with the child: nothing may use it after `wait`.pub def Proc.wait (c : Child) : IO I64 := IO.mk (proc_wait c Proc.reap_flag)/// SIGKILL the child, then reap it and free its slot -- one call is the/// whole teardown, so no caller needs a `wait` after `kill`. Killing/// an already-exited child is not an error (a disposer must be/// idempotent); a `wait` AFTER `kill` returns -1 because the slot is/// already freed, not because the kill failed to reap.pub def Proc.kill (c : Child) : IO Unit := IO.mk (RawIO.bind (proc_wait c Proc.kill_flag) (fn _ => RawIO.pure Unit.unit))// ── Capturing a command's output ────────────────────────────────────────// `exec_cmd` above hands back an exit status and nothing else:// `monad_exec_cmd` (runtime/src/runtime.c) is fork + execvp + waitpid// returning `WEXITSTATUS`, with no pipe and no `dup2`. Reading what a tool// PRINTED therefore needs a detour, and `Proc.capture` is the one place// that detour lives -- `clang -dumpmachine`, `llc --version` and// `git rev-parse` all want it, and a second hand-rolled copy is how the// old `link_ir` build-commit probe drifted (see llvm/src/link.mo's// `build_commit_define` for that story).//// Deliberately NOT a new native. A native costs six wiring places --// core_native.rs's dispatch arm AND its PURE_NATIVES allowlist,// lower_core_ir.rs, natives.mo's `native_runtime_fn_name` AND its// `runtime_declarations`, and runtime.c -- and then has to be kept in step// across both runtimes forever. Everything below is ordinary Monad over// primitives that already exist on both./// The byte `'` (0x27). Named because it is load-bearing twice below: it/// is what `Proc.shell_quote` has to escape, and the fact that it is/// BELOW 0x80 is what makes slicing at its index UTF-8-safe.def Proc.quote_byte : U8 := 39u8/// Index of the first `'` in `s`, or `none`.////// Byte-exact, via `String.to_list`. That is not fussiness: `String.slice`/// and `String.drop` are byte-oriented and silently return `""` when an/// offset lands mid-character (see the UTF-8 note in/// lang/src/parser/combinators.mo, which was written after exactly that/// bug truncated everything after an em dash). Scanning the byte list/// gives an exact index, and slicing AT that index is safe for the one/// reason that matters: `0x27` is below `0x80`, so it can never be a/// continuation byte, and a quote's index is therefore always a character/// boundary.def Proc.first_quote (s : String) : Option I64 := Proc.first_quote_go (String.to_list s) 0#[partial]def Proc.first_quote_go (bytes : List U8) (i : I64) : Option I64 := match bytes { List.empty => Option.none, List.cons b rest => if U8.beq b Proc.quote_byte then Option.some i else Proc.first_quote_go rest (i + 1) }/// Replace every `'` with `'\''` -- close the quote, emit an escaped/// quote, reopen it. Splits AT each quote rather than walking byte by/// byte, for the boundary reason in `Proc.first_quote`.#[partial]def Proc.escape_quotes (s : String) : String := match Proc.first_quote s { Option.none => s, Option.some i => // `String.slice`'s third argument is a LENGTH, not an end // index -- so this is "the i bytes before the quote". String.concat (String.slice s 0 i) (String.concat "'\\''" (Proc.escape_quotes (String.drop (i + 1) s))) }/// Quote `s` so that a POSIX shell reads it as one literal word.////// Single quotes, because they are the only POSIX quoting that is FULLY/// literal: no parameter expansion, no command substitution, no backslash/// escapes, no globbing. So a quoted argument cannot be reinterpreted by/// the shell whatever it contains -- which is what makes it safe to pass a/// path, a git URL or a ref through `sh -c` at all.////// This is the control, not a convention. Every interpolated component of/// a `sh -c` script must go through it, and/// `test_capture_does_not_expand_a_dollar_sign` (in/// `std/src/process_tests.mo`) is what fails if one stops doing so: it/// asserts that `$HOME` reaches `echo` as four literal characters.pub def Proc.shell_quote (s : String) : String := String.concat "'" (String.concat (Proc.escape_quotes s) "'")/// `cmd arg arg ...`, every word quoted.#[partial]def Proc.quoted_argv (cmd : String) (args : List String) : String := String.concat (Proc.shell_quote cmd) (Proc.quoted_args args)#[partial]def Proc.quoted_args (args : List String) : String := match args { List.empty => "", List.cons a rest => String.concat " " (String.concat (Proc.shell_quote a) (Proc.quoted_args rest)) }/// Where the redirect lands. Pid AND nanosecond, because a fixed `/tmp`/// name collides across concurrent runs and this corpus is swept sharded/// (scripts/check-monad-tests.sh runs MONAD_SWEEP_JOBS processes at once).////// Uniqueness is not GUARANTEED -- two captures in the same nanosecond on/// the same pid would share a path. Each call does a fork and an exec, so/// that cannot happen in practice; saying so is better than implying a/// guarantee this cannot make.def Proc.scratch_path : IO String := do { let nanos <- current_time_nano; return ("/tmp/monad_capture_" ++ I64.to_string process_id ++ "_" ++ I64.to_string nanos)}/// Read the redirect file, then remove it. Missing means `sh` never got/// far enough to create it, which is not an error here: the caller still/// gets the exit status, with empty output.////// The existence check is not belt-and-braces -- `read_file_native` still/// carries a `TODO Return Option and none on failure` and has no failure/// channel at all, so reading a file that is not there is exactly the case/// to keep it away from.////// `rm` rather than a native, because there is no removal native and this/// is already the established spelling (lang/src/codegen/test//// e2e_harness.mo and four slow_tests files all do `exec_cmd "rm"`).def Proc.read_then_remove (path : String) : IO String := do { let exists <- file_exists_native path; let out <- (if exists then read_file_native path else return ""); let _removed <- exec_cmd "rm" ["-f", path]; return out}/// Run `cmd args` and return its exit status together with everything it/// wrote, stdout and stderr MERGED.////// Merged on purpose. The callers are toolchain probes and failing/// external tools, and which stream carries the interesting text is not/// something they should have to know: `clang -dumpmachine` prints the/// triple on stdout, `llc --version` splits its target list across both/// depending on version, and a failed `mlir-opt` pass pipeline puts its/// ENTIRE signal on stderr (see plans/bootstrapping/mlir-codegen.md, which/// records that as a hard blocker). One string, one exit code.#[partial]pub def Proc.capture (cmd : String) (args : List String) : IO (Pair I64 String) := do { let tmp <- Proc.scratch_path; let script : String := Proc.quoted_argv cmd args ++ " > " ++ Proc.shell_quote tmp ++ " 2>&1"; let code <- exec_cmd "sh" ["-c", script]; let out <- Proc.read_then_remove tmp; return (Pair.pair code out)}// Tests live in `std/src/process_tests.mo`, not here, and that is forced// rather than stylistic: this module is one of the three `std/src/lib.mo`// re-exports (`path`, `io`, `process`), which the module loader seeds// ambiently into every closure. A `#[test]` in one of them is never// attributed to a TARGET module, so `monad test std/src/process.mo`// answers "No tests found" and the `monad test std` directory sweep skips// it silently -- verified by putting a trivial `def test_probe : Bool :=// true` in this file and watching both ignore it. That is why// `path_tests.mo`, `map_tests.mo` and `sha256_tests.mo` are separate files// too.