diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 0f29376847..3d118d9285 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2647,6 +2647,9 @@ expr elaborator::visit_equations(expr const & e) {
     }
     new_e = instantiate_mvars(new_e);
     ensure_no_unassigned_metavars(new_e);
+    if (has_sorry(new_e))
+        // aborting here prevents many additional errors
+        throw elaborator_exception(e, "[abort visit_equation]").ignore_if(true);
     metavar_context mctx = m_ctx.mctx();
     expr r = compile_equations(m_env, *this, mctx, m_ctx.lctx(), new_e);
     m_ctx.set_env(m_env);
diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp
index a64da874d5..d18a96f631 100644
--- a/src/library/compiler/compiler.cpp
+++ b/src/library/compiler/compiler.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "library/max_sharing.h"
 #include "library/trace.h"
+#include "library/sorry.h"
 #include "library/vm/vm.h"
 #include "library/compiler/util.h"
 #include "library/compiler/lcnf.h"
@@ -92,7 +93,7 @@ environment compile(environment const & env, options const & opts, names const &
         return env;
 
     for (name const & c : cs) {
-        if (!env.get(c).is_definition() || is_vm_builtin_function(c))
+        if (!env.get(c).is_definition() || is_vm_builtin_function(c) || has_sorry(env.get(c).get_value()))
             return env;
     }