From 6d0b3afa7ef77371722378b75bdd87f7981e393a Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 17 Nov 2018 17:42:24 +0100
Subject: [PATCH] fix(library/compiler/compiler): do not silently abort on
 user-given `sorry`s

---
 src/library/compiler/compiler.cpp     | 2 +-
 tests/lean/run/array1.lean            | 6 ++----
 tests/lean/run/compiler_proj_bug.lean | 4 +---
 3 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp
index a6bc992e13..440fdc3f1e 100644
--- a/src/library/compiler/compiler.cpp
+++ b/src/library/compiler/compiler.cpp
@@ -93,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_builtin_constant(c) || has_sorry(env.get(c).get_value()))
+        if (!env.get(c).is_definition() || is_builtin_constant(c) || has_synthetic_sorry(env.get(c).get_value()))
             return env;
     }
     // TODO(Leo): generate boxed_version for builtin constants
diff --git a/tests/lean/run/array1.lean b/tests/lean/run/array1.lean
index 77409f2c69..9226b182a3 100644
--- a/tests/lean/run/array1.lean
+++ b/tests/lean/run/array1.lean
@@ -12,10 +12,8 @@ def w : array nat :=
 def f : fin w.sz → nat :=
 array.cases_on w (λ _ f, f)
 
-constant magic {a : Prop} : a
-
-#eval f ⟨1, magic⟩
-#eval f ⟨9, magic⟩
+#eval f ⟨1, sorry⟩
+#eval f ⟨9, sorry⟩
 
 #eval (((mk_array 1 1).push 2).push 3).foldl 0 (+)
 
diff --git a/tests/lean/run/compiler_proj_bug.lean b/tests/lean/run/compiler_proj_bug.lean
index 0d5b2dea22..e6be817614 100644
--- a/tests/lean/run/compiler_proj_bug.lean
+++ b/tests/lean/run/compiler_proj_bug.lean
@@ -4,6 +4,4 @@ structure S :=
 def f (s : S) :=
 s.b - s.a
 
-constant magic {p : Prop} : p
-
-#eval f {a := 5, b := 30, h := magic }
+#eval f {a := 5, b := 30, h := sorry }