diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index d06ca9f7c4..cc6df6d3e1 100644
--- a/library/init/meta/expr.lean
+++ b/library/init/meta/expr.lean
@@ -104,6 +104,11 @@ const `true []
 meta def mk_false : expr :=
 const `false []
 
+/-- Returns the sorry macro with the given type. -/
+meta constant mk_sorry (type : expr) : expr
+/-- Checks whether e is sorry, and returns its type. -/
+meta constant is_sorry (e : expr) : option expr
+
 meta def app_of_list : expr → list expr → expr
 | f []      := f
 | f (p::ps) := app_of_list (f p) ps
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 2ed42a8f7d..ec51786ca3 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -321,6 +321,9 @@ do e ← to_expr p,
 meta def trivial : tactic unit :=
 tactic.triv <|> tactic.reflexivity <|> tactic.contradiction <|> fail "trivial tactic failed"
 
+/-- Closes the main goal using sorry. -/
+meta def admit : tactic unit := tactic.admit
+
 /--
 This tactic applies to any goal. The contradiction tactic attempts to find in the current local context an hypothesis that is equivalent to
 an empty inductive type (e.g. `false`), a hypothesis of the form `c_1 ... = c_2 ...` where `c_1` and `c_2` are distinct constructors,
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 3da8784a87..d90432b034 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -763,6 +763,16 @@ do u ← mk_meta_univ,
    t ← mk_meta_var (expr.sort u),
    mk_meta_var t
 
+/-- Makes a sorry macro with a meta-variable as its type. -/
+meta def mk_sorry : tactic expr := do
+u ← mk_meta_univ,
+t ← mk_meta_var (expr.sort u),
+return $ expr.mk_sorry t
+
+/-- Closes the main goal using sorry. -/
+meta def admit : tactic unit :=
+target >>= exact ∘ expr.mk_sorry
+
 meta def mk_local' (pp_name : name) (bi : binder_info) (type : expr) : tactic expr := do
 uniq_name ← mk_fresh_name,
 return $ expr.local_const uniq_name pp_name bi type
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index a896b02f87..f0cd9c2bc2 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -23,10 +23,6 @@ option(JEMALLOC           "JEMALLOC"           OFF)
 # When OFF we disable JSON support to support older compilers
 option(JSON               "JSON"               ON)
 
-# IGNORE_SORRY is a tempory option (hack). It allows us to build
-# a version of Lean that does not report when 'sorry' is used.
-# This is useful for suppressing warning messages in the nightly builds.
-option(IGNORE_SORRY       "IGNORE_SORRY"      OFF)
 # When cross-compiling, we do not compile the standard library since
 # the executable will not work on the host machine
 option(CROSS_COMPILE      "CROSS_COMPILE"     OFF)
@@ -148,11 +144,6 @@ if (${CMAKE_SYSTEM_NAME} MATCHES "Linux")
   set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fPIC")
 endif()
 
-if (IGNORE_SORRY)
-  message(STATUS "IGNORE_SORRY is ON, Lean will not report when 'sorry' is used directly or indirectly")
-  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D LEAN_IGNORE_SORRY")
-endif()
-
 # SPLIT_STACK
 if (SPLIT_STACK)
   if ((${CMAKE_SYSTEM_NAME} MATCHES "Linux") AND ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index 265d03c108..d6670b7959 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -321,19 +321,22 @@ static certified_declaration check(parser & p, environment const & env, name con
     }
 }
 
-static void check_noncomputable(bool ignore_noncomputable, environment const & env, name const & c_name, name const & c_real_name, bool is_noncomputable,
+static bool check_noncomputable(bool ignore_noncomputable, environment const & env, name const & c_name, name const & c_real_name, bool is_noncomputable,
                                 std::string const & file_name, pos_info const & pos) {
     if (ignore_noncomputable)
-        return;
+        return true;
     if (!is_noncomputable && is_marked_noncomputable(env, c_real_name)) {
         auto reason = get_noncomputable_reason(env, c_real_name);
         lean_assert(reason);
-        throw exception(sstream() << "definition '" << c_name << "' is noncomputable, it depends on '" << *reason << "'");
+        report_message(message(file_name, pos, ERROR,
+                               (sstream() << "definition '" << c_name << "' is noncomputable, it depends on '" << *reason << "'").str()));
+        return false;
     }
     if (is_noncomputable && !is_marked_noncomputable(env, c_real_name)) {
         report_message(message(file_name, pos, WARNING,
                                (sstream() << "definition '" << c_name << "' was incorrectly marked as noncomputable").str()));
     }
+    return true;
 }
 
 static environment compile_decl(parser & p, environment const & env,
@@ -383,7 +386,8 @@ declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffe
         p.require_success(cdef.get_declaration().get_value_task());
     new_env           = module::add(new_env, cdef);
 
-    check_noncomputable(p.ignore_noncomputable(), new_env, c_name, c_real_name, modifiers.m_is_noncomputable, p.get_file_name(), pos);
+    if (!check_noncomputable(p.ignore_noncomputable(), new_env, c_name, c_real_name, modifiers.m_is_noncomputable, p.get_file_name(), pos))
+        p.set_error();
 
     if (modifiers.m_is_protected)
         new_env = add_protected(new_env, c_real_name);
@@ -756,8 +760,10 @@ public:
             auto cdef = check(new_env, def);
             new_env = module::add(new_env, cdef);
 
-            check_noncomputable(false, new_env, decl_name, def.get_name(), m_modifiers.m_is_noncomputable,
-                                m_pos_provider.get_file_name(), m_pos_provider.get_some_pos());
+            if (!check_noncomputable(false, new_env, decl_name, def.get_name(), m_modifiers.m_is_noncomputable,
+                                m_pos_provider.get_file_name(), m_pos_provider.get_some_pos())) {
+                throw std::exception(); // set parser to failed.
+            }
         } catch (exception & ex) {
             message_builder error_msg(&m_pos_provider, tc, m_decl_env, get_global_ios(),
                                       m_pos_provider.get_file_name(), m_pos_provider.get_some_pos(),
@@ -789,7 +795,6 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
     if (is_instance)
         attrs.set_attribute(p.env(), "instance");
     std::tie(fn, val) = parse_definition(p, lp_names, params, is_example, is_instance, modifiers.m_is_meta);
-    p.declare_sorry_if_used();
 
     // skip elaboration of definitions during reparsing
     if (p.get_break_at_pos())
@@ -865,11 +870,9 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
     } catch (throwable & ex1) {
         /* Try again using 'sorry' */
         expr sorry = p.mk_sorry(header_pos);
-        p.declare_sorry_if_used();
         elab.set_env(p.env());
         environment new_env;
         try {
-            modifiers.m_is_noncomputable = false;
             new_env = process(sorry);
         } catch (throwable & ex2) {
             /* Throw original error */
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index bb30e88176..d3c4e3e9ac 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2446,6 +2446,8 @@ expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_typ
         /* If the as_atomic macro is not the the function in a function application, then we need to consume
            implicit arguments. */
         return visit_base_app_core(new_e, arg_mask::Default, buffer<expr>(), true, expected_type, e);
+    } else if (is_sorry(e)) {
+        return copy_tag(e, expected_type ? mk_sorry(*expected_type) : mk_sorry(mk_type_metavar(e)));
     } else if (is_structure_instance(e)) {
         return visit_structure_instance(e, expected_type);
     } else if (is_annotation(e)) {
@@ -3185,9 +3187,6 @@ static expr resolve_local_name(environment const & env, local_context const & lc
         }
     }
 
-    if (id == "sorry")
-        return copy_tag(src, mk_constant(id));
-
     optional<expr> r;
     // globals
     if (env.find(id))
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 44d9c2c27a..8894268b6c 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -187,7 +187,6 @@ parser::parser(environment const & env, io_state const & ios,
     m_has_params = false;
     m_id_behavior  = id_behavior::ErrorIfUndef;
     m_found_errors = false;
-    m_used_sorry   = false;
     updt_options();
     m_next_tag_idx  = 0;
     m_curr = token_kind::Identifier;
@@ -244,23 +243,7 @@ void parser::scan() {
 }
 
 expr parser::mk_sorry(pos_info const & p) {
-    m_used_sorry = true;
-    m_ignore_noncomputable = true;
-    /* Remark: we should not declare 'sorry' here because we may be inside of a scope. */
-    {
-#ifndef LEAN_IGNORE_SORRY
-        // TODO(Leo): remove the #ifdef.
-        // The compilation option LEAN_IGNORE_SORRY is a temporary hack for the nightly builds
-        // We use it to avoid a buch of warnings on cdash.
-        (mk_message(p, WARNING) << "using 'sorry'").report();
-#endif
-    }
-    return save_pos(::lean::mk_sorry(), p);
-}
-
-void parser::declare_sorry_if_used() {
-    if (m_used_sorry)
-        m_env = declare_sorry(m_env);
+    return save_pos(::lean::mk_sorry(mk_Prop()), p);
 }
 
 void parser::updt_options() {
@@ -2221,6 +2204,35 @@ void parser::parse_imports(unsigned & fingerprint, std::vector<module_name> & im
     }
 }
 
+struct sorry_imports_task : public task<unit> {
+    environment m_env;
+    pos_info m_pos;
+    std::vector<generic_task_result> m_delayed_proofs;
+
+    sorry_imports_task(environment const & env, pos_info const & import_cmd_pos) : m_env(env), m_pos(import_cmd_pos) {
+        env.for_each_declaration([&] (declaration const & decl) {
+            if (decl.is_theorem()) m_delayed_proofs.push_back(decl.get_value_task());
+        });
+    }
+
+    void description(std::ostream & out) const override {
+        out << "Checking whether imported files use sorry";
+    }
+
+    std::vector<generic_task_result> get_dependencies() override {
+        return m_delayed_proofs;
+    }
+
+    bool is_tiny() const override { return true; }
+    bool do_priority_inversion() const override { return false; }
+
+    unit execute() override {
+        if (has_sorry(m_env))
+            report_message(message(get_module_id(), m_pos, WARNING, "imported file uses 'sorry'"));
+        return {};
+    }
+};
+
 void parser::process_imports() {
     unsigned fingerprint = 0;
     std::vector<module_name> imports;
@@ -2254,14 +2266,7 @@ void parser::process_imports() {
     m_env = update_fingerprint(m_env, fingerprint);
     m_env = activate_export_decls(m_env, {}); // explicitly activate exports in root namespace
     m_env = replay_export_decls_core(m_env, m_ios);
-    if (has_sorry(m_env)) {
-#ifndef LEAN_IGNORE_SORRY
-        // TODO(Leo): remove the #ifdef.
-        // The compilation option LEAN_IGNORE_SORRY is a temporary hack for the nightly builds
-        // We use it to avoid a buch of warnings on cdash.
-        (mk_message(m_last_cmd_pos, WARNING) << "imported file uses 'sorry'").report();
-#endif
-    }
+    get_global_task_queue()->submit<sorry_imports_task>(m_env, m_last_cmd_pos);
     m_imports_parsed = true;
 
     if (exception_during_scanning) std::rethrow_exception(exception_during_scanning);
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index feb8c46161..d90bc37cfe 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -58,7 +58,6 @@ class parser : public abstract_parser {
     unsigned                m_next_tag_idx;
     unsigned                m_next_inst_idx;
     bool                    m_found_errors;
-    bool                    m_used_sorry;
     pos_info_table          m_pos_table;
     // By default, when the parser finds a unknown identifier, it signs an error.
     // When the following flag is true, it creates a constant.
@@ -478,13 +477,13 @@ public:
     pair<expr, level_param_names> elaborate_type(name const & decl_name, metavar_context & mctx, expr const & e);
 
     expr mk_sorry(pos_info const & p);
-    bool used_sorry() const { return m_used_sorry; }
-    void declare_sorry_if_used();
 
     void require_success(generic_task_result const & t) {
         m_required_successes = cons(t, m_required_successes);
     }
 
+    void set_error() { m_found_errors = true; }
+
     /** return true iff profiling is enabled */
     bool profiling() const { return m_profile; }
 
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 1768f59358..f577994891 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <limits>
 #include <string>
 #include <util/utf8.h>
+#include "library/sorry.h"
 #include "util/flet.h"
 #include "util/fresh_name.h"
 #include "kernel/replace_fn.h"
@@ -1021,6 +1022,8 @@ auto pretty_fn::pp_macro(expr const & e) -> result {
         return pp(get_annotation_arg(e));
     } else if (is_rec_fn_macro(e)) {
         return format("[") + format(get_rec_fn_name(e)) + format("]");
+    } else if (is_sorry(e)) {
+        return format("sorry");
     } else {
         return pp_macro_default(e);
     }
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 62b183e234..a6889f3a52 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -264,7 +264,6 @@ level mk_result_level(buffer<level> const & r_lvls) {
 
 std::tuple<expr, level_param_names> parse_local_expr(parser & p, name const & decl_name, metavar_context & mctx, bool relaxed) {
     expr e = p.parse_expr();
-    p.declare_sorry_if_used();
     bool check_unassigend = !relaxed;
     expr new_e; level_param_names ls;
     std::tie(new_e, ls) = p.elaborate(decl_name, mctx, e, check_unassigend);
diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp
index 95fc0868d7..61bf906590 100644
--- a/src/library/compiler/vm_compiler.cpp
+++ b/src/library/compiler/vm_compiler.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/sorry.h"
 #include "library/noncomputable.h"
 #include "util/fresh_name.h"
 #include "util/sstream.h"
@@ -294,6 +295,8 @@ class vm_compiler_fn {
             compile(get_annotation_arg(e), bpz, m);
         } else if (is_quote(e)) {
             emit(mk_pexpr_instr(get_quote_expr(e)));
+        } else if (is_sorry(e)) {
+            compile_global(*get_vm_decl(m_env, "sorry"), 0, nullptr, bpz, m);
         } else {
             throw exception(sstream() << "code generation failed, unexpected kind of macro has been found: '"
                             << macro_def(e).get_name() << "'");
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 7bd840b4a6..7b730962fd 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -397,7 +397,6 @@ name const * g_smt_array = nullptr;
 name const * g_smt_select = nullptr;
 name const * g_smt_store = nullptr;
 name const * g_smt_prove = nullptr;
-name const * g_sorry = nullptr;
 name const * g_store = nullptr;
 name const * g_string = nullptr;
 name const * g_string_empty = nullptr;
@@ -875,7 +874,6 @@ void initialize_constants() {
     g_smt_select = new name{"smt", "select"};
     g_smt_store = new name{"smt", "store"};
     g_smt_prove = new name{"smt", "prove"};
-    g_sorry = new name{"sorry"};
     g_store = new name{"store"};
     g_string = new name{"string"};
     g_string_empty = new name{"string", "empty"};
@@ -1354,7 +1352,6 @@ void finalize_constants() {
     delete g_smt_select;
     delete g_smt_store;
     delete g_smt_prove;
-    delete g_sorry;
     delete g_store;
     delete g_string;
     delete g_string_empty;
@@ -1832,7 +1829,6 @@ name const & get_smt_array_name() { return *g_smt_array; }
 name const & get_smt_select_name() { return *g_smt_select; }
 name const & get_smt_store_name() { return *g_smt_store; }
 name const & get_smt_prove_name() { return *g_smt_prove; }
-name const & get_sorry_name() { return *g_sorry; }
 name const & get_store_name() { return *g_store; }
 name const & get_string_name() { return *g_string; }
 name const & get_string_empty_name() { return *g_string_empty; }
diff --git a/src/library/constants.h b/src/library/constants.h
index df8ebf9870..e079799c64 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -399,7 +399,6 @@ name const & get_smt_array_name();
 name const & get_smt_select_name();
 name const & get_smt_store_name();
 name const & get_smt_prove_name();
-name const & get_sorry_name();
 name const & get_store_name();
 name const & get_string_name();
 name const & get_string_empty_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 4249fde933..b401b9d7dd 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -392,7 +392,6 @@ smt.array
 smt.select
 smt.store
 smt.prove
-sorry
 store
 string
 string.empty
diff --git a/src/library/module.cpp b/src/library/module.cpp
index 09d30c968f..b37ab19429 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -296,10 +296,6 @@ struct decl_modification : public modification {
             decl = unfold_untrusted_macros(env, decl);
         }
 
-        if (decl.get_name() == get_sorry_name() && has_sorry(env)) {
-            // ignore double sorrys
-            return;
-        }
         // TODO(gabriel): this might be a bit more unsafe here than before
         env = import_helper::add_unchecked(env, decl);
     }
@@ -388,6 +384,37 @@ environment update_module_defs(environment const & env, declaration const & d) {
     }
 }
 
+struct add_decl_sorry_check : public task<unit> {
+    declaration m_decl;
+    pos_info m_pos;
+
+    add_decl_sorry_check(declaration const & decl, pos_info const & pos) :
+            m_decl(decl), m_pos(pos) {}
+
+    void description(std::ostream & out) const override {
+        out << "Checking added declaration " << m_decl.get_name() << " for use of sorry";
+    }
+
+    std::vector<generic_task_result> get_dependencies() override {
+        if (m_decl.is_theorem()) {
+            return {m_decl.get_value_task()};
+        } else {
+            return {};
+        }
+    }
+
+    bool is_tiny() const override { return true; }
+    task_kind get_kind() const override { return task_kind::elab; }
+
+    unit execute() override {
+        if (has_sorry(m_decl)) {
+            report_message(message(get_module_id(), m_pos, WARNING,
+                                   (sstream() << "declaration '" << m_decl.get_name() << "' uses sorry").str()));
+        }
+        return {};
+    }
+};
+
 environment add(environment const & env, certified_declaration const & d) {
     environment new_env = env.add(d);
     declaration _d = d.get_declaration();
@@ -395,6 +422,7 @@ environment add(environment const & env, certified_declaration const & d) {
         new_env = mark_noncomputable(new_env, _d.get_name());
     new_env = update_module_defs(new_env, _d);
     new_env = add(new_env, std::make_shared<decl_modification>(_d, env.trust_lvl()));
+    get_global_task_queue()->submit<add_decl_sorry_check>(_d, pos_info {g_curr_line, g_curr_column});
     return add_decl_pos_info(new_env, _d.get_name());
 }
 
diff --git a/src/library/sorry.cpp b/src/library/sorry.cpp
index 34f211ffa6..ce7b726e89 100644
--- a/src/library/sorry.cpp
+++ b/src/library/sorry.cpp
@@ -4,40 +4,94 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/sorry.h"
+#include <string>
 #include "kernel/type_checker.h"
 #include "kernel/environment.h"
 #include "library/module.h"
-#include "library/constants.h"
+#include "kernel/for_each_fn.h"
+#include "library/kernel_serializer.h"
 
 namespace lean {
-static name * g_l          = nullptr;
-static expr * g_sorry_type = nullptr;
+static name * g_sorry_name = nullptr;
+static macro_definition * g_sorry = nullptr;
+static std::string * g_sorry_opcode = nullptr;
+
+class sorry_macro_cell : public macro_definition_cell {
+public:
+    virtual name get_name() const override { return *g_sorry_name; }
+
+    unsigned int trust_level() const override { return 1; }
+
+    virtual expr check_type(expr const & sry, abstract_type_context & ctx, bool infer_only) const override {
+        if (!is_sorry(sry)) throw exception("invalid sorry macro");
+        auto sort = ctx.whnf(ctx.check(sorry_type(sry), infer_only));
+        if (!is_sort(sort)) throw exception("type of sorry macro is not a sort");
+        return sorry_type(sry);
+    }
+
+    virtual optional<expr> expand(expr const &, abstract_type_context &) const override {
+        return {};
+    }
+
+    virtual void write(serializer & s) const {
+        s.write_string(*g_sorry_opcode);
+    }
+};
 
 void initialize_sorry() {
-    g_l          = new name("l");
-    g_sorry_type = new expr(mk_pi("A", mk_sort(mk_param_univ(*g_l)), mk_var(0), binder_info(true)));
+    g_sorry_name = new name{"sorry"};
+    g_sorry_opcode = new std::string("Sorry");
+    g_sorry = new macro_definition(new sorry_macro_cell);
+
+    register_macro_deserializer(*g_sorry_opcode,
+        [] (deserializer &, unsigned num, expr const * args) {
+            if (num != 1) throw corrupted_stream_exception();
+            return mk_sorry(args[0]);
+        });
 }
 
 void finalize_sorry() {
-    delete g_sorry_type;
-    delete g_l;
+    delete g_sorry;
+    delete g_sorry_opcode;
+    delete g_sorry_name;
+}
+
+expr mk_sorry(expr const & ty) {
+    return mk_macro(*g_sorry, 1, &ty);
+}
+bool is_sorry(expr const & e) {
+    return is_macro(e) && macro_num_args(e) == 1 && macro_def(e) == *g_sorry;
+}
+
+bool has_sorry(expr const & ex) {
+    bool found_sorry = false;
+    for_each(ex, [&] (expr const & e, unsigned) {
+        if (found_sorry) return false;
+
+        if (is_sorry(e)) {
+            found_sorry = true;
+            return false;
+        }
+
+        return true;
+    });
+    return found_sorry;
+}
+
+bool has_sorry(declaration const & decl) {
+    return has_sorry(decl.get_type()) || (decl.is_definition() && has_sorry(decl.get_value()));
+}
+
+expr const & sorry_type(expr const & sry) {
+    return macro_arg(sry, 0);
 }
 
 bool has_sorry(environment const & env) {
-    auto decl = env.find(get_sorry_name());
-    return decl && decl->get_type() == *g_sorry_type;
+    bool found_sorry = false;
+    env.for_each_declaration([&] (declaration const & decl) {
+        if (!found_sorry && has_sorry(decl)) found_sorry = true;
+    });
+    return found_sorry;
 }
-
-environment declare_sorry(environment const & env) {
-    if (auto decl = env.find(get_sorry_name())) {
-        if (decl->get_type() != *g_sorry_type)
-            throw exception("failed to declare 'sorry', environment already has an object named 'sorry'");
-        return env;
-    } else {
-        return module::add(env, check(env, mk_constant_assumption(get_sorry_name(), list<name>(*g_l), *g_sorry_type)));
-    }
-}
-
-expr mk_sorry() { return mk_constant(get_sorry_name()); }
-bool is_sorry(expr const & e) { return is_constant(e) && const_name(e) == get_sorry_name(); }
 }
diff --git a/src/library/sorry.h b/src/library/sorry.h
index 2fe904f06a..2fde78f2a2 100644
--- a/src/library/sorry.h
+++ b/src/library/sorry.h
@@ -8,17 +8,17 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 
 namespace lean {
-/** \brief Return true iff the given environment has <tt>sorry.{l} : Pi {A : Type.{l}}, A</tt> */
+/** \brief Return true iff the given environment contains a sorry macro. */
 bool has_sorry(environment const & env);
+bool has_sorry(expr const &);
+bool has_sorry(declaration const &);
 
-/** \brief Declare <tt>sorry.{l} : Pi {A : Type.{l}}, A</tt> in the given environment if it doesn't already contain it.
-    Throw an exception if the environment already contains a declaration named \c sorry. */
-environment declare_sorry(environment const & env);
-
-/** \brief Return the constant \c sorry */
-expr mk_sorry();
-/** \brief Return true iff \c e is a sorry expression */
+/** \brief Returns the sorry macro with the specified type. */
+expr mk_sorry(expr const & ty);
+/** \brief Return true iff \c e is a sorry macro. */
 bool is_sorry(expr const & e);
+/** \brief Type of the sorry macro. */
+expr const & sorry_type(expr const & sry);
 void initialize_sorry();
 void finalize_sorry();
 }
diff --git a/src/library/vm/vm_aux.cpp b/src/library/vm/vm_aux.cpp
index 93470fcbb0..5264c5d4cf 100644
--- a/src/library/vm/vm_aux.cpp
+++ b/src/library/vm/vm_aux.cpp
@@ -32,7 +32,7 @@ vm_obj vm_trace_call_stack(vm_obj const &, vm_obj const & fn) {
     return invoke(fn, mk_vm_unit());
 }
 
-vm_obj vm_sorry(vm_obj const &) {
+vm_obj vm_sorry() {
     auto & s = get_vm_state();
     throw exception(sstream() << s.call_stack_fn(s.call_stack_size() - 1)
                               << ": trying to evaluate sorry");
diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp
index 29ddd31c41..231c7375dc 100644
--- a/src/library/vm/vm_expr.cpp
+++ b/src/library/vm/vm_expr.cpp
@@ -6,7 +6,8 @@ Author: Leonardo de Moura
 */
 #include <string>
 #include <iostream>
-#include <library/locals.h>
+#include "library/locals.h"
+#include "library/sorry.h"
 #include "kernel/expr.h"
 #include "kernel/free_vars.h"
 #include "kernel/instantiate.h"
@@ -418,6 +419,15 @@ vm_obj expr_is_choice_macro(vm_obj const & e) {
     return mk_vm_bool(is_choice(to_expr(e)));
 }
 
+vm_obj expr_mk_sorry(vm_obj const & t) {
+    return to_obj(mk_sorry(to_expr(t)));
+}
+
+vm_obj expr_is_sorry(vm_obj const & e_) {
+    auto & e = to_expr(e_);
+    return to_obj(is_sorry(e) ? some(sorry_type(e)) : none_expr());
+}
+
 void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name({"expr", "var"}),              expr_var);
     DECLARE_VM_BUILTIN(name({"expr", "sort"}),             expr_sort);
@@ -464,6 +474,9 @@ void initialize_vm_expr() {
 
     DECLARE_VM_BUILTIN(name("expr", "is_choice_macro"),    expr_is_choice_macro);
 
+    DECLARE_VM_BUILTIN(name("expr", "mk_sorry"), expr_mk_sorry);
+    DECLARE_VM_BUILTIN(name("expr", "is_sorry"), expr_is_sorry);
+
     // Not sure if we should expose these or what?
     DECLARE_VM_BUILTIN(name({"expr", "is_internal_cnstr"}), expr_is_internal_cnstr);
     DECLARE_VM_BUILTIN(name({"expr", "get_nat_value"}), expr_get_nat_value);
diff --git a/tests/lean/1162.lean.expected.out b/tests/lean/1162.lean.expected.out
index f8ab5643f8..8ae3324604 100644
--- a/tests/lean/1162.lean.expected.out
+++ b/tests/lean/1162.lean.expected.out
@@ -1 +1,3 @@
+1162.lean:7:4: warning: declaration 'ppday' uses sorry
+1162.lean:7:4: warning: declaration 'ppday.equations._eqn_1' uses sorry
 1162.lean:10:12: error: equation compiler error, equation #2 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
diff --git a/tests/lean/anc1.lean.expected.out b/tests/lean/anc1.lean.expected.out
index 25736cd0da..a8f4b9b6d7 100644
--- a/tests/lean/anc1.lean.expected.out
+++ b/tests/lean/anc1.lean.expected.out
@@ -1,5 +1,6 @@
 (1, 2) : ℕ × ℕ
 and.intro trivial trivial : true ∧ true
+anc1.lean:5:8: warning: declaration '_example' uses sorry
 psigma.mk 1 sorry : Σ' (x : ℕ), x > 0
 show true, from true.intro : true
 Exists.intro 1 (id_locked (1 ≠ 0) (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0
diff --git a/tests/lean/aux_decl_zeta.lean.expected.out b/tests/lean/aux_decl_zeta.lean.expected.out
index 7382fbffeb..f015dc58a2 100644
--- a/tests/lean/aux_decl_zeta.lean.expected.out
+++ b/tests/lean/aux_decl_zeta.lean.expected.out
@@ -1,3 +1,5 @@
+aux_decl_zeta.lean:5:11: warning: declaration 'f' uses sorry
+aux_decl_zeta.lean:5:11: warning: declaration 'f.equations._eqn_1' uses sorry
 aux_decl_zeta.lean:11:48: error: equation compiler failed to create auxiliary declaration 'f._match_1', auxiliary declaration has references to let-declarations (possible solution: use 'set_option eqn_compiler.zeta true')
 nested exception message:
 type mismatch at application
diff --git a/tests/lean/bad_error4.lean.expected.out b/tests/lean/bad_error4.lean.expected.out
index d2d96b55fb..fb280a8b8e 100644
--- a/tests/lean/bad_error4.lean.expected.out
+++ b/tests/lean/bad_error4.lean.expected.out
@@ -1,3 +1,5 @@
+bad_error4.lean:4:11: warning: declaration 'bar' uses sorry
+bad_error4.lean:4:11: warning: declaration 'bar.equations._eqn_1' uses sorry
 bad_error4.lean:5:0: error: type mismatch at application
   foo.mk (λ (a : unit) (b : delayed[?m_1]), delayed[?m_3])
 term
diff --git a/tests/lean/bad_error5.lean.expected.out b/tests/lean/bad_error5.lean.expected.out
index 2afafd6f02..bd6b7ce2d3 100644
--- a/tests/lean/bad_error5.lean.expected.out
+++ b/tests/lean/bad_error5.lean.expected.out
@@ -1 +1,3 @@
+bad_error5.lean:9:11: warning: declaration 'V' uses sorry
+bad_error5.lean:9:11: warning: declaration 'V.equations._eqn_1' uses sorry
 bad_error5.lean:9:0: error: _tactic._val_3: trying to evaluate sorry
diff --git a/tests/lean/bad_inaccessible.lean.expected.out b/tests/lean/bad_inaccessible.lean.expected.out
index 2bfa2331f3..d9f1b7ab0a 100644
--- a/tests/lean/bad_inaccessible.lean.expected.out
+++ b/tests/lean/bad_inaccessible.lean.expected.out
@@ -1,7 +1,13 @@
+bad_inaccessible.lean:2:11: warning: declaration 'f1' uses sorry
+bad_inaccessible.lean:2:11: warning: declaration 'f1.equations._eqn_1' uses sorry
 bad_inaccessible.lean:3:5: error: invalid use of inaccessible term, it is not fixed by other arguments
+bad_inaccessible.lean:5:11: warning: declaration 'f2' uses sorry
+bad_inaccessible.lean:5:11: warning: declaration 'f2.equations._eqn_1' uses sorry
 bad_inaccessible.lean:6:7: error: invalid use of inaccessible term, the provided term is
   b
 but is expected to be
   a
+bad_inaccessible.lean:12:11: warning: declaration 'foo' uses sorry
+bad_inaccessible.lean:12:11: warning: declaration 'foo.equations._eqn_1' uses sorry
 bad_inaccessible.lean:14:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments
   .?m_1 + 1
diff --git a/tests/lean/bad_inaccessible2.lean.expected.out b/tests/lean/bad_inaccessible2.lean.expected.out
index eac7867c00..0b936d9226 100644
--- a/tests/lean/bad_inaccessible2.lean.expected.out
+++ b/tests/lean/bad_inaccessible2.lean.expected.out
@@ -1,3 +1,5 @@
+bad_inaccessible2.lean:29:11: warning: declaration 'map_head' uses sorry
+bad_inaccessible2.lean:29:11: warning: declaration 'map_head.equations._eqn_1' uses sorry
 bad_inaccessible2.lean:31:2: error: type mismatch at application
   map_head (cons a va) (cons b vb)
 term
diff --git a/tests/lean/cls_err.lean.expected.out b/tests/lean/cls_err.lean.expected.out
index 56275436c4..fce47c3b93 100644
--- a/tests/lean/cls_err.lean.expected.out
+++ b/tests/lean/cls_err.lean.expected.out
@@ -1,3 +1,5 @@
+cls_err.lean:12:13: warning: declaration 'tst' uses sorry
+cls_err.lean:12:13: warning: declaration 'tst.equations._eqn_1' uses sorry
 cls_err.lean:13:2: error: failed to synthesize type class instance for
 A : Type u
 ⊢ H A
diff --git a/tests/lean/config.lean.expected.out b/tests/lean/config.lean.expected.out
deleted file mode 100644
index e69de29bb2..0000000000
diff --git a/tests/lean/ctx.lean.expected.out b/tests/lean/ctx.lean.expected.out
index b36c9b1f68..c2be0ffa4c 100644
--- a/tests/lean/ctx.lean.expected.out
+++ b/tests/lean/ctx.lean.expected.out
@@ -6,4 +6,6 @@ b1 b2 b3 : bool,
 h : A = B,
 p1 p2 : A × B
 ⊢ ℕ
+ctx.lean:2:11: warning: declaration 'foo' uses sorry
+ctx.lean:2:11: warning: declaration 'foo.equations._eqn_1' uses sorry
 ctx.lean:3:0: error: elaborator failed
diff --git a/tests/lean/def2.lean b/tests/lean/def2.lean
index a0e957bf6e..f72b34308e 100644
--- a/tests/lean/def2.lean
+++ b/tests/lean/def2.lean
@@ -6,5 +6,5 @@ val
 noncomputable definition foo2 : nat :=
 val
 
-noncomputable definition bla : nat :=
+definition bla : nat :=
 2
diff --git a/tests/lean/def2.lean.expected.out b/tests/lean/def2.lean.expected.out
index 987efe9829..2d379e5040 100644
--- a/tests/lean/def2.lean.expected.out
+++ b/tests/lean/def2.lean.expected.out
@@ -1 +1 @@
-def2.lean:3:0: error: definition 'foo' is noncomputable, it depends on 'val'
+def2.lean:3:11: error: definition 'foo' is noncomputable, it depends on 'val'
diff --git a/tests/lean/elab_error_msgs.lean.expected.out b/tests/lean/elab_error_msgs.lean.expected.out
index 0944df9267..2c0e7cadab 100644
--- a/tests/lean/elab_error_msgs.lean.expected.out
+++ b/tests/lean/elab_error_msgs.lean.expected.out
@@ -8,6 +8,8 @@ but is expected to have type
   ?m_1 → ?m_2 → ?m_4
 Additional information:
 elab_error_msgs.lean:2:0: context: 'eliminator' elaboration was not used for 'and.rec' because it is not fully applied, #2 explicit arguments expected
+elab_error_msgs.lean:5:4: warning: declaration 'bogus_elim' uses sorry
+elab_error_msgs.lean:5:4: warning: declaration 'bogus_elim.equations._eqn_1' uses sorry
 elab_error_msgs.lean:9:0: error: type mismatch at application
   bogus_elim trivial
 term
diff --git a/tests/lean/empty.lean.expected.out b/tests/lean/empty.lean.expected.out
index c0d6a6c209..51a18a581d 100644
--- a/tests/lean/empty.lean.expected.out
+++ b/tests/lean/empty.lean.expected.out
@@ -1,2 +1,5 @@
+empty.lean:6:25: warning: declaration 'v2' uses sorry
+empty.lean:6:25: warning: definition 'v2' was incorrectly marked as noncomputable
+empty.lean:6:25: warning: declaration 'v2.equations._eqn_1' uses sorry
 empty.lean:6:39: error: failed to synthesize type class instance for
 ⊢ nonempty Empty
diff --git a/tests/lean/eqn_hole.lean.expected.out b/tests/lean/eqn_hole.lean.expected.out
index e139ea06a2..d767c30ced 100644
--- a/tests/lean/eqn_hole.lean.expected.out
+++ b/tests/lean/eqn_hole.lean.expected.out
@@ -2,10 +2,14 @@ eqn_hole.lean:3:7: error: don't know how to synthesize placeholder
 context:
 f : ℕ → ℕ
 ⊢ ℕ
+eqn_hole.lean:2:11: warning: declaration 'f' uses sorry
+eqn_hole.lean:2:11: warning: declaration 'f.equations._eqn_1' uses sorry
 eqn_hole.lean:3:7: error: elaborator failed
 eqn_hole.lean:8:13: error: don't know how to synthesize placeholder
 context:
 g : ℕ → ℕ,
 n : ℕ
 ⊢ ℕ
+eqn_hole.lean:6:11: warning: declaration 'g' uses sorry
+eqn_hole.lean:6:11: warning: declaration 'g.equations._eqn_1' uses sorry
 eqn_hole.lean:8:13: error: elaborator failed
diff --git a/tests/lean/eval_expr_error.lean.expected.out b/tests/lean/eval_expr_error.lean.expected.out
index 509921e29e..e24b42dde5 100644
--- a/tests/lean/eval_expr_error.lean.expected.out
+++ b/tests/lean/eval_expr_error.lean.expected.out
@@ -1,3 +1,4 @@
+eval_expr_error.lean:3:9: warning: declaration 'tst1' uses sorry
 eval_expr_error.lean:5:8: error: invalid eval_expr, type must be a closed expression
 eval_expr_error.lean:8:0: error: invalid eval_expr, type mismatch
 state:
diff --git a/tests/lean/hole_in_fn.lean.expected.out b/tests/lean/hole_in_fn.lean.expected.out
index 7bdd51c1cb..c4818a499a 100644
--- a/tests/lean/hole_in_fn.lean.expected.out
+++ b/tests/lean/hole_in_fn.lean.expected.out
@@ -2,4 +2,6 @@ hole_in_fn.lean:6:13: error: don't know how to synthesize placeholder
 context:
 n : ℕ
 ⊢ ℕ
+hole_in_fn.lean:5:11: warning: declaration 'f' uses sorry
+hole_in_fn.lean:5:11: warning: declaration 'f.equations._eqn_1' uses sorry
 hole_in_fn.lean:6:13: error: elaborator failed
diff --git a/tests/lean/hole_issue2.lean.expected.out b/tests/lean/hole_issue2.lean.expected.out
index d66527346d..d8a2513d91 100644
--- a/tests/lean/hole_issue2.lean.expected.out
+++ b/tests/lean/hole_issue2.lean.expected.out
@@ -1,3 +1,5 @@
+hole_issue2.lean:12:25: warning: declaration 'count' uses sorry
+hole_issue2.lean:12:25: warning: declaration 'count.equations._eqn_1' uses sorry
 hole_issue2.lean:22:74: error: don't know how to synthesize placeholder
 context:
 A : Type,
@@ -9,6 +11,8 @@ h : ⟦l₁⟧ ⊆ ⟦l₂⟧,
 w : A,
 hw : ¬list.count w l₁ ≤ list.count w l₂
 ⊢ false
+hole_issue2.lean:18:25: warning: declaration 'decidable_subbag_1' uses sorry
+hole_issue2.lean:18:25: warning: declaration 'decidable_subbag_1.equations._eqn_1' uses sorry
 hole_issue2.lean:22:74: error: elaborator failed
 Additional information:
 hole_issue2.lean:19:0: context: the inferred motive for the eliminator-like application is
@@ -22,6 +26,8 @@ _match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦
 H : subcount l₁ l₂ = ff,
 h : ⟦l₁⟧ ⊆ ⟦l₂⟧
 ⊢ ∀ (a : A), ¬list.count a l₁ ≤ list.count a l₂ → false
+hole_issue2.lean:25:25: warning: declaration 'decidable_subbag_2' uses sorry
+hole_issue2.lean:25:25: warning: declaration 'decidable_subbag_2.equations._eqn_1' uses sorry
 hole_issue2.lean:29:65: error: elaborator failed
 Additional information:
 hole_issue2.lean:26:0: context: the inferred motive for the eliminator-like application is
@@ -35,6 +41,8 @@ _match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦
 H : subcount l₁ l₂ = ff,
 h : ⟦l₁⟧ ⊆ ⟦l₂⟧
 ⊢ false
+hole_issue2.lean:32:25: warning: declaration 'decidable_subbag_3' uses sorry
+hole_issue2.lean:32:25: warning: declaration 'decidable_subbag_3.equations._eqn_1' uses sorry
 hole_issue2.lean:36:28: error: elaborator failed
 Additional information:
 hole_issue2.lean:33:0: context: the inferred motive for the eliminator-like application is
diff --git a/tests/lean/inaccessible.lean.expected.out b/tests/lean/inaccessible.lean.expected.out
index ac7197d20e..e620936096 100644
--- a/tests/lean/inaccessible.lean.expected.out
+++ b/tests/lean/inaccessible.lean.expected.out
@@ -1,9 +1,15 @@
+inaccessible.lean:13:11: warning: declaration 'inv_3' uses sorry
+inaccessible.lean:13:11: warning: declaration 'inv_3.equations._eqn_1' uses sorry
 inaccessible.lean:14:10: error: function expected at
   mk
 inaccessible.lean:17:11: error: invalid inaccessible annotation, it cannot be used around functions in applications
 inaccessible.lean:25:12: error: invalid pattern, 'a' already appeared in this pattern
+inaccessible.lean:27:11: warning: declaration 'inv_7' uses sorry
+inaccessible.lean:27:11: warning: declaration 'inv_7.equations._eqn_1' uses sorry
 inaccessible.lean:28:3: error: function expected at
   f
 inaccessible.lean:31:4: error: invalid pattern, 'a' already appeared in this pattern
+inaccessible.lean:80:11: warning: declaration 'map_6' uses sorry
+inaccessible.lean:80:11: warning: declaration 'map_6.equations._eqn_1' uses sorry
 inaccessible.lean:82:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments
   .?m_1 + 1
diff --git a/tests/lean/inaccessible2.lean.expected.out b/tests/lean/inaccessible2.lean.expected.out
index 00bb267fdc..9dd4b921bc 100644
--- a/tests/lean/inaccessible2.lean.expected.out
+++ b/tests/lean/inaccessible2.lean.expected.out
@@ -1,4 +1,8 @@
+inaccessible2.lean:4:11: warning: declaration 'inv_1' uses sorry
+inaccessible2.lean:4:11: warning: declaration 'inv_1.equations._eqn_1' uses sorry
 inaccessible2.lean:5:7: error: invalid occurrence of 'inaccessible' annotation, it must only occur in patterns
 inaccessible2.lean:8:10: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
 inaccessible2.lean:11:11: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
+inaccessible2.lean:13:11: warning: declaration 'symm' uses sorry
+inaccessible2.lean:13:11: warning: declaration 'symm.equations._eqn_1' uses sorry
 inaccessible2.lean:14:9: error: invalid pattern, in a constructor application, the parameters of the inductive datatype must be marked as inaccessible
diff --git a/tests/lean/instance_cache1.lean.expected.out b/tests/lean/instance_cache1.lean.expected.out
index 461a6c7a1e..8c1d2fd009 100644
--- a/tests/lean/instance_cache1.lean.expected.out
+++ b/tests/lean/instance_cache1.lean.expected.out
@@ -3,6 +3,8 @@ A : Type ?,
 a : A,
 this : has_add A
 ⊢ has_add A
+instance_cache1.lean:5:11: warning: declaration 'f2' uses sorry
+instance_cache1.lean:5:11: warning: declaration 'f2.equations._eqn_1' uses sorry
 instance_cache1.lean:6:7: error: failed to synthesize type class instance for
 A : Type ?,
 a : A,
diff --git a/tests/lean/minimize_errors.lean.expected.out b/tests/lean/minimize_errors.lean.expected.out
index 3872bca04d..722ba80ca8 100644
--- a/tests/lean/minimize_errors.lean.expected.out
+++ b/tests/lean/minimize_errors.lean.expected.out
@@ -1,3 +1,5 @@
+minimize_errors.lean:1:4: warning: declaration 'f' uses sorry
+minimize_errors.lean:1:4: warning: declaration 'f.equations._eqn_1' uses sorry
 minimize_errors.lean:2:0: error: type mismatch, expression
   λ (a : ℕ), a
 has type
@@ -6,7 +8,7 @@ but is expected to have type
   ℕ → ℕ → ℕ
 f : ℕ → ℕ → ℕ
 g : ℕ → ℕ → ℕ
-noncomputable def g : ℕ → ℕ → ℕ :=
+def g : ℕ → ℕ → ℕ :=
 f
-noncomputable def h : ℕ → ℕ → ℕ :=
+def h : ℕ → ℕ → ℕ :=
 h._main
diff --git a/tests/lean/no_meta_rec_inst.lean.expected.out b/tests/lean/no_meta_rec_inst.lean.expected.out
index befcbb3fb6..336dffce4c 100644
--- a/tests/lean/no_meta_rec_inst.lean.expected.out
+++ b/tests/lean/no_meta_rec_inst.lean.expected.out
@@ -1,3 +1,4 @@
+no_meta_rec_inst.lean:4:9: warning: declaration 'n_has_false' uses sorry
 no_meta_rec_inst.lean:5:3: error: tactic.mk_instance failed to generate instance for
   has_false ℕ
 state:
diff --git a/tests/lean/non_exhaustive_error.lean.expected.out b/tests/lean/non_exhaustive_error.lean.expected.out
index 56703eab52..2aa91952a2 100644
--- a/tests/lean/non_exhaustive_error.lean.expected.out
+++ b/tests/lean/non_exhaustive_error.lean.expected.out
@@ -1 +1,3 @@
+non_exhaustive_error.lean:2:11: warning: declaration 'f' uses sorry
+non_exhaustive_error.lean:2:11: warning: declaration 'f.equations._eqn_1' uses sorry
 non_exhaustive_error.lean:2:11: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
diff --git a/tests/lean/noncomp.lean b/tests/lean/noncomp.lean
index 62bef47d72..162d670aa1 100644
--- a/tests/lean/noncomp.lean
+++ b/tests/lean/noncomp.lean
@@ -5,4 +5,4 @@ axiom n : nat
 definition f (x : nat) :=  -- Error this is not computable
 x + n
 
-noncomputable definition f (x : nat) := x + n
+noncomputable definition g (x : nat) := x + n
diff --git a/tests/lean/noncomp.lean.expected.out b/tests/lean/noncomp.lean.expected.out
index 08930de2bc..f1551d5720 100644
--- a/tests/lean/noncomp.lean.expected.out
+++ b/tests/lean/noncomp.lean.expected.out
@@ -1,5 +1 @@
-noncomp.lean:5:11: error: don't know how to synthesize placeholder
-context:
-x : ℕ
-⊢ Sort ?
-noncomp.lean:5:0: error: definition 'f' is noncomputable, it depends on 'n'
+noncomp.lean:5:11: error: definition 'f' is noncomputable, it depends on 'n'
diff --git a/tests/lean/noncomp_error.lean.expected.out b/tests/lean/noncomp_error.lean.expected.out
index 15d3c3dd03..e5d9d19aaf 100644
--- a/tests/lean/noncomp_error.lean.expected.out
+++ b/tests/lean/noncomp_error.lean.expected.out
@@ -1 +1 @@
-noncomp_error.lean:1:0: error: definition 'a' was incorrectly marked as noncomputable
+noncomp_error.lean:1:25: warning: definition 'a' was incorrectly marked as noncomputable
diff --git a/tests/lean/noncomp_thm.lean.expected.out b/tests/lean/noncomp_thm.lean.expected.out
index 398286f148..0cfbc17ccd 100644
--- a/tests/lean/noncomp_thm.lean.expected.out
+++ b/tests/lean/noncomp_thm.lean.expected.out
@@ -1 +1 @@
-noncomp_thm.lean:1:0: error: definition 'foo' was incorrectly marked as noncomputable
+noncomp_thm.lean:1:22: warning: definition 'foo' was incorrectly marked as noncomputable
diff --git a/tests/lean/quot_bug.lean.expected.out b/tests/lean/quot_bug.lean.expected.out
index d925317acc..d49b118ee6 100644
--- a/tests/lean/quot_bug.lean.expected.out
+++ b/tests/lean/quot_bug.lean.expected.out
@@ -1 +1,2 @@
 λ (x : A), f x
+quot_bug.lean:8:8: warning: declaration '_example' uses sorry
diff --git a/tests/lean/run/elab_crash1.lean b/tests/lean/run/elab_crash1.lean
index bc4d8773b1..ffcd4d9816 100644
--- a/tests/lean/run/elab_crash1.lean
+++ b/tests/lean/run/elab_crash1.lean
@@ -4,10 +4,10 @@ meta definition to_expr_target (a : pexpr) : tactic expr :=
 do tgt ← target,
    to_expr `((%%a : %%tgt))
 
-noncomputable example (A : Type) (a : A) : A :=
+example (A : Type) (a : A) : A :=
 by do to_expr_target `(sorry) >>= exact
 
-noncomputable example (A : Type) (a : A) : A :=
+example (A : Type) (a : A) : A :=
 by do refine `(sorry)
 
 example (a : nat) : nat :=
diff --git a/tests/lean/run/fun_info1.lean b/tests/lean/run/fun_info1.lean
index f670a1927d..1ff9c492f3 100644
--- a/tests/lean/run/fun_info1.lean
+++ b/tests/lean/run/fun_info1.lean
@@ -1,7 +1,7 @@
 open tactic
 
 set_option pp.binder_types true
-noncomputable definition foo (A : Type) : A → A :=
+definition foo (A : Type) : A → A :=
 sorry
 
 example (a : nat) (H : foo unit () = ()) : true :=
diff --git a/tests/lean/run/pack_unpack2.lean b/tests/lean/run/pack_unpack2.lean
index b2a548c493..060a327117 100644
--- a/tests/lean/run/pack_unpack2.lean
+++ b/tests/lean/run/pack_unpack2.lean
@@ -19,7 +19,7 @@ noncomputable definition bla {A : Type*} : ∀ n : tree A, P n
 check bla._main.equations._eqn_1
 check bla._main.equations._eqn_2
 
-noncomputable definition foo {A : Type*} : nat → tree A → nat
+definition foo {A : Type*} : nat → tree A → nat
 | 0     _                   := sorry
 | (n+1) (tree.leaf a)       := 0
 | (n+1) (tree.node [])      := foo n (tree.node [])
diff --git a/tests/lean/run/pack_unpack3.lean b/tests/lean/run/pack_unpack3.lean
index f5c8c7969b..16a2b4da9b 100644
--- a/tests/lean/run/pack_unpack3.lean
+++ b/tests/lean/run/pack_unpack3.lean
@@ -19,7 +19,7 @@ noncomputable definition {u} bla {A : Type u} : ∀ n : tree A, P n
 check bla._main.equations._eqn_1
 check bla._main.equations._eqn_2
 
-noncomputable definition {u} foo {A : Type u} : nat → tree A → nat
+definition {u} foo {A : Type u} : nat → tree A → nat
 | 0     _                                     := sorry
 | (n+1) (tree.leaf a)                         := 0
 | (n+1) (tree.node m xs)                      := foo n (tree.node m xs)
diff --git a/tests/lean/run/section3.lean b/tests/lean/run/section3.lean
index 36620ea715..771a6565ce 100644
--- a/tests/lean/run/section3.lean
+++ b/tests/lean/run/section3.lean
@@ -1,6 +1,6 @@
 section
   parameter (A : Type)
   definition foo := A
-  noncomputable definition bar {X : Type} {A : X} : foo :=
+  definition bar {X : Type} {A : X} : foo :=
   sorry
 end
diff --git a/tests/lean/run/sorry.lean b/tests/lean/run/sorry.lean
index 395ad20fd9..8685e3a5af 100644
--- a/tests/lean/run/sorry.lean
+++ b/tests/lean/run/sorry.lean
@@ -1,4 +1,4 @@
-noncomputable definition b : Prop :=
+definition b : Prop :=
 sorry
 
 theorem tst : true = false :=
diff --git a/tests/lean/run/unreachable_cases.lean b/tests/lean/run/unreachable_cases.lean
index 09606047a3..66d49b9245 100644
--- a/tests/lean/run/unreachable_cases.lean
+++ b/tests/lean/run/unreachable_cases.lean
@@ -6,14 +6,14 @@ inductive ifin : ℕ → Type -- inductively defined fin-type
 
 open ifin
 
-noncomputable definition foo {N : Type} : Π{n : ℕ}, N → ifin n → (N × ifin n)
+definition foo {N : Type} : Π{n : ℕ}, N → ifin n → (N × ifin n)
 | (succ k) n (fz .k) := sorry
 | (succ k) n (fs x) := sorry
 
-noncomputable definition bar {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
+definition bar {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
 | (succ k) (n, fz .k) := sorry
 | (succ k) (n, fs x) := sorry
 
-noncomputable definition bar2 {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
+definition bar2 {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
 | (succ k) (n, fz .k) := sorry
 | (succ k) (n, fs x) := sorry
diff --git a/tests/lean/set_attr1.lean.expected.out b/tests/lean/set_attr1.lean.expected.out
index a5e7ab33f3..a006e8d0ea 100644
--- a/tests/lean/set_attr1.lean.expected.out
+++ b/tests/lean/set_attr1.lean.expected.out
@@ -1,3 +1,5 @@
+set_attr1.lean:13:11: warning: declaration 'ex2' uses sorry
+set_attr1.lean:13:11: warning: declaration 'ex2.equations._eqn_1' uses sorry
 set_attr1.lean:14:3: error: tactic failed, there are unsolved goals
 state:
 n : ℕ
diff --git a/tests/lean/structure_instance_bug.lean.expected.out b/tests/lean/structure_instance_bug.lean.expected.out
index 5c1809dd8e..ac974aaa44 100644
--- a/tests/lean/structure_instance_bug.lean.expected.out
+++ b/tests/lean/structure_instance_bug.lean.expected.out
@@ -1 +1,3 @@
+structure_instance_bug.lean:10:11: warning: declaration 'foo3' uses sorry
+structure_instance_bug.lean:10:11: warning: declaration 'foo3.equations._eqn_1' uses sorry
 structure_instance_bug.lean:11:0: error: invalid structure value {...}, field 'B' is implicit and must not be provided
diff --git a/tests/lean/structure_instance_bug2.lean.expected.out b/tests/lean/structure_instance_bug2.lean.expected.out
index 0d7ac96c71..bcc718ab7c 100644
--- a/tests/lean/structure_instance_bug2.lean.expected.out
+++ b/tests/lean/structure_instance_bug2.lean.expected.out
@@ -1 +1,3 @@
+structure_instance_bug2.lean:3:4: warning: declaration 'my_pre_config1' uses sorry
+structure_instance_bug2.lean:3:4: warning: declaration 'my_pre_config1.equations._eqn_1' uses sorry
 structure_instance_bug2.lean:4:0: error: invalid structure instance, 'default_smt_pre_config' is not the name of a structure type
diff --git a/tests/lean/vm_sorry.lean b/tests/lean/vm_sorry.lean
index 707dd3d23d..5a3d508d1e 100644
--- a/tests/lean/vm_sorry.lean
+++ b/tests/lean/vm_sorry.lean
@@ -9,4 +9,12 @@ meta def my_partial_fun : bool → ℕ
 | tt := 42
 | ff := undefined
 
-vm_eval (my_partial_fun ff)
\ No newline at end of file
+vm_eval (my_partial_fun ff)
+
+open expr tactic
+run_command (do v ← to_expr `(half_baked ff) >>= whnf,
+                trace $ to_string v^.is_sorry)
+
+example : 0 = 1 := by admit
+example : 0 = 1 := by mk_sorry >>= exact
+example : 0 = 1 := by exact sorry
diff --git a/tests/lean/vm_sorry.lean.expected.out b/tests/lean/vm_sorry.lean.expected.out
index 1b86f1b245..75e604bc27 100644
--- a/tests/lean/vm_sorry.lean.expected.out
+++ b/tests/lean/vm_sorry.lean.expected.out
@@ -1,3 +1,10 @@
+vm_sorry.lean:1:4: warning: declaration 'half_baked._main' uses sorry
+vm_sorry.lean:1:4: warning: declaration 'half_baked._main.equations._eqn_1' uses sorry
+vm_sorry.lean:1:4: warning: declaration 'half_baked.equations._eqn_1' uses sorry
 42
-vm_sorry.lean:6:0: error: _main._val_1: trying to evaluate sorry
+vm_sorry.lean:6:0: error: half_baked._main._val_1: trying to evaluate sorry
 vm_sorry.lean:12:0: error: undefined
+(some nat)
+vm_sorry.lean:18:8: warning: declaration '_example' uses sorry
+vm_sorry.lean:19:8: warning: declaration '_example' uses sorry
+vm_sorry.lean:20:8: warning: declaration '_example' uses sorry