From 13f0a7cd810db8ea2ae6cc6aca5adbf4eb9b3941 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Oct 2018 13:20:24 -0700 Subject: [PATCH] chore(frontends/lean, library/vm): save some debugging help code --- src/frontends/lean/pp.cpp | 1 + src/library/vm/vm.cpp | 7 ++++--- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index b826f9cb20..7b9974262c 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -1142,6 +1142,7 @@ auto pretty_fn::pp_proj(expr const & e) -> result { format arg_fmt = pp_child(proj_expr(e), max_bp()).fmt(); format idx_fmt(proj_idx(e).get_small_value() + 1); return result(arg_fmt + format(".") + idx_fmt); + // return result(arg_fmt + format("[") + format(proj_sname(e)) + format("].") + idx_fmt); } auto pretty_fn::pp_let(expr e) -> result { diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 0f982e3582..d17aa8d91b 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -2870,11 +2870,12 @@ void vm_state::run() { DEBUG_CODE({ /* We only trace VM in debug mode */ lean_trace(name({"vm", "run"}), - tout() << m_pc << ": "; + tout() << m_decl_vector[m_fn_idx].get_name() << " @ " << m_pc << ": "; instr.display(tout().get_stream()); tout() << "\n"; - display_stack(tout().get_stream()); - tout() << "\n";) + // display_stack(tout().get_stream()); + //tout() << "\n"; + ) }); switch (instr.op()) { case opcode::Push: