feat(frontends/lean/elaborator): do not execute tactics after error recovery

src/frontends/lean/elaborator.cpp

@@ -3692,6 +3692,13 @@ void elaborator::invoke_tactic(expr const & mvar, expr const & tactic) {
     expr type            = m_ctx.mctx().get_metavar_decl(mvar).get_type();
     tactic_state s       = mk_tactic_state_for(mvar);
 
+    if (has_synth_sorry({type, tactic})) {
+        // Skip if tactic or goal is broken. It is unlikely we will obtain
+        // any additional useful error messages.
+        m_ctx.assign(mvar, mk_sorry(some_expr(type), ref));
+        return;
+    }
+
     try {
         scoped_expr_caching scope(true);
         vm_obj r = tactic_evaluator(m_ctx, m_opts, ref)(tactic, s);

tests/lean/1207.lean.expected.out

@@ -4,7 +4,6 @@ context:
 h : tactic unit,
 _example : true
 ⊢ Type ?
-1207.lean:17:0: error: _interaction._lambda_3: trying to evaluate sorry
 1207.lean:21:23: error: unknown identifier 'foo'
 1207.lean:21:23: error: don't know how to synthesize placeholder
 context:

tests/lean/bad_error3.lean.expected.out

@@ -2,15 +2,7 @@ bad_error3.lean:1:33: error: type expected at
   p 0
 term has type
   ℕ → Prop
-bad_error3.lean:3:0: error: tactic failed, there are unsolved goals
-state:
-p : ℕ → ℕ → Prop
-⊢ ⁇
 bad_error3.lean:5:32: error: type expected at
   p 0
 term has type
   ℕ → Prop
-bad_error3.lean:7:0: error: tactic failed, there are unsolved goals
-state:
-p : ℕ → ℕ → Prop
-⊢ ⁇

tests/lean/begin_end_bug.lean.expected.out

@@ -5,4 +5,3 @@ a b c : ℕ,
 hab : a = b,
 hac : a = c
 ⊢ Type
-begin_end_bug.lean:3:48: error: _interaction._lambda_3: trying to evaluate sorry

tests/lean/elab_error_recovery.lean.expected.out

@@ -13,7 +13,6 @@ elab_error_recovery.lean:10:11: error: don't know how to synthesize placeholder
 context:
 half_baked : ℕ → ℕ
 ⊢ Type ?
-elab_error_recovery.lean:10:11: error: undefined
 elab_error_recovery.lean:12:20: error: invalid type ascription, term has type
   list ?m_1 : Type ?
 but is expected to have type

tests/lean/interactive/complete_tactic.lean.expected.out

@@ -2,8 +2,7 @@
 {"msgs":[{"caption":"","file_name":"complete_tactic.lean","pos_col":14,"pos_line":1,"severity":"error","text":"assumption tactic failed\nstate:\n⊢ ?m_1"},{"caption":"","file_name":"complete_tactic.lean","pos_col":8,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
 {"msgs":[{"caption":"","file_name":"complete_tactic.lean","pos_col":14,"pos_line":1,"severity":"error","text":"assumption tactic failed\nstate:\n⊢ ?m_1"},{"caption":"","file_name":"complete_tactic.lean","pos_col":8,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"complete_tactic.lean","pos_col":66,"pos_line":5,"severity":"error","text":"invalid expression, unexpected token"}],"response":"all_messages"}
 {"msgs":[{"caption":"","file_name":"complete_tactic.lean","pos_col":14,"pos_line":1,"severity":"error","text":"assumption tactic failed\nstate:\n⊢ ?m_1"},{"caption":"","file_name":"complete_tactic.lean","pos_col":8,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"complete_tactic.lean","pos_col":66,"pos_line":5,"severity":"error","text":"invalid expression, unexpected token"},{"caption":"","file_name":"complete_tactic.lean","pos_col":66,"pos_line":5,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Type ?"}],"response":"all_messages"}
-{"msgs":[{"caption":"","file_name":"complete_tactic.lean","pos_col":14,"pos_line":1,"severity":"error","text":"assumption tactic failed\nstate:\n⊢ ?m_1"},{"caption":"","file_name":"complete_tactic.lean","pos_col":8,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"complete_tactic.lean","pos_col":66,"pos_line":5,"severity":"error","text":"invalid expression, unexpected token"},{"caption":"","file_name":"complete_tactic.lean","pos_col":66,"pos_line":5,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Type ?"},{"caption":"","file_name":"complete_tactic.lean","pos_col":66,"pos_line":5,"severity":"error","text":"_interaction._lambda_3: trying to evaluate sorry"}],"response":"all_messages"}
-{"msgs":[{"caption":"","file_name":"complete_tactic.lean","pos_col":14,"pos_line":1,"severity":"error","text":"assumption tactic failed\nstate:\n⊢ ?m_1"},{"caption":"","file_name":"complete_tactic.lean","pos_col":8,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"complete_tactic.lean","pos_col":66,"pos_line":5,"severity":"error","text":"invalid expression, unexpected token"},{"caption":"","file_name":"complete_tactic.lean","pos_col":66,"pos_line":5,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Type ?"},{"caption":"","file_name":"complete_tactic.lean","pos_col":66,"pos_line":5,"severity":"error","text":"_interaction._lambda_3: trying to evaluate sorry"},{"caption":"","file_name":"complete_tactic.lean","pos_col":8,"pos_line":4,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"complete_tactic.lean","pos_col":14,"pos_line":1,"severity":"error","text":"assumption tactic failed\nstate:\n⊢ ?m_1"},{"caption":"","file_name":"complete_tactic.lean","pos_col":8,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"complete_tactic.lean","pos_col":66,"pos_line":5,"severity":"error","text":"invalid expression, unexpected token"},{"caption":"","file_name":"complete_tactic.lean","pos_col":66,"pos_line":5,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Type ?"},{"caption":"","file_name":"complete_tactic.lean","pos_col":8,"pos_line":4,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"prefix":"","response":"ok","seq_num":2}
 {"prefix":"","response":"ok","seq_num":5}

tests/lean/parser_error_recovery.lean.expected.out

@@ -42,5 +42,3 @@ parser_error_recovery.lean:37:13: error: don't know how to synthesize placeholde
 context:
 x : ℕ
 ⊢ Type ?
-no goals
-parser_error_recovery.lean:33:3: error: _interaction._lambda_3: trying to evaluate sorry

tests/lean/structure_instance_bug3.lean.expected.out

@@ -4,23 +4,3 @@ structure_instance_bug3.lean:1:23: error: failed to synthesize type class instan
 ⊢ has_pure set
 structure_instance_bug3.lean:1:23: error: failed to synthesize type class instance for
 ⊢ has_bind set
-structure_instance_bug3.lean:1:23: error: exact tactic failed, type mismatch, given expression has type
-  ?m_2 = ?m_2
-but is expected to have type
-  x >>= has_pure.pure set ∘ f = set.image f x
-state:
-3 goals
-α β : Type ?,
-f : α → β,
-x : set α
-⊢ x >>= has_pure.pure set ∘ f = set.image f x
-
-α β : Type ?,
-f : α → β,
-x : set α
-⊢ Sort ?
-
-α β : Type ?,
-f : α → β,
-x : set α
-⊢ ?m_1