feat: replace OS-specific stream redirection with pure-Lean Stream redirection

This avoids the temporary files workaround on macOS and Windows, and makes sure
we can process a `#eval` command and write messages to stdout at the same time.

src/Init/System/IO.lean

@@ -133,10 +133,6 @@ constant setStdout : FS.Stream → IO FS.Stream := arbitrary _
 @[extern "lean_get_set_stderr"]
 constant setStderr : FS.Stream → IO FS.Stream := arbitrary _
 
-/-- Run action with `stdin` closed and `stdout+stderr` captured into a `String`. -/
-@[extern "lean_with_isolated_streams"]
-constant withIsolatedStreams {α : Type} : IO α → IO (String × Except IO.Error α) := arbitrary _
-
 @[specialize] partial def iterate {α β : Type} : α → (α → IO (Sum α β)) → IO β
 | a, f => do
   v ← f a;
@@ -296,6 +292,9 @@ liftIO $ out.putStr $ toString s
 
 def println {α} [HasToString α] (s : α) : m Unit := print s *> print "\n"
 
+@[export lean_io_println]
+private def printlnAux (s : String) : IO Unit := println s
+
 def eprint {α} [HasToString α] (s : α) : m Unit := do
 out ← getStderr;
 liftIO $ out.putStr $ toString s
@@ -417,6 +416,19 @@ def ofBuffer (r : Ref Buffer) : Stream := {
       { b with data := data.copySlice 0 b.data b.pos data.size false, pos := b.pos + data.size },
 }
 end Stream
+
+/-- Run action with `stdin` emptied and `stdout+stderr` captured into a `String`. -/
+def withIsolatedStreams {α : Type} (x : IO α) : IO (String × Except IO.Error α) := do
+bIn ← mkRef { : Stream.Buffer };
+bOut ← mkRef { : Stream.Buffer };
+r ← withStdin (Stream.ofBuffer bIn) $
+  withStdout (Stream.ofBuffer bOut) $
+    withStderr (Stream.ofBuffer bOut) $
+      observing x;
+bOut ← bOut.get;
+let out := String.fromUTF8Unchecked bOut.data;
+pure (out, r)
+
 end FS
 end IO
 
@@ -439,4 +451,7 @@ instance Unit.hasEval : HasEval Unit :=
 instance IO.HasEval {α : Type} [HasEval α] : HasEval (IO α) :=
 ⟨fun x _ => do a ← x; HasEval.eval a⟩
 
+def runEval {α : Type u} [HasEval α] (a : α) : IO (String × Except IO.Error Unit) :=
+IO.FS.withIsolatedStreams (HasEval.eval a false)
+
 end Lean

src/Lean/Elab/Command.lean

@@ -556,22 +556,21 @@ fun stx => withoutModifyingEnv do
     addAndCompile decl
   };
   let elabMetaEval : CommandElabM Unit := do {
-    act : IO Environment ← runTermElabM (some n) fun _ => do {
+    act ← runTermElabM (some n) fun _ => do {
       e    ← Term.elabTerm term none;
       Term.synthesizeSyntheticMVarsNoPostponing;
         e ← withLocalDeclD `env (mkConst `Lean.Environment) fun env =>
           withLocalDeclD `opts (mkConst `Lean.Options) fun opts => do {
-            e ← mkAppM `Lean.MetaHasEval.eval #[env, opts, e, toExpr false];
+            e ← mkAppM `Lean.runMetaEval #[env, opts, e];
             mkLambdaFVars #[env, opts] e
           };
         addAndCompile e;
         env ← getEnv;
         opts ← getOptions;
-        match env.evalConst (Environment → Options → IO Environment) n with
-        | Except.error e => throwError e
-        | Except.ok act  => pure $ act env opts
+      act ← ofExcept $ env.evalConst (Environment → Options → IO (String × Except IO.Error Environment)) n;
+      pure $ act env opts
     };
-    (out, res) ← liftIO $ IO.Prim.withIsolatedStreams act;
+    (out, res) ← liftIO act;
     logInfo out;
     match res with
     | Except.error e => throw $ Exception.error ref e.toString
@@ -579,18 +578,16 @@ fun stx => withoutModifyingEnv do
   };
   let elabEval : CommandElabM Unit := do {
     -- fall back to non-meta eval if MetaHasEval hasn't been defined yet
-    -- modify e to `HasEval.eval (hideUnit := false) e`
-    act : IO Unit ← runTermElabM (some n) fun _ => do {
+    -- modify e to `runEval e`
+    act ← runTermElabM (some n) fun _ => do {
       e    ← Term.elabTerm term none;
       Term.synthesizeSyntheticMVarsNoPostponing;
-      e ← mkAppM `Lean.HasEval.eval #[e, toExpr false];
+      e ← mkAppM `Lean.runEval #[e];
       addAndCompile e;
       env ← getEnv;
-      match env.evalConst (IO Unit) n with
-      | Except.error e => throwError e
-      | Except.ok act  => pure act
+      ofExcept $ env.evalConst (IO (String × Except IO.Error Unit)) n
     };
-    (out, res) ← liftIO $ IO.Prim.withIsolatedStreams act;
+    (out, res) ← liftIO act;
     logInfo out;
     match res with
     | Except.error e => throw $ Exception.error ref e.toString

src/Lean/Eval.lean

@@ -18,4 +18,7 @@ class MetaHasEval (α : Type u) :=
 instance metaHasEvalOfHasEval {α : Type u} [HasEval α] : MetaHasEval α :=
 ⟨fun env opts a hideUnit => do HasEval.eval a hideUnit; pure env⟩
 
+def runMetaEval {α : Type u} [MetaHasEval α] (env : Environment) (opts : Options) (a : α) : IO (String × Except IO.Error Environment) :=
+IO.FS.withIsolatedStreams (MetaHasEval.eval env opts a false)
+
 end Lean

src/frontends/lean/builtin_cmds.cpp

@@ -331,8 +331,6 @@ environment hide_cmd(parser & p) {
     return new_env;
 }
 
-void with_isolated_streams(std::string & streams_out, std::function<void()> fn);
-
 static environment eval_cmd(parser & p) {
     transient_cmd_scope cmd_scope(p);
     auto pos = p.pos();
@@ -356,8 +354,8 @@ static environment eval_cmd(parser & p) {
         expr env = tc.push_local("env", mk_const({"Lean", "Environment"}));
         expr opts = tc.push_local("opts", mk_const({"Lean", "Options"}));
         e = tc.mk_lambda(env, tc.mk_lambda(opts,
-                                           mk_app(tc, {"Lean", "MetaHasEval", "eval"}, 6,
-                                                  {type, *meta_eval_instance, env, opts, e, mk_bool_false()})));
+                                           mk_app(tc, {"Lean", "runMetaEval"}, 5,
+                                                  {type, *meta_eval_instance, env, opts, e})));
         // run `Environment -> Options -> IO Unit`
         args = { p.env().to_obj_arg(), p.get_options().to_obj_arg(), io_mk_world() };
     } else {
@@ -369,7 +367,7 @@ static environment eval_cmd(parser & p) {
 
         if (eval_instance) {
             /* Modify the 'program' to (HasEval.eval (hideUnit := false) e) */
-            e = mk_app(tc, {"Lean", "HasEval", "eval"}, 4, {type, *eval_instance, e, mk_bool_false()});
+            e = mk_app(tc, {"Lean", "runEval"}, 3, {type, *eval_instance, e});
             // run `IO Unit`
             args = { io_mk_world() };
         } else {
@@ -388,32 +386,27 @@ static environment eval_cmd(parser & p) {
 
     std::string streams_out;
     object_ref r;
-    try {
-        with_isolated_streams(streams_out, [&]() {
-            scope_traces_as_messages scope_traces(p.get_stream_name(), p.cmd_pos());
-            time_task t("#eval execution",
-                        message_builder(environment(), get_global_ios(), "foo", pos_info(), message_severity::INFORMATION));
-            r = object_ref(ir::run_boxed(new_env, fn_name, args.size(), &args[0]));
-        });
-    } catch (exception &) {
-        out << streams_out;
-        out.report();
-        throw;
+    {
+        scope_traces_as_messages scope_traces(p.get_stream_name(), p.cmd_pos());
+        time_task t("#eval execution",
+                    message_builder(environment(), get_global_ios(), "foo", pos_info(), message_severity::INFORMATION));
+        r = object_ref(ir::run_boxed(new_env, fn_name, args.size(), &args[0]));
     }
-    out << streams_out;
+    lean_assert(io_result_is_ok(r.raw()));
+    r = object_ref(io_result_get_value(r.raw()), true);
+    out << cnstr_get_ref_t<string_ref>(r, 0).to_std_string();
     out.report();
 
-    if (io_result_is_error(r.raw())) {
+    // `Except IO.Error _`
+    r = cnstr_get_ref(r, 1);
+    if (cnstr_tag(r.raw()) == 0) {
         message_builder msg = p.mk_message(p.cmd_pos(), p.pos(), ERROR);
-        object * err = io_result_get_error(r.raw());
-        inc(err);
-        object * str = lean_io_error_to_string(err);
-        msg << string_to_std(str);
+        string_ref str(lean_io_error_to_string(cnstr_get_ref_t<string_ref>(r, 0).to_obj_arg()));
+        msg << str.to_std_string();
         msg.report();
-        dec_ref(str);
         return p.env();
     } else if (meta_eval_instance) {
-        return environment(io_result_get_value(r.raw()), true);
+        return cnstr_get_ref_t<environment>(r, 0);
     } else {
         return p.env();
     }

src/runtime/io.cpp

@@ -183,82 +183,6 @@ static FILE * io_get_handle(lean_object * hfile) {
     return static_cast<FILE *>(lean_get_external_data(hfile));
 }
 
-void with_isolated_streams(std::string & streams_out, std::function<void()> fn) {
-    // When running `#eval`, we want to temporarily close stdin and capture stdout/stderr of the evaluated program
-    // so it doesn't interfere with the server I/O. We could do this on the Lean API level (i.e. `IO.getLine/putStr`),
-    // but that wouldn't affect direct access to `IO.stdin/...` nor FFI-called code. Instead, we directly work on file
-    // descriptors.
-    // Create a fresh file descriptor we can point stdout/stderr to
-#if defined(__linux__)
-    // On Linux, we can simply open an anonymous file in memory
-    int buf_fd = memfd_create("lean-eval", 0);
-#elif 0
-    // On macOS, we can open exclusive shared memory object, guessing a hopefully unique name
-    // ...or at least we should be able to, but it doesn't work for some reason.
-    // NOTE: what doesn't work: `funopen` returns a `FILE *` stream without a file descriptor
-    std::string shm_name = (sstream() << "lean-eval-" << getpid()).str();
-    int buf_fd = shm_open(shm_name.c_str(), O_RDWR | O_CREAT | O_EXCL, S_IRWXU);
-    lean_always_assert(shm_unlink(shm_name.c_str()) == 0);
-#else
-    // On Windows we can open an actual file I guess
-    FILE * buf_f = tmpfile(); lean_always_assert(buf_f != nullptr);
-    int buf_fd = fileno(buf_f);
-#endif
-    lean_always_assert(buf_fd >= 0);
-    // NOTE: what doesn't work: `pipe` creates file descriptors, but we would need a separate consumer thread so
-    // the evaluated program doesn't block on a full pipe
-
-    // make sure to drain user-level buffers
-    fflush(stdout); fflush(stderr);
-    // copy stdout/stderr, then set them to `buf_fd`
-#ifdef __linux__
-    // On Linux, we also redirect stdin so it appears as empty. This doesn't seem to work on other platforms.
-    // NOTE: Since we can't flush stdin, this only really works if we are on a line ending (assuming stdin is line buffered).
-    // This should be the case for the server, which is line-based.
-    int old_stdin  = dup(STDIN_FILENO);  lean_always_assert(old_stdin  >= 0); lean_always_assert(dup2(buf_fd, STDIN_FILENO)  >= 0);
-#endif
-    int old_stdout = dup(STDOUT_FILENO); lean_always_assert(old_stdout >= 0); lean_always_assert(dup2(buf_fd, STDOUT_FILENO) >= 0);
-    int old_stderr = dup(STDERR_FILENO); lean_always_assert(old_stderr >= 0); lean_always_assert(dup2(buf_fd, STDERR_FILENO) >= 0);
-
-    std::function<void()> finally = [&]() {
-        fflush(stdout); fflush(stderr);
-        // restore old streams
-#ifdef __linux__
-        lean_always_assert(dup2(old_stdin,  STDIN_FILENO)  >= 0); lean_always_assert(close(old_stdin) == 0);
-#endif
-        lean_always_assert(dup2(old_stdout, STDOUT_FILENO) >= 0); lean_always_assert(close(old_stdout) == 0);
-        lean_always_assert(dup2(old_stderr, STDERR_FILENO) >= 0); lean_always_assert(close(old_stderr) == 0);
-        // write `buf_fd` contents to `out`
-        off_t buf_sz = lseek(buf_fd, 0, SEEK_CUR);
-        lseek(buf_fd, 0, SEEK_SET);
-        std::string buf_s(buf_sz, '\0');
-        lean_always_assert(read(buf_fd, static_cast<void *>(&buf_s[0]), buf_sz) == buf_sz);
-        lean_always_assert(close(buf_fd) == 0);
-        streams_out = buf_s;
-    };
-
-    try {
-        fn();
-    } catch (exception &) {
-        finally();
-        throw;
-    }
-
-    finally();
-}
-
-/* withIsolatedStreams {α : Type} : IO α → IO (String × Except IO.Error α) */
-extern "C" obj_res lean_with_isolated_streams(obj_arg act, obj_arg w) {
-    std::string streams_out;
-    object_ref act_res;
-    with_isolated_streams(streams_out, [&]() { act_res = object_ref(apply_1(act, w)); });
-    if (io_result_is_ok(act_res.raw())) {
-        return set_io_result(mk_cnstr(0, mk_string(streams_out), mk_except_ok(object_ref(io_result_get_value(act_res.raw()), true))).steal());
-    } else {
-        return set_io_result(mk_cnstr(0, mk_string(streams_out), mk_except_error(object_ref(io_result_get_error(act_res.raw()), true))).steal());
-    }
-}
-
 obj_res decode_io_error(int errnum, b_obj_arg fname) {
     object * details = mk_string(strerror(errnum));
     switch (errnum) {

src/runtime/object.cpp

@@ -2018,27 +2018,15 @@ extern "C" object * lean_max_small_nat(object *) {
 // =======================================
 // Debugging helper functions
 
-void dbg_print_str(object * o) {
-    lean_assert(is_string(o));
-    std::cout << string_cstr(o) << "\n";
+extern "C" obj_res lean_io_println(obj_arg s, obj_arg w);
+void io_println(obj_arg s) {
+    object * r = lean_io_println(s, lean_io_mk_world());
+    lean_assert(lean_io_result_is_ok(r));
+    lean_dec(r);
 }
 
-void dbg_print_num(object * o) {
-    if (is_scalar(o)) {
-        std::cout << unbox(o) << "\n";
-    } else {
-        std::cout << mpz_value(o) << "\n";
-    }
-}
-
-static mutex g_dbg_mutex;
-
 extern "C" object * lean_dbg_trace(obj_arg s, obj_arg fn) {
-    {
-        unique_lock<mutex> lock(g_dbg_mutex);
-        std::cout << lean_string_cstr(s) << std::endl;
-    }
-    lean_dec(s);
+    io_println(s);
     return lean_apply_1(fn, lean_box(0));
 }
 
@@ -2050,10 +2038,8 @@ extern "C" object * lean_dbg_sleep(uint32 ms, obj_arg fn) {
 
 extern "C" object * lean_dbg_trace_if_shared(obj_arg s, obj_arg a) {
     if (lean_is_shared(a)) {
-        unique_lock<mutex> lock(g_dbg_mutex);
-        std::cout << "shared RC " << lean_string_cstr(s) << std::endl;
+        io_println(mk_string(std::string("shared RC ") + lean_string_cstr(s)));
     }
-    lean_dec(s);
     return a;
 }
 
@@ -2083,6 +2069,3 @@ void finalize_object() {
     delete g_ext_classes_mutex;
 }
 }
-
-extern "C" void lean_dbg_print_str(lean::object* o) { lean::dbg_print_str(o); }
-extern "C" void lean_dbg_print_num(lean::object* o) { lean::dbg_print_num(o); }

tests/lean/run/Reparen.lean

@@ -34,7 +34,7 @@ cmds.forM $ fun cmd => do
   some s ← pure cmd.reprint | throw $ IO.userError "cmd reprint failed";
   IO.print s
 
---#eval main ["../../../src/Init/Core.lean"]
+#eval main ["../../../src/Init/Core.lean"]
 
 def check (stx : Syntax) : CoreM Unit := do
 let stx' := unparen stx;