From 2593c5bf601fa0b35595dcf911d922d303ac09ed Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 8 Jul 2025 14:16:37 -0700 Subject: [PATCH 1/2] feat(repl): Isolate stdout --- Repl.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Repl.lean b/Repl.lean index 963503b..2574dab 100644 --- a/Repl.lean +++ b/Repl.lean @@ -267,7 +267,10 @@ def execute (command: Protocol.Command): MainM Json := do try match fromJson? command.payload with | .ok args => do - match (← comm args |>.run) with + let (msg, result) ← IO.FS.withIsolatedStreams (isolateStderr := false) $ comm args + if !msg.isEmpty then + IO.eprintln s!"stdout: {msg}" + match result with | .ok result => return toJson result | .error ierror => return toJson ierror | .error error => return toJson $ errorCommand s!"Unable to parse json: {error}" From 855a882f7bfc8ee71007b3b64514f0f29b9e9e6c Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 8 Jul 2025 14:29:37 -0700 Subject: [PATCH 2/2] fix(repl): Extra newline in stdout bypass --- Repl.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Repl.lean b/Repl.lean index 2574dab..c7a997d 100644 --- a/Repl.lean +++ b/Repl.lean @@ -269,7 +269,7 @@ def execute (command: Protocol.Command): MainM Json := do | .ok args => do let (msg, result) ← IO.FS.withIsolatedStreams (isolateStderr := false) $ comm args if !msg.isEmpty then - IO.eprintln s!"stdout: {msg}" + IO.eprint s!"stdout: {msg}" match result with | .ok result => return toJson result | .error ierror => return toJson ierror