max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: print dbg* output to stderr

Browse source
This commit is contained in:
Sebastian Ullrich 2020-10-08 14:27:01 +02:00
parent 7c6b10012b
commit 8b62665788
2 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/System/IO.lean
View file

@ -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

10
src/runtime/object.cpp
View file

@ -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;
}