From 8b626657880fc48698a0ded8d745f74ee009a57b Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 8 Oct 2020 14:27:01 +0200 Subject: [PATCH] chore: print `dbg*` output to stderr --- src/Init/System/IO.lean | 6 +++--- src/runtime/object.cpp | 10 +++++----- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 1e359dc08b..8e6fe829d8 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -333,15 +333,15 @@ liftIO $ out.putStr $ toString s def println {α} [HasToString α] (s : α) : m Unit := print ((toString s).push '\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 def eprintln {α} [HasToString α] (s : α) : m Unit := eprint ((toString s).push '\n') +@[export lean_io_eprintln] +private def eprintlnAux (s : String) : IO Unit := eprintln s + def getEnv : String → m (Option String) := liftIO ∘ Prim.getEnv def realPath : String → m String := liftIO ∘ Prim.realPath def isDir : String → m Bool := liftIO ∘ Prim.isDir diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 23790c1c19..87410e2464 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -2019,15 +2019,15 @@ extern "C" object * lean_max_small_nat(object *) { // ======================================= // Debugging helper functions -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()); +extern "C" obj_res lean_io_eprintln(obj_arg s, obj_arg w); +void io_eprintln(obj_arg s) { + object * r = lean_io_eprintln(s, lean_io_mk_world()); lean_assert(lean_io_result_is_ok(r)); lean_dec(r); } extern "C" object * lean_dbg_trace(obj_arg s, obj_arg fn) { - io_println(s); + io_eprintln(s); return lean_apply_1(fn, lean_box(0)); } @@ -2039,7 +2039,7 @@ 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)) { - io_println(mk_string(std::string("shared RC ") + lean_string_cstr(s))); + io_eprintln(mk_string(std::string("shared RC ") + lean_string_cstr(s))); } return a; }