child process

Stream: lean4

[Arthur Paulino]

Hello! I'm trying to spawn a python child process and let the user use Python's REPL via my binary.

I'm doing this:

def List.pop : (l : List α) → l ≠ [] → α × Array α
  | a :: as, _ => (a, ⟨as⟩)

def spawn (cmd : String) : IO Unit := do
  let cmd := cmd.splitOn " "
  if h : cmd ≠ [] then
    let (cmd, args) := cmd.pop h
    let _ ← IO.Process.spawn {
      cmd := cmd
      args := args
    }

And then calling spawn "python". It almost works, except that the input/output gets buggy (I don't understand what happens).

How can I make this happen smoothly? The full code is here.

Thanks in advance!!!

[Arthur Paulino]

Ah, I had to use wait :D