fix(frontends/lean): 'sorry' axiom auto generation

src/frontends/lean/definition_cmds.cpp

@@ -629,12 +629,13 @@ public:
                 throw exception("not a rfl-lemma, even though marked as rfl");
             return inline_new_defs(m_decl_env, elab.env(), val);
         } catch (exception & ex) {
+            // TODO(gabriel,leo): remove this catch block after single threaded queue discard bad tasks
             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(),
                                       ERROR);
             error_msg.set_exception(ex);
             error_msg.report();
-            return mk_sorry();
+            throw exception("failed to elaborate theorem");
         }
     }
 };
@@ -734,6 +735,7 @@ 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);
+    p.declare_sorry_if_used();
     elaborator elab(p.env(), p.get_options(), metavar_context(), local_context());
     buffer<expr> new_params;
     elaborate_params(elab, params, new_params);
@@ -798,6 +800,8 @@ 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());
         modifiers.m_is_noncomputable = true;
         environment new_env;
         try {

src/frontends/lean/elaborator.cpp

@@ -1454,10 +1454,6 @@ expr elaborator::visit_local(expr const & e, optional<expr> const & expected_typ
 }
 
 expr elaborator::visit_constant(expr const & e, optional<expr> const & expected_type) {
-    if (is_sorry(e)) {
-        m_env = declare_sorry(m_env);
-        m_ctx.set_env(m_env);
-    }
     return visit_app_core(e, buffer<expr>(), expected_type, e);
 }
 

src/frontends/lean/elaborator.h

@@ -289,6 +289,10 @@ public:
     expr finalize_theorem_proof(expr const & val, theorem_finalization_info const & info);
 
     environment const & env() const { return m_env; }
+    void set_env(environment const & env) {
+        m_env = env;
+        m_ctx.set_env(m_env);
+    }
 };
 
 pair<expr, level_param_names> elaborate(environment & env, options const & opts,

src/frontends/lean/parser.cpp

@@ -259,6 +259,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.
@@ -270,6 +271,11 @@ expr parser::mk_sorry(pos_info const & p) {
     return save_pos(::lean::mk_sorry(), p);
 }
 
+void parser::declare_sorry_if_used() {
+    if (m_used_sorry)
+        m_env = declare_sorry(m_env);
+}
+
 void parser::updt_options() {
     m_verbose        = get_verbose(m_ios.get_options());
     m_show_errors    = get_parser_show_errors(m_ios.get_options());

src/frontends/lean/parser.h

@@ -482,6 +482,7 @@ public:
 
     expr mk_sorry(pos_info const & p);
     bool used_sorry() const { return m_used_sorry; }
+    void declare_sorry_if_used();
 
     /** return true iff profiling is enabled */
     bool profiling() const { return m_profile; }

src/frontends/lean/util.cpp

@@ -257,6 +257,7 @@ level mk_result_level(buffer<level> const & r_lvls) {
 
 std::tuple<expr, level_param_names> parse_local_expr(parser & p, 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(mctx, e, check_unassigend);

tests/lean/bad_error1.lean.expected.out

@@ -4,4 +4,3 @@ given argument
   n
 expected argument
   m
-bad_error1.lean:3:0: error: unknown declaration 'sorry'

tests/lean/bug1.lean.expected.out

@@ -4,19 +4,16 @@ has type
   ∀ (c : bool), (p → q → c) → c
 but is expected to have type
   a
-bug1.lean:8:0: error: unknown declaration 'sorry'
 bug1.lean:13:3: error: type mismatch, expression
   λ (c : bool) (H : p → q → c), H H1 H2
 has type
   ∀ (c : bool), (p → q → c) → c
 but is expected to have type
   p ∧ p
-bug1.lean:12:0: error: unknown declaration 'sorry'
 bug1.lean:17:3: error: type mismatch, expression
   λ (c : bool) (H : p → q → c), H H1 H2
 has type
   ∀ (c : bool), (p → q → c) → c
 but is expected to have type
   q ∧ p
-bug1.lean:16:0: error: unknown declaration 'sorry'
 and_intro4 : ∀ (p q : bool), p → q → p ∧ q

tests/lean/def1.lean.expected.out

@@ -9,4 +9,3 @@ def1.lean:5:16: context: the inferred motive for the eliminator-like application
   λ (_x : A), f _x = f c
 def1.lean:5:3: context: the inferred motive for the eliminator-like application is
   λ (_x : A), f a = f c
-def1.lean:4:0: error: unknown declaration 'sorry'

tests/lean/elab_error_msgs.lean.expected.out

@@ -8,7 +8,6 @@ but is expected to have type
   ?m_1 → ?m_2 → ?m_3
 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:1:0: error: unknown declaration 'sorry'
 elab_error_msgs.lean:9:0: error: type mismatch at application
   bogus_elim trivial
 term
@@ -19,7 +18,6 @@ but is expected to have type
   ?m_2 ?m_3 ?m_3
 Additional information:
 elab_error_msgs.lean:9:0: context: 'eliminator' elaboration is not used for 'bogus_elim' because a (reliable) way to synthesize 'a', which occurs in the resulting type, was not found
-elab_error_msgs.lean:8:0: error: incorrect number of universe levels parameters for 'sorry', #1 expected, #0 provided
 elab_error_msgs.lean:13:20: error: failed to synthesize type class instance for
 a b : Prop,
 h : a ∧ b ∧ b,

tests/lean/eqn_compiler_loop.lean.expected.out

@@ -1,2 +1 @@
 eqn_compiler_loop.lean:3:8: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
-eqn_compiler_loop.lean:3:0: error: unknown declaration 'sorry'

tests/lean/noncomp_thm.lean.expected.out

@@ -1,2 +1 @@
-noncomp_thm.lean:1:0: error: unknown declaration 'sorry'
 noncomp_thm.lean:1:0: error: definition 'foo' was incorrectly marked as noncomputable

tests/lean/test_single.sh

@@ -24,8 +24,8 @@ echo "-- testing $f"
 "$LEAN" -Dpp.colors=false -Dpp.unicode=true -j0 "$ff" &> "$f.produced.out"
 sed "/warning: imported file uses 'sorry'/d" "$f.produced.out" > "$f.produced.out.tmp"
 sed "/warning: using 'sorry'/d" "$f.produced.out.tmp" > "$f.produced.out"
-sed "s|^$ff|$f|" "$f.produced.out" > "$f.produced.out.tmp"
-mv "$f.produced.out.tmp" "$f.produced.out"
+sed "/failed to elaborate theorem/d" "$f.produced.out" > "$f.produced.tmp"
+sed "s|^$ff|$f|" "$f.produced.tmp" > "$f.produced.out"
 if test -f "$f.expected.out"; then
     if diff --ignore-all-space -I "executing external script" "$f.produced.out" "$f.expected.out"; then
         echo "-- checked"

tests/lean/wrong_arity.lean.expected.out

@@ -1,2 +1 @@
 wrong_arity.lean:5:6: error: invalid match/equations expression, each case must have the same number of patterns
-wrong_arity.lean:3:0: error: unknown declaration 'sorry'