From bb81311e0a0ceccbf285d7ce3395ce5dd7d8ced7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 20 Dec 2013 17:15:12 -0800 Subject: [PATCH] feat(frontends/lean/parser): include proof state in exception for tactic failure Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 4 ++-- tests/lean/interactive/t10.lean.expected.out | 2 ++ tests/lean/interactive/t2.lean.expected.out | 2 ++ 3 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index daa9ac3d32..c611149d29 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1709,8 +1709,8 @@ class parser::imp { } switch (st) { case status::Done: return *pr; - case status::Eof: throw parser_error("invalid tactic command, unexpected end of file", pos()); - case status::Abort: throw parser_error("failed to prove theorem, proof has been aborted", pos()); + case status::Eof: throw tactic_cmd_error("invalid tactic command, unexpected end of file", pos(), s); + case status::Abort: throw tactic_cmd_error("failed to prove theorem, proof has been aborted", pos(), s); default: lean_unreachable(); // LCOV_EXCL_LINE } } diff --git a/tests/lean/interactive/t10.lean.expected.out b/tests/lean/interactive/t10.lean.expected.out index fd82763094..06ad68cb00 100644 --- a/tests/lean/interactive/t10.lean.expected.out +++ b/tests/lean/interactive/t10.lean.expected.out @@ -15,4 +15,6 @@ no goals ## Proof state: A : Bool, B : Bool, H : A ∧ B, H1 : A, H2 : B ⊢ B ∧ A ## Error (line: 18, pos: 0) failed to prove theorem, proof has been aborted +Proof state: +A : Bool, B : Bool, H : A ∧ B, H1 : A, H2 : B ⊢ B ∧ A # echo command after failure diff --git a/tests/lean/interactive/t2.lean.expected.out b/tests/lean/interactive/t2.lean.expected.out index 6b29f63b65..a2ad66205d 100644 --- a/tests/lean/interactive/t2.lean.expected.out +++ b/tests/lean/interactive/t2.lean.expected.out @@ -11,6 +11,8 @@ H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b ## Proof state: H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b ## Error (line: 9, pos: 5) failed to prove theorem, proof has been aborted +Proof state: +H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b # Assumed: a Assumed: b # Variable a : Bool