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: