diff --git a/src/frontends/lean/tactic_evaluator.cpp b/src/frontends/lean/tactic_evaluator.cpp
index 919d2cc0f3..988ab447a1 100644
--- a/src/frontends/lean/tactic_evaluator.cpp
+++ b/src/frontends/lean/tactic_evaluator.cpp
@@ -48,7 +48,11 @@ environment tactic_evaluator::compile_tactic(name const & tactic_name, expr cons
     new_env = new_env.add(cd);
     if (auto pos = provider->get_pos_info(tactic))
         new_env = add_transient_decl_pos_info(new_env, tactic_name, *pos);
-    return vm_compile(new_env, new_env.get(tactic_name));
+    try {
+        return vm_compile(new_env, new_env.get(tactic_name));
+    } catch (exception & ex) {
+        throw elaborator_exception(tactic, ex.what());
+    }
 }
 
 vm_obj tactic_evaluator::invoke_tactic(vm_state & S, name const & tactic_name, std::initializer_list<vm_obj> const & args) {
@@ -183,7 +187,11 @@ pair<vm_obj, tactic_state> tactic_evaluator::mk_smt_state(tactic_state const & s
     name init_state_name("_init_state");
     auto cd = check(new_env, mk_definition(new_env, init_state_name, {}, type, value, use_conv_opt, is_trusted));
     new_env = new_env.add(cd);
-    new_env = vm_compile(new_env, new_env.get(init_state_name));
+    try {
+        new_env = vm_compile(new_env, new_env.get(init_state_name));
+    } catch (exception & ex) {
+        throw elaborator_exception(ref, ex.what());
+    }
     vm_state S(new_env, m_opts);
     vm_obj r = S.invoke(init_state_name, to_obj(s));
     if (is_tactic_result_success(r)) {
diff --git a/tests/lean/bad_error5.lean b/tests/lean/bad_error5.lean
new file mode 100644
index 0000000000..c80839b5b1
--- /dev/null
+++ b/tests/lean/bad_error5.lean
@@ -0,0 +1,14 @@
+structure S :=
+  (α : Type)
+  (β : unit)
+
+structure T (c : S)
+
+structure U (c: S) (A : c^.α)
+
+definition V (c : S) : S :=
+{
+  α := T c,
+  -- code generation error should be shown on tactic
+  β := by sorry
+}
diff --git a/tests/lean/bad_error5.lean.expected.out b/tests/lean/bad_error5.lean.expected.out
new file mode 100644
index 0000000000..fc54467747
--- /dev/null
+++ b/tests/lean/bad_error5.lean.expected.out
@@ -0,0 +1 @@
+bad_error5.lean:13:10: error: code generation failed, VM does not have code for 'sorry'