From 65bdb9c7e0c3b467a23b826fbc4b0e33e2b7b181 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Jan 2014 19:56:20 -0800 Subject: [PATCH] fix(frontends/lean): unprotected call to Lua API Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser_expr.cpp | 5 ++--- tests/lean/tacluacrash.lean | 2 ++ tests/lean/tacluacrash.lean.expected.out | 6 ++++++ 3 files changed, 10 insertions(+), 3 deletions(-) create mode 100644 tests/lean/tacluacrash.lean create mode 100644 tests/lean/tacluacrash.lean.expected.out diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp index 3ac59cb01..a79b5fc60 100644 --- a/src/frontends/lean/parser_expr.cpp +++ b/src/frontends/lean/parser_expr.cpp @@ -844,11 +844,10 @@ tactic parser_imp::parse_tactic_expr() { if (curr() == scanner::token::ScriptBlock) { parse_script_expr(); return using_script([&](lua_State * L) { - try { + if (is_tactic(L, -1)) return to_tactic(L, -1); - } catch (...) { + else throw parser_error("invalid script-block, it must return a tactic", p); - } }); } else if (curr_is_identifier() && m_tactic_macros && m_tactic_macros->find(curr_name()) != m_tactic_macros->end()) { return parse_tactic_macro(curr_name(), p); diff --git a/tests/lean/tacluacrash.lean b/tests/lean/tacluacrash.lean new file mode 100644 index 000000000..f630e35fd --- /dev/null +++ b/tests/lean/tacluacrash.lean @@ -0,0 +1,2 @@ +theorem T (a : Bool) : a → a. +(* foo_tac *) diff --git a/tests/lean/tacluacrash.lean.expected.out b/tests/lean/tacluacrash.lean.expected.out new file mode 100644 index 000000000..7e32db3dd --- /dev/null +++ b/tests/lean/tacluacrash.lean.expected.out @@ -0,0 +1,6 @@ + Set: pp::colors + Set: pp::unicode +tacluacrash.lean:2:0: error: invalid script-block, it must return a tactic +tacluacrash.lean:3:0: error: invalid tactic command, unexpected end of file +Proof state: +a : Bool, H : a ⊢ a