From 703d12d594f1591296d529e72794a00ba42dbade Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 2 Feb 2018 16:54:37 +0100 Subject: [PATCH] feat(frontends/lean/elaborator): do not execute tactics after error recovery --- src/frontends/lean/elaborator.cpp | 7 +++++++ tests/lean/1207.lean.expected.out | 1 - tests/lean/bad_error3.lean.expected.out | 8 -------- tests/lean/begin_end_bug.lean.expected.out | 1 - .../elab_error_recovery.lean.expected.out | 1 - .../complete_tactic.lean.expected.out | 3 +-- .../parser_error_recovery.lean.expected.out | 2 -- .../structure_instance_bug3.lean.expected.out | 20 ------------------- 8 files changed, 8 insertions(+), 35 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 71124bc571..d60dc0f6bc 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/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); diff --git a/tests/lean/1207.lean.expected.out b/tests/lean/1207.lean.expected.out index bf9abebb51..b35a43e798 100644 --- a/tests/lean/1207.lean.expected.out +++ b/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: diff --git a/tests/lean/bad_error3.lean.expected.out b/tests/lean/bad_error3.lean.expected.out index a8fb7ade66..aabbd0ff36 100644 --- a/tests/lean/bad_error3.lean.expected.out +++ b/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 -⊢ ⁇ diff --git a/tests/lean/begin_end_bug.lean.expected.out b/tests/lean/begin_end_bug.lean.expected.out index 449a13fff7..59fa19bdbf 100644 --- a/tests/lean/begin_end_bug.lean.expected.out +++ b/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 diff --git a/tests/lean/elab_error_recovery.lean.expected.out b/tests/lean/elab_error_recovery.lean.expected.out index 9f1946af9b..633110a9b7 100644 --- a/tests/lean/elab_error_recovery.lean.expected.out +++ b/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 diff --git a/tests/lean/interactive/complete_tactic.lean.expected.out b/tests/lean/interactive/complete_tactic.lean.expected.out index d74299c4f8..54ee5529d2 100644 --- a/tests/lean/interactive/complete_tactic.lean.expected.out +++ b/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} diff --git a/tests/lean/parser_error_recovery.lean.expected.out b/tests/lean/parser_error_recovery.lean.expected.out index bb2f346ff9..28cf256f29 100644 --- a/tests/lean/parser_error_recovery.lean.expected.out +++ b/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 diff --git a/tests/lean/structure_instance_bug3.lean.expected.out b/tests/lean/structure_instance_bug3.lean.expected.out index db64b8425a..a5b03e1099 100644 --- a/tests/lean/structure_instance_bug3.lean.expected.out +++ b/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