diff --git a/library/init/meta/base_tactic.lean b/library/init/meta/base_tactic.lean
index 62cac696f7..75769bdc93 100644
--- a/library/init/meta/base_tactic.lean
+++ b/library/init/meta/base_tactic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.monad init.meta.format
+import init.monad init.meta.exceptional init.meta.format
 /-
 Remark: we use a function that produces a format object as the exception information.
 Motivation: the formatting object may be big, and we may create it on demand.
@@ -62,8 +62,8 @@ meta_definition fail (e : format) : base_tactic S unit :=
 
 meta_definition try (t : base_tactic S A) : base_tactic S unit :=
 λ s, base_tactic_result.cases_on (t s)
- (λ a, success unit.star)
- (λ e, success unit.star s)
+ (λ a, success ())
+ (λ e, success () s)
 
 meta_definition or_else (t₁ t₂ : base_tactic S A) : base_tactic S A :=
 λ s, base_tactic_result.cases_on (t₁ s)
@@ -77,6 +77,12 @@ infix `<|>`:1 := or_else
 meta_definition skip : base_tactic S unit :=
 success unit.star
 
+meta_definition returnex (e : exceptional A) : base_tactic S A :=
+λ s, match e with
+| exceptional.success a    := base_tactic_result.success a s
+| !exceptional.exception f := !base_tactic_result.exception f
+end
+
 /- Decorate t's exceptions with msg -/
 meta_definition decorate_ex (msg : format) (t : base_tactic S A) : base_tactic S A :=
 λ s, base_tactic_result.cases_on (t s)
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index b13945451a..5d2321cd93 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -4,18 +4,33 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.base_tactic init.meta.environment
+import init.meta.base_tactic init.meta.environment init.trace
 
 meta_constant tactic_state : Type₁
 
 namespace tactic_state
 meta_constant env : tactic_state → environment
+meta_constant format_expr : tactic_state → expr → format
 end tactic_state
 
-open tactic
-
 meta_definition tactic [reducible] (A : Type) := base_tactic tactic_state A
 
+namespace tactic
+open tactic_state
+
 meta_definition get_env : tactic environment :=
 do s ← read,
-   return (tactic_state.env s)
+   return (env s)
+
+meta_definition get_decl (n : name) : tactic declaration :=
+do s ← read,
+   returnex (environment.get (env s) n)
+
+meta_definition trace (s : string) : tactic unit :=
+return (_root_.trace s (λ u, ()))
+
+meta_definition trace_expr (e : expr) : tactic unit :=
+do s ← read,
+   trace (to_string (format_expr s e))
+
+end tactic
diff --git a/library/init/monad.lean b/library/init/monad.lean
index 4b49b8b0f4..740909c598 100644
--- a/library/init/monad.lean
+++ b/library/init/monad.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson and Jared Roesch
 -/
 prelude
-import init.functor
+import init.functor init.string init.trace
 
 structure monad [class] (m : Type → Type) extends functor m : Type :=
 (ret  : Π {a:Type}, a → m a)
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index c149c7de96..7696a5887d 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -34,7 +34,12 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/replace_visitor.h"
 #include "library/string.h"
+#include "library/type_context.h"
 #include "library/definitional/equations.h"
+#include "library/vm/vm.h"
+#include "library/vm/vm_format.h"
+#include "library/vm/vm_expr.h"
+#include "library/tactic/tactic_state.h"
 #include "library/compiler/comp_irrelevant.h"
 #include "library/compiler/erase_irrelevant.h"
 #include "library/compiler/rec_fn_macro.h"
@@ -110,6 +115,21 @@ static optional<unsigned> to_unsigned(expr const & e) {
     return g_nat_numeral_pp->to_unsigned(e);
 }
 
+vm_obj tactic_state_format_expr(vm_obj const & o, vm_obj const & e) {
+    tactic_state const & s = to_tactic_state(o);
+    list<expr> const & gs  = s.goals();
+    local_context lctx;
+    if (gs) {
+        if (auto d = s.mctx().get_metavar_decl(head(gs))) {
+            lctx = d->get_context();
+        }
+    }
+    metavar_context mctx = s.mctx();
+    type_context tc(s.env(), s.get_options(), mctx, lctx, transparency_mode::All);
+    pretty_fn pp(s.env(), s.get_options(), tc);
+    return to_obj(pp(to_expr(e)));
+}
+
 void initialize_pp() {
     g_ellipsis_n_fmt  = new format(highlight(format("\u2026")));
     g_ellipsis_fmt    = new format(highlight(format("...")));
@@ -133,6 +153,7 @@ void initialize_pp() {
     g_partial_explicit_fmt    = new format(highlight_keyword(format("@@")));
     g_tmp_prefix      = new name(name::mk_internal_unique_name());
     g_nat_numeral_pp  = new nat_numeral_pp();
+    DECLARE_VM_BUILTIN(name({"tactic_state", "format_expr"}), tactic_state_format_expr);
 }
 
 void finalize_pp() {
diff --git a/tests/lean/run/meta_tac1.lean b/tests/lean/run/meta_tac1.lean
index 6dd5fc3918..679406b1b5 100644
--- a/tests/lean/run/meta_tac1.lean
+++ b/tests/lean/run/meta_tac1.lean
@@ -1,7 +1,16 @@
 set_option pp.all true
 
-open tactic
+open tactic name
 
 #tactic (∀ (p : Prop), p → p),
  do env ← get_env,
+    trace "testing",
+    return unit.star
+
+#tactic (∀ (p : Prop), p → p),
+ do d ← get_decl ("nat" <s> "add"),
+    trace_expr (declaration.type d),
+    trace "nat.rec type:",
+    d ← get_decl ("nat" <s> "rec"),
+    trace_expr (declaration.type d),
     return unit.star