Isolate std I/O streams during tactic execution #230

New Issue

aniva · 2025-07-08T14:07:34-07:00

aniva commented

2025-07-08 14:07:34 -07:00

This is to prevent stray outputs from jamming the repl. The relevant function is this one (IO.FS.withIsolatedStreams):

/--
Runs an action with `stdin` emptied and `stdout` and `stderr` captured into a `String`. If
`isolateStderr` is `false`, only `stdout` is captured.
-/
def withIsolatedStreams [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (x : m α)
    (isolateStderr := true) : m (String × α) := do
  let bIn ← mkRef { : Stream.Buffer }
  let bOut ← mkRef { : Stream.Buffer }
  let r ← withStdin (Stream.ofBuffer bIn) <|
    withStdout (Stream.ofBuffer bOut) <|
      (if isolateStderr then withStderr (Stream.ofBuffer bOut) else id) <|
        x
  let bOut ← liftM (m := BaseIO) bOut.get
  let out := String.fromUTF8! bOut.data
  pure (out, r)

This is to prevent stray outputs from jamming the repl. The relevant function is this one (`IO.FS.withIsolatedStreams`): ```lean /-- Runs an action with `stdin` emptied and `stdout` and `stderr` captured into a `String`. If `isolateStderr` is `false`, only `stdout` is captured. -/ def withIsolatedStreams [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (x : m α) (isolateStderr := true) : m (String × α) := do let bIn ← mkRef { : Stream.Buffer } let bOut ← mkRef { : Stream.Buffer } let r ← withStdin (Stream.ofBuffer bIn) <| withStdout (Stream.ofBuffer bOut) <| (if isolateStderr then withStderr (Stream.ofBuffer bOut) else id) <| x let bOut ← liftM (m := BaseIO) bOut.get let out := String.fromUTF8! bOut.data pure (out, r) ```

aniva added this to the 0.3.4 milestone 2025-07-08 14:07:34 -07:00

aniva added the

labels 2025-07-08 14:07:34 -07:00

aniva self-assigned this 2025-07-08 14:07:34 -07:00

aniva referenced a pull request that will close this issue

2025-07-08 14:11:04 -07:00

feat(repl): Replace StdIO when executing IO-based monads #231

aniva commented

2025-07-08 14:25:06 -07:00

I don't think its necessary to modify our current protocol to accomodate for such stray outputs. They should only exist in exceptional circumstances. For this reason, redirecting stdout to stderr is appropriate.

aniva commented

2025-07-08 14:28:50 -07:00

To verify:

lake exe repl Lean Init < interactions/run-tac.jsonl > /tmp/output.txt

where the input .jsonl is

frontend.process {"file": "example : Nat := by\n  run_tac do IO.println \"hi\"\n  exact 0", "readHeader": false, "inheritEnv": false, "sorrys": false, "typeErrorsAsGoals": false, "newConstants": false}
goal.start {"expr": "forall (n : Nat), n = n + 1"}
goal.tactic {"stateId": 0, "tactic": "run_tac do\n  IO.println \"hi\""}

Previously, such operation would jam the repl.

To verify: ```sh lake exe repl Lean Init < interactions/run-tac.jsonl > /tmp/output.txt ``` where the input `.jsonl` is ``` frontend.process {"file": "example : Nat := by\n run_tac do IO.println \"hi\"\n exact 0", "readHeader": false, "inheritEnv": false, "sorrys": false, "typeErrorsAsGoals": false, "newConstants": false} goal.start {"expr": "forall (n : Nat), n = n + 1"} goal.tactic {"stateId": 0, "tactic": "run_tac do\n IO.println \"hi\""} ``` Previously, such operation would jam the repl.

aniva commented

2025-07-08 14:30:14 -07:00

I have not tested it, but jamming stdin may be another issue.

aniva closed this issue

2025-07-08 14:30:51 -07:00

aniva added a new dependency 2025-07-08 14:31:26 -07:00

#231 feat(repl): Replace StdIO when executing IO-based monads

Sign in to join this conversation.