From ccb9faf0656469651ddb400da24242919c1c0f7e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 13 Jan 2014 16:54:21 -0800 Subject: [PATCH] refactor(*): error messages Signed-off-by: Leonardo de Moura --- doc/lua/lua.md | 2 +- src/CMakeLists.txt | 2 + src/frontends/lean/parser.cpp | 1 + src/frontends/lean/parser.h | 2 +- src/frontends/lean/parser_cmds.cpp | 2 +- src/frontends/lean/parser_error.cpp | 138 ++++--------- src/frontends/lean/parser_imp.cpp | 4 + src/frontends/lean/parser_imp.h | 61 +++--- src/frontends/lean/parser_macros.cpp | 11 +- src/frontends/lean/shell.cpp | 4 +- src/kernel/pos_info_provider.cpp | 4 +- src/kernel/pos_info_provider.h | 5 +- src/library/error_handling/CMakeLists.txt | 2 + src/library/error_handling/error_handling.cpp | 183 ++++++++++++++++++ src/library/error_handling/error_handling.h | 18 ++ src/library/kernel_bindings.cpp | 17 +- src/library/kernel_bindings.h | 8 +- src/library/parser_nested_exception.h | 25 +++ src/shell/lean.cpp | 160 +++++++-------- src/util/exception.h | 4 + src/util/lua.cpp | 17 +- src/util/script_exception.cpp | 24 ++- src/util/script_exception.h | 24 ++- tests/lean/alias3.lean.expected.out | 2 +- tests/lean/coercion1.lean.expected.out | 8 +- tests/lean/env_errors.lean.expected.out | 12 +- tests/lean/explicit.lean.expected.out | 2 +- tests/lean/interactive/t1.lean.expected.out | 10 +- tests/lean/interactive/t10.lean.expected.out | 6 +- tests/lean/interactive/t2.lean.expected.out | 4 +- tests/lean/interactive/t3.lean.expected.out | 2 +- tests/lean/interactive/t4.lean.expected.out | 2 +- tests/lean/lua15.lean.expected.out | 8 +- tests/lean/lua15b.lean | 13 ++ tests/lean/lua15b.lean.expected.out | 27 +++ tests/lean/parser1.lean | 20 ++ tests/lean/parser1.lean.expected.out | 6 + tests/lua/threads/sleep1.lua | 2 +- tests/lua/threads/th5.lua | 4 +- 39 files changed, 572 insertions(+), 274 deletions(-) create mode 100644 src/library/error_handling/CMakeLists.txt create mode 100644 src/library/error_handling/error_handling.cpp create mode 100644 src/library/error_handling/error_handling.h create mode 100644 src/library/parser_nested_exception.h create mode 100644 tests/lean/lua15b.lean create mode 100644 tests/lean/lua15b.lean.expected.out create mode 100644 tests/lean/parser1.lean create mode 100644 tests/lean/parser1.lean.expected.out diff --git a/doc/lua/lua.md b/doc/lua/lua.md index 69555ce5f..d8c7fcebe 100644 --- a/doc/lua/lua.md +++ b/doc/lua/lua.md @@ -304,7 +304,7 @@ print(o2) -- An error is raised if the option is not known. local ok, ex = pcall(function() options({"pp", "foo"}, true) end) assert(not ok) -assert(ex:what() == "unknown option 'pp::foo'") +assert(ex:what():find("unknown option 'pp::foo'")) ``` Options objects are non-mutable values. The method `update` returns a new diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 62dce5880..2acc77f0f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -223,6 +223,8 @@ add_subdirectory(library/elaborator) set(LEAN_LIBS ${LEAN_LIBS} elaborator) add_subdirectory(library/tactic) set(LEAN_LIBS ${LEAN_LIBS} tactic) +add_subdirectory(library/error_handling) +set(LEAN_LIBS ${LEAN_LIBS} error_handling) add_subdirectory(frontends/lean) set(LEAN_LIBS ${LEAN_LIBS} lean_frontend) add_subdirectory(frontends/lua) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 375d260b9..aa97bc9bd 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -14,6 +14,7 @@ namespace lean { parser::parser(environment const & env, io_state const & ios, std::istream & in, char const * strm_name, script_state * S, bool use_exceptions, bool interactive) { parser_imp::show_prompt(interactive, ios); m_ptr.reset(new parser_imp(env, ios, in, strm_name, S, use_exceptions, interactive)); + m_ptr->m_this = m_ptr; } parser::~parser() { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 11bbac355..dfc6e358c 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -16,7 +16,7 @@ class parser_imp; /** \brief Functional object for parsing commands and expressions */ class parser { private: - std::unique_ptr m_ptr; + std::shared_ptr m_ptr; public: parser(environment const & env, io_state const & st, std::istream & in, char const * strm_name, script_state * S, bool use_exceptions = true, bool interactive = false); ~parser(); diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp index 2388acba9..446110be4 100644 --- a/src/frontends/lean/parser_cmds.cpp +++ b/src/frontends/lean/parser_cmds.cpp @@ -83,7 +83,7 @@ void parser_imp::register_implicit_arguments(name const & n, parameter_buffer & /** \brief Throw an exception if \c e contains a metavariable */ -void parser_imp::check_no_metavar(expr const & e, metavar_env const & menv, char const * msg) { +void parser_imp::check_no_metavar(expr const & e, metavar_env const &, char const * msg) { if (has_metavar(e)) throw unsolved_metavar_exception(msg, e); } diff --git a/src/frontends/lean/parser_error.cpp b/src/frontends/lean/parser_error.cpp index ad8c1fd52..7948c4e7d 100644 --- a/src/frontends/lean/parser_error.cpp +++ b/src/frontends/lean/parser_error.cpp @@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "kernel/kernel_exception.h" #include "kernel/for_each_fn.h" #include "library/io_state_stream.h" -#include "library/elaborator/elaborator_justification.h" +#include "library/parser_nested_exception.h" +#include "library/error_handling/error_handling.h" #include "frontends/lean/parser_imp.h" namespace lean { @@ -21,94 +21,21 @@ void parser_imp::display_error_pos(unsigned line, unsigned pos) { void parser_imp::display_error_pos(pos_info const & p) { display_error_pos(p.first, p.second); } -void parser_imp::display_error_pos(optional const & e) { - if (e) { - auto it = m_expr_pos_info.find(*e); - if (it == m_expr_pos_info.end()) - return display_error_pos(m_last_cmd_pos); - else - return display_error_pos(it->second); - } else { - return display_error_pos(m_last_cmd_pos); - } -} - void parser_imp::display_error(char const * msg, unsigned line, unsigned pos) { display_error_pos(line, pos); regular(m_io_state) << " " << msg << endl; } -void parser_imp::display_error(char const * msg) { - display_error(msg, m_scanner.get_line(), m_scanner.get_pos()); -} - -void parser_imp::display_error(kernel_exception const & ex) { - optional main_expr = ex.get_main_expr(); - if (main_expr) - display_error_pos(some_expr(m_elaborator.get_original(*main_expr))); - else - display_error_pos(main_expr); - regular(m_io_state) << " " << ex << endl; -} - -void parser_imp::display_error(unsolved_metavar_exception const & ex) { - display_error_pos(some_expr(m_elaborator.get_original(ex.get_expr()))); - formatter fmt = m_io_state.get_formatter(); - options opts = m_io_state.get_options(); - unsigned indent = get_pp_indent(opts); - format r = nest(indent, compose(line(), fmt(ex.get_expr(), opts))); - regular(m_io_state) << " " << ex.what() << mk_pair(r, opts) << endl; - name_set already_displayed; - for_each(ex.get_expr(), [&](expr const & e, unsigned) -> bool { - if (is_metavar(e)) { - name const & m = metavar_name(e); - if (already_displayed.find(m) == already_displayed.end()) { - already_displayed.insert(m); - for (unsigned i = 0; i < indent; i++) regular(m_io_state) << " "; - display_error_pos(some_expr(m_elaborator.get_original(e))); - regular(m_io_state) << " unsolved metavar " << m << endl; - } - } - return true; - }); -} - std::pair parser_imp::lean_pos_info_provider::get_pos_info(expr const & e) const { - expr const & o = m_ref.m_elaborator.get_original(e); - auto it = m_ref.m_expr_pos_info.find(o); - if (it == m_ref.m_expr_pos_info.end()) - throw exception("position is not available"); // information is not available + expr const & o = m_parser->m_elaborator.get_original(e); + auto it = m_parser->m_expr_pos_info.find(o); + if (it == m_parser->m_expr_pos_info.end()) + return m_pos; return it->second; } -char const * parser_imp::lean_pos_info_provider::get_file_name(expr const & ) const { - return m_ref.m_strm_name.c_str(); -} - -void parser_imp::display_error(elaborator_exception const & ex) { - formatter fmt = m_io_state.get_formatter(); - options opts = m_io_state.get_options(); - lean_pos_info_provider pos_provider(*this); - auto j = ex.get_justification(); - j = remove_detail(j); - regular(m_io_state) << mk_pair(j.pp(fmt, opts, &pos_provider, true), opts) << endl; -} - -void parser_imp::display_error(script_exception const & ex) { - switch (ex.get_source()) { - case script_exception::source::String: - display_error_pos(ex.get_line() + m_last_script_pos.first - 1, static_cast(-1)); - regular(m_io_state) << " executing script," << ex.get_msg() << endl; - break; - case script_exception::source::File: - display_error_pos(m_last_script_pos); - regular(m_io_state) << " executing external script (" << ex.get_filename() << ":" << ex.get_line() << ")," << ex.get_msg() << endl; - break; - case script_exception::source::Unknown: - display_error_pos(m_last_script_pos); - regular(m_io_state) << " executing script, exact error position is not available, " << ex.what() << endl; - break; - } +char const * parser_imp::lean_pos_info_provider::get_file_name() const { + return m_parser->m_strm_name.c_str(); } void parser_imp::display_error(tactic_cmd_error const & ex) { @@ -116,13 +43,21 @@ void parser_imp::display_error(tactic_cmd_error const & ex) { display_proof_state(ex.m_state); } -#define CATCH_CORE(ShowError, ThrowError) \ -m_found_errors = true; \ -if (m_show_errors) { ShowError ; } \ -sync(); \ -if (m_use_exceptions) { ThrowError ; } +void parser_imp::display_error(exception const & ex) { + lean_pos_info_provider pos_provider(m_this.lock(), m_last_cmd_pos); + ::lean::display_error(m_io_state, &pos_provider, ex); +} -#define CATCH(ShowError) CATCH_CORE(ShowError, throw;) +void parser_imp::display_error(script_exception const & ex) { + lean_pos_info_provider pos_provider(m_this.lock(), m_last_script_pos); + ::lean::display_error(m_io_state, &pos_provider, ex); +} + +#define CATCH(ShowError, ThrowError) \ +m_found_errors = true; \ +if (!m_use_exceptions && m_show_errors) { ShowError ; } \ +sync(); \ +if (m_use_exceptions) { ThrowError ; } /** \brief Execute the given function \c f, and handle exceptions occurring @@ -133,21 +68,14 @@ void parser_imp::protected_call(std::function && f, std::function && f, std::function(ex.clone()), + std::shared_ptr(new lean_pos_info_provider(m_this.lock(), m_last_script_pos)))); } catch (exception & ex) { - CATCH(display_error(ex.what());); + reset_interrupt(); + CATCH(display_error(ex), + throw parser_nested_exception(std::shared_ptr(ex.clone()), + std::shared_ptr(new lean_pos_info_provider(m_this.lock(), m_last_cmd_pos)))); } } } diff --git a/src/frontends/lean/parser_imp.cpp b/src/frontends/lean/parser_imp.cpp index ebfa53dd4..ce88c08aa 100644 --- a/src/frontends/lean/parser_imp.cpp +++ b/src/frontends/lean/parser_imp.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include "library/io_state_stream.h" +#include "library/parser_nested_exception.h" #include "frontends/lean/parser_imp.h" #include "frontends/lean/parser_macros.h" #include "frontends/lean/parser_calc.h" @@ -217,6 +218,9 @@ expr parser_imp::parse_expr_main() { return p.first; } catch (parser_error & ex) { throw parser_exception(ex.what(), m_strm_name.c_str(), ex.m_pos.first, ex.m_pos.second); + } catch (exception & ex) { + throw parser_nested_exception(std::shared_ptr(ex.clone()), + std::shared_ptr(new lean_pos_info_provider(m_this.lock(), m_last_cmd_pos))); } } }; diff --git a/src/frontends/lean/parser_imp.h b/src/frontends/lean/parser_imp.h index 65ba94893..f3f7b714b 100644 --- a/src/frontends/lean/parser_imp.h +++ b/src/frontends/lean/parser_imp.h @@ -34,7 +34,7 @@ bool get_parser_show_errors(options const & opts); /** \brief Auxiliary object that stores a reference to the parser object inside the Lua State */ struct set_parser { - script_state * m_state; + script_state::weak_ref m_state; parser_imp * m_prev; set_parser(script_state * S, parser_imp * ptr); ~set_parser(); @@ -57,29 +57,30 @@ class parser_imp { typedef expr_map expr_pos_info; typedef expr_map tactic_hints; // a mapping from placeholder to tactic typedef scoped_map using_decls; - environment m_env; - io_state m_io_state; - scanner m_scanner; - std::string m_strm_name; // input stream name - frontend_elaborator m_elaborator; - macros const * m_expr_macros; - macros const * m_cmd_macros; - macros const * m_tactic_macros; - scanner::token m_curr; - bool m_use_exceptions; - bool m_interactive; - bool m_found_errors; - local_decls m_local_decls; - unsigned m_num_local_decls; - expr_pos_info m_expr_pos_info; - pos_info m_last_cmd_pos; - pos_info m_last_script_pos; - tactic_hints m_tactic_hints; - using_decls m_using_decls; - std::vector m_namespace_prefixes; enum class scope_kind { Scope, Namespace }; - std::vector m_scope_kinds; + std::weak_ptr m_this; + environment m_env; + io_state m_io_state; + scanner m_scanner; + std::string m_strm_name; // input stream name + frontend_elaborator m_elaborator; + macros const * m_expr_macros; + macros const * m_cmd_macros; + macros const * m_tactic_macros; + scanner::token m_curr; + bool m_use_exceptions; + bool m_interactive; + bool m_found_errors; + local_decls m_local_decls; + unsigned m_num_local_decls; + expr_pos_info m_expr_pos_info; + pos_info m_last_cmd_pos; + pos_info m_last_script_pos; + tactic_hints m_tactic_hints; + using_decls m_using_decls; + std::vector m_namespace_prefixes; + std::vector m_scope_kinds; std::unique_ptr m_calc_proof_parser; @@ -202,22 +203,20 @@ public: private: void display_error_pos(unsigned line, unsigned pos); void display_error_pos(pos_info const & p); - void display_error_pos(optional const & e); void display_error(char const * msg, unsigned line, unsigned pos); - void display_error(char const * msg); - void display_error(kernel_exception const & ex); - void display_error(unsolved_metavar_exception const & ex); struct lean_pos_info_provider : public pos_info_provider { - parser_imp const & m_ref; - lean_pos_info_provider(parser_imp const & r):m_ref(r) {} + std::shared_ptr m_parser; + pos_info m_pos; + lean_pos_info_provider(std::shared_ptr const & p, pos_info const & pos):m_parser(p), m_pos(pos) {} virtual std::pair get_pos_info(expr const & e) const; - virtual char const * get_file_name(expr const & e) const; + virtual std::pair get_some_pos() const { return m_pos; } + virtual char const * get_file_name() const; }; - void display_error(elaborator_exception const & ex); - void display_error(script_exception const & ex); void display_error(tactic_cmd_error const & ex); + void display_error(script_exception const & ex); + void display_error(exception const & ex); public: void protected_call(std::function && f, std::function && sync); /*@}*/ diff --git a/src/frontends/lean/parser_macros.cpp b/src/frontends/lean/parser_macros.cpp index 5f8bd725e..d242c6186 100644 --- a/src/frontends/lean/parser_macros.cpp +++ b/src/frontends/lean/parser_macros.cpp @@ -24,9 +24,9 @@ parser_imp * get_parser(lua_State * L) { } set_parser::set_parser(script_state * S, parser_imp * ptr) { - m_state = S; - if (m_state) { - m_state->apply([&](lua_State * L) { + if (S) { + m_state = S->to_weak_ref(); + S->apply([&](lua_State * L) { m_prev = get_parser(L); lua_pushlightuserdata(L, static_cast(&g_set_parser_key)); lua_pushlightuserdata(L, ptr); @@ -35,8 +35,9 @@ set_parser::set_parser(script_state * S, parser_imp * ptr) { } } set_parser::~set_parser() { - if (m_state) { - m_state->apply([&](lua_State * L) { + if (!m_state.expired()) { + script_state S(m_state); + S.apply([&](lua_State * L) { lua_pushlightuserdata(L, static_cast(&g_set_parser_key)); lua_pushlightuserdata(L, m_prev); lua_settable(L, LUA_REGISTRYINDEX); diff --git a/src/frontends/lean/shell.cpp b/src/frontends/lean/shell.cpp index 91813f264..8be492d96 100644 --- a/src/frontends/lean/shell.cpp +++ b/src/frontends/lean/shell.cpp @@ -101,9 +101,9 @@ bool shell::operator()() { #ifdef LEAN_USE_READLINE readline_streambuf buf; std::istream is(&buf); - parser p(m_env, m_io_state, is, "stdin", m_script_state, false, true); + parser p(m_env, m_io_state, is, "[stdin]", m_script_state, false, true); #else - parser p(m_env, m_io_state, std::cin, "stdin", m_script_state, false, true); + parser p(m_env, m_io_state, std::cin, "[stdin]", m_script_state, false, true); #endif return p(); } diff --git a/src/kernel/pos_info_provider.cpp b/src/kernel/pos_info_provider.cpp index ae2dd1886..518d3d766 100644 --- a/src/kernel/pos_info_provider.cpp +++ b/src/kernel/pos_info_provider.cpp @@ -7,13 +7,13 @@ Author: Leonardo de Moura #include "kernel/pos_info_provider.h" namespace lean { -char const * pos_info_provider::get_file_name(expr const & ) const { +char const * pos_info_provider::get_file_name() const { return "unknown"; } format pos_info_provider::pp(expr const & e) const { try { auto p = get_pos_info(e); - return format{format(get_file_name(e)), colon(), format(p.first), colon(), format(p.second), colon()}; + return format{format(get_file_name()), colon(), format(p.first), colon(), format(p.second), colon()}; } catch (exception &) { return format(); } diff --git a/src/kernel/pos_info_provider.h b/src/kernel/pos_info_provider.h index a46e5cf2d..692e5a14a 100644 --- a/src/kernel/pos_info_provider.h +++ b/src/kernel/pos_info_provider.h @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#pragma once #include #include "util/sexpr/format.h" #include "kernel/expr.h" @@ -20,7 +21,9 @@ public: Throws an exception if the given expression does not have this kind of information associated with it. */ virtual std::pair get_pos_info(expr const & e) const = 0; - virtual char const * get_file_name(expr const & e) const; + virtual char const * get_file_name() const; + virtual std::pair get_some_pos() const = 0; + unsigned get_line(expr const & e) const { return get_pos_info(e).first; } unsigned get_pos(expr const & e) const { return get_pos_info(e).second; } /** diff --git a/src/library/error_handling/CMakeLists.txt b/src/library/error_handling/CMakeLists.txt new file mode 100644 index 000000000..5d540bfe1 --- /dev/null +++ b/src/library/error_handling/CMakeLists.txt @@ -0,0 +1,2 @@ +add_library(error_handling error_handling.cpp) +target_link_libraries(error_handling ${LEAN_LIBS}) diff --git a/src/library/error_handling/error_handling.cpp b/src/library/error_handling/error_handling.cpp new file mode 100644 index 000000000..705235631 --- /dev/null +++ b/src/library/error_handling/error_handling.cpp @@ -0,0 +1,183 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include +#include "util/script_exception.h" +#include "util/name_set.h" +#include "kernel/kernel_exception.h" +#include "kernel/for_each_fn.h" +#include "library/io_state_stream.h" +#include "library/elaborator/elaborator_justification.h" +#include "library/elaborator/elaborator_exception.h" +#include "library/parser_nested_exception.h" +#include "library/unsolved_metavar_exception.h" + +namespace lean { +void display_error_pos(io_state const & ios, char const * strm_name, unsigned line, unsigned pos) { + regular(ios) << strm_name << ":" << line << ":"; + if (pos != static_cast(-1)) + regular(ios) << pos << ":"; + regular(ios) << " error:"; +} + +void display_error_pos(io_state const & ios, pos_info_provider const * p, expr const & e) { + if (p) { + auto pos = p->get_pos_info(e); + display_error_pos(ios, p->get_file_name(), pos.first, pos.second); + } else { + regular(ios) << "error:"; + } +} + +void display_error_pos(io_state const & ios, pos_info_provider const * p, optional const & e) { + if (e) { + display_error_pos(ios, p, *e); + } else if (p) { + auto pos = p->get_some_pos(); + display_error_pos(ios, p->get_file_name(), pos.first, pos.second); + } else { + regular(ios) << "error:"; + } +} + +void display_error(io_state const & ios, pos_info_provider const * p, exception const & ex); + +static void display_error(io_state const & ios, pos_info_provider const * p, kernel_exception const & ex) { + display_error_pos(ios, p, ex.get_main_expr()); + regular(ios) << " " << ex << endl; +} + +static void display_error(io_state const & ios, pos_info_provider const * p, elaborator_exception const & ex) { + formatter fmt = ios.get_formatter(); + options opts = ios.get_options(); + auto j = ex.get_justification(); + j = remove_detail(j); + regular(ios) << mk_pair(j.pp(fmt, opts, p, true), opts) << endl; +} + +struct delta_pos_info_provider : public pos_info_provider { + unsigned m_delta; + std::string m_file_name; + pos_info_provider const & m_provider; + delta_pos_info_provider(unsigned d, char const * fname, pos_info_provider const & p):m_delta(d), m_file_name(fname), m_provider(p) {} + virtual std::pair get_pos_info(expr const & e) const { + auto r = m_provider.get_pos_info(e); + return mk_pair(r.first + m_delta, r.second); + } + virtual char const * get_file_name() const { return m_file_name.c_str(); } + virtual std::pair get_some_pos() const { + auto r = m_provider.get_some_pos(); + return mk_pair(r.first + m_delta, r.second); + } +}; + +static void display_error(io_state const & ios, pos_info_provider const * p, script_exception const & ex) { + if (p) { + char const * msg = ex.get_msg(); + char const * space = msg && *msg == ' ' ? "" : " "; + switch (ex.get_source()) { + case script_exception::source::String: + display_error_pos(ios, p->get_file_name(), ex.get_line() + p->get_some_pos().first - 1, static_cast(-1)); + regular(ios) << " executing script," << space << msg << endl; + break; + case script_exception::source::File: + display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second); + regular(ios) << " executing external script (" << ex.get_file_name() << ":" << ex.get_line() << ")," << space << msg << endl; + break; + case script_exception::source::Unknown: + display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second); + regular(ios) << " executing script, exact error position is not available, " << ex.what() << endl; + break; + } + } else { + regular(ios) << ex.what() << endl; + } +} + + + +static void display_error(io_state const & ios, pos_info_provider const * p, script_nested_exception const & ex) { + switch (ex.get_source()) { + case script_exception::source::String: + if (p) { + display_error_pos(ios, p->get_file_name(), ex.get_line() + p->get_some_pos().first - 1, static_cast(-1)); + regular(ios) << " executing script" << endl; + } + display_error(ios, nullptr, ex.get_exception()); + break; + case script_exception::source::File: + if (p) { + display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second); + regular(ios) << " executing external script (" << ex.get_file_name() << ":" << ex.get_line() << ")" << endl; + } else { + display_error_pos(ios, ex.get_file_name(), ex.get_line(), -1); + regular(ios) << " executing script" << endl; + } + display_error(ios, nullptr, ex.get_exception()); + break; + case script_exception::source::Unknown: + display_error(ios, nullptr, ex.get_exception()); + break; + } +} + +static void display_error(io_state const & ios, pos_info_provider const *, parser_nested_exception const & ex) { + display_error(ios, &(ex.get_provider()), ex.get_exception()); +} + +static void display_error(io_state const & ios, pos_info_provider const *, parser_exception const & ex) { + regular(ios) << ex.what() << endl; +} + +static void display_error(io_state const & ios, pos_info_provider const * p, unsolved_metavar_exception const & ex) { + display_error_pos(ios, p, ex.get_expr()); + formatter fmt = ios.get_formatter(); + options opts = ios.get_options(); + unsigned indent = get_pp_indent(opts); + format r = nest(indent, compose(line(), fmt(ex.get_expr(), opts))); + regular(ios) << " " << ex.what() << mk_pair(r, opts) << endl; + if (p) { + name_set already_displayed; + for_each(ex.get_expr(), [&](expr const & e, unsigned) -> bool { + if (is_metavar(e)) { + name const & m = metavar_name(e); + if (already_displayed.find(m) == already_displayed.end()) { + already_displayed.insert(m); + for (unsigned i = 0; i < indent; i++) regular(ios) << " "; + display_error_pos(ios, p, e); + regular(ios) << " unsolved metavar " << m << endl; + } + } + return true; + }); + } +} + +void display_error(io_state const & ios, pos_info_provider const * p, exception const & ex) { + if (auto k_ex = dynamic_cast(&ex)) { + display_error(ios, p, *k_ex); + } else if (auto e_ex = dynamic_cast(&ex)) { + display_error(ios, p, *e_ex); + } else if (auto m_ex = dynamic_cast(&ex)) { + display_error(ios, p, *m_ex); + } else if (auto ls_ex = dynamic_cast(&ex)) { + display_error(ios, p, *ls_ex); + } else if (auto s_ex = dynamic_cast(&ex)) { + display_error(ios, p, *s_ex); + } else if (auto n_ex = dynamic_cast(&ex)) { + display_error(ios, p, *n_ex); + } else if (auto n_ex = dynamic_cast(&ex)) { + display_error(ios, p, *n_ex); + } else if (p) { + display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second); + regular(ios) << " " << ex.what() << endl; + } else { + regular(ios) << "error: " << ex.what() << endl; + } +} +} + diff --git a/src/library/error_handling/error_handling.h b/src/library/error_handling/error_handling.h new file mode 100644 index 000000000..5e94427a3 --- /dev/null +++ b/src/library/error_handling/error_handling.h @@ -0,0 +1,18 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/exception.h" +#include "kernel/pos_info_provider.h" +#include "kernel/io_state.h" + +namespace lean { +/** + \brief Display exception in the regular stream of \c ios, using the configuration options and formatter from \c ios. + Exceptions that contain expressions use the given \c pos_info_provider (if available) to retrieve line number information. +*/ +void display_error(io_state const & ios, pos_info_provider const * p, exception const & ex); +} diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 96440e7fc..31e162caa 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1205,11 +1205,15 @@ static const struct luaL_Reg environment_m[] = { static char g_set_environment_key; +void set_global_environment(lua_State * L, environment const & env) { + lua_pushlightuserdata(L, static_cast(&g_set_environment_key)); + push_environment(L, env); + lua_settable(L, LUA_REGISTRYINDEX); +} + set_environment::set_environment(lua_State * L, environment const & env) { m_state = L; - lua_pushlightuserdata(m_state, static_cast(&g_set_environment_key)); - push_environment(m_state, env); - lua_settable(m_state, LUA_REGISTRYINDEX); + set_global_environment(L, env); } set_environment::~set_environment() { @@ -1832,6 +1836,13 @@ void open_io_state(lua_State * L) { static char g_set_state_key; +void set_global_io_state(lua_State * L, io_state & ios) { + lua_pushlightuserdata(L, static_cast(&g_set_state_key)); + lua_pushlightuserdata(L, &ios); + lua_settable(L, LUA_REGISTRYINDEX); + set_global_options(L, ios.get_options()); +} + set_io_state::set_io_state(lua_State * L, io_state & st) { m_state = L; m_prev = get_io_state(L); diff --git a/src/library/kernel_bindings.h b/src/library/kernel_bindings.h index b99a68453..3b25521c3 100644 --- a/src/library/kernel_bindings.h +++ b/src/library/kernel_bindings.h @@ -44,8 +44,11 @@ formatter get_global_formatter(lua_State * L); Otherwise, we update the registry of \c L. */ void set_global_formatter(lua_State * L, formatter const & fmt); + +/** \brief Set the Lua registry of a Lua state with an environment object. */ +void set_global_environment(lua_State * L, environment const & env); /** - \brief Auxiliary class for setting the Lua registry of a Lua state + \brief Auxiliary class for temporarily setting the Lua registry of a Lua state with an environment object. */ class set_environment { @@ -74,6 +77,9 @@ public: rw_shared_environment(lua_State * L, int idx); rw_shared_environment(lua_State * L); }; + +/** \brief Set the Lua registry of a Lua state with an io_state object. */ +void set_global_io_state(lua_State * L, io_state & ios); /** \brief Auxiliary class for temporarily setting the Lua registry of a Lua state with a Lean io_state object. diff --git a/src/library/parser_nested_exception.h b/src/library/parser_nested_exception.h new file mode 100644 index 000000000..2c99186a0 --- /dev/null +++ b/src/library/parser_nested_exception.h @@ -0,0 +1,25 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "util/exception.h" +#include "kernel/pos_info_provider.h" + +namespace lean { +/** \brief Lean exception occurred when parsing file. */ +class parser_nested_exception : public exception { + std::shared_ptr m_exception; + std::shared_ptr m_provider; +public: + parser_nested_exception(std::shared_ptr const & ex, std::shared_ptr const & pr):exception("parser exception"), m_exception(ex), m_provider(pr) {} + virtual ~parser_nested_exception() {} + virtual exception * clone() const { return new parser_nested_exception(m_exception, m_provider); } + virtual void rethrow() const { throw *this; } + virtual char const * what() const noexcept { return m_exception->what(); } + exception const & get_exception() const { return *(m_exception.get()); } + pos_info_provider const & get_provider() const { return *(m_provider.get()); } +}; +} diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index d416f1656..65a97b0be 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -23,6 +23,7 @@ Author: Leonardo de Moura #include "library/printer.h" #include "library/kernel_bindings.h" #include "library/io_state_stream.h" +#include "library/error_handling/error_handling.h" #include "frontends/lean/parser.h" #include "frontends/lean/shell.h" #include "frontends/lean/frontend.h" @@ -108,67 +109,77 @@ static struct option g_long_options[] = { }; int main(int argc, char ** argv) { - try { - lean::save_stack_info(); - lean::register_modules(); - bool no_kernel = false; - bool export_objects = false; - bool trust_imported = false; - bool quiet = false; - std::string output; - input_kind default_k = input_kind::Lean; // default - while (true) { - int c = getopt_long(argc, argv, "qtnlupgvhc:012s:012o:", g_long_options, NULL); - if (c == -1) - break; // end of command line - switch (c) { - case 'v': - display_header(std::cout); - return 0; - case 'g': - std::cout << g_githash << "\n"; - return 0; - case 'h': - display_help(std::cout); - return 0; - case 'l': - default_k = input_kind::Lean; - break; - case 'u': - default_k = input_kind::Lua; - break; - case 'b': - default_k = input_kind::OLean; - break; - case 'c': - script_state::set_check_interrupt_freq(atoi(optarg)); - break; - case 'p': - std::cout << lean::get_lean_path() << "\n"; - return 0; - case 's': - lean::set_thread_stack_size(atoi(optarg)*1024); - break; - case 'n': - no_kernel = true; - break; - case 'o': - output = optarg; - export_objects = true; - break; - case 't': - trust_imported = true; - lean::set_default_trust_imported_for_lua(true); - break; - case 'q': - quiet = true; - break; - default: - std::cerr << "Unknown command line option\n"; - display_help(std::cerr); - return 1; - } + lean::save_stack_info(); + lean::register_modules(); + bool no_kernel = false; + bool export_objects = false; + bool trust_imported = false; + bool quiet = false; + std::string output; + input_kind default_k = input_kind::Lean; // default + while (true) { + int c = getopt_long(argc, argv, "qtnlupgvhc:012s:012o:", g_long_options, NULL); + if (c == -1) + break; // end of command line + switch (c) { + case 'v': + display_header(std::cout); + return 0; + case 'g': + std::cout << g_githash << "\n"; + return 0; + case 'h': + display_help(std::cout); + return 0; + case 'l': + default_k = input_kind::Lean; + break; + case 'u': + default_k = input_kind::Lua; + break; + case 'b': + default_k = input_kind::OLean; + break; + case 'c': + script_state::set_check_interrupt_freq(atoi(optarg)); + break; + case 'p': + std::cout << lean::get_lean_path() << "\n"; + return 0; + case 's': + lean::set_thread_stack_size(atoi(optarg)*1024); + break; + case 'n': + no_kernel = true; + break; + case 'o': + output = optarg; + export_objects = true; + break; + case 't': + trust_imported = true; + lean::set_default_trust_imported_for_lua(true); + break; + case 'q': + quiet = true; + break; + default: + std::cerr << "Unknown command line option\n"; + display_help(std::cerr); + return 1; } + } + environment env; + env->set_trusted_imported(trust_imported); + io_state ios = init_frontend(env, no_kernel); + if (quiet) + ios.set_option("verbose", false); + script_state S; + S.apply([&](lua_State * L) { + set_global_environment(L, env); + set_global_io_state(L, ios); + }); + try { if (optind >= argc) { display_header(std::cout); signal(SIGINT, on_ctrl_c); @@ -178,12 +189,6 @@ int main(int argc, char ** argv) { #else std::cout << "Type Ctrl-D or 'Exit.' to exit or 'Help.' for help."<< std::endl; #endif - environment env; - env->set_trusted_imported(trust_imported); - io_state ios = init_frontend(env, no_kernel); - if (quiet) - ios.set_option("verbose", false); - script_state S; shell sh(env, &S); int status = sh() ? 0 : 1; if (export_objects) @@ -191,17 +196,10 @@ int main(int argc, char ** argv) { return status; } else { lean_assert(default_k == input_kind::Lua); - script_state S; S.import("repl"); return 0; } } else { - environment env; - env->set_trusted_imported(trust_imported); - io_state ios = init_frontend(env, no_kernel); - if (quiet) - ios.set_option("verbose", false); - script_state S; bool ok = true; for (int i = optind; i < argc; i++) { char const * ext = get_file_extension(argv[i]); @@ -227,15 +225,9 @@ int main(int argc, char ** argv) { } } else if (k == input_kind::Lua) { try { - S.apply([&](lua_State * L) { - lean::set_io_state set1(L, ios); - lean::set_environment set2(L, env); - S.exec_unprotected([&]() { - S.dofile(argv[i]); - }); - }); + S.dofile(argv[i]); } catch (lean::exception & ex) { - std::cerr << ex.what() << std::endl; + ::lean::display_error(ios, nullptr, ex); ok = false; } } else { @@ -246,12 +238,8 @@ int main(int argc, char ** argv) { env->export_objects(output); return ok ? 0 : 1; } - } catch (lean::kernel_exception & ex) { - std::cerr << "Error: " << ex.pp(lean::mk_simple_formatter(), lean::options()) << "\n"; - } catch (lean::parser_exception & ex) { - std::cerr << ex.what() << "\n"; } catch (lean::exception & ex) { - std::cerr << "Error: " << ex.what() << "\n"; + ::lean::display_error(ios, nullptr, ex); } return 1; } diff --git a/src/util/exception.h b/src/util/exception.h index ce9838c61..7e8096598 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "util/lua.h" #include #include +#include namespace lean { class sstream; @@ -39,9 +40,12 @@ public: virtual char const * what() const noexcept; unsigned get_line() const { return m_line; } unsigned get_pos() const { return m_pos; } + std::string const & get_file_name() const { return m_fname; } virtual exception * clone() const { return new parser_exception(m_msg, m_fname.c_str(), m_line, m_pos); } virtual void rethrow() const { throw *this; } + parser_exception update_line(unsigned line_delta) const { return parser_exception(m_msg, m_fname.c_str(), m_line + line_delta, m_pos); } }; + /** \brief Exception used to sign that a computation was interrupted */ class interrupted : public exception { public: diff --git a/src/util/lua.cpp b/src/util/lua.cpp index 267d18099..9968e6d55 100644 --- a/src/util/lua.cpp +++ b/src/util/lua.cpp @@ -91,10 +91,11 @@ static void exec(lua_State * L) { void check_result(lua_State * L, int result) { if (result) { - if (is_exception(L, -1)) + if (is_exception(L, -1)) { to_exception(L, -1).rethrow(); - else + } else { throw script_exception(lua_tostring(L, -1)); + } } } @@ -137,10 +138,16 @@ bool resume(lua_State * L, int nargs) { int safe_function_wrapper(lua_State * L, lua_CFunction f) { try { return f(L); - } catch (script_exception & e) { - lua_pushstring(L, e.what()); } catch (exception & e) { - push_exception(L, e); + lua_Debug ar; + lua_getstack(L, 1, &ar); + lua_getinfo(L, "Sl", &ar); + if (ar.source && *(ar.source) == '@') + push_exception(L, script_nested_exception(true, ar.source+1, ar.currentline, std::shared_ptr(e.clone()))); + else if (ar.source) + push_exception(L, script_nested_exception(false, ar.source, ar.currentline, std::shared_ptr(e.clone()))); + else + push_exception(L, e); } catch (std::bad_alloc &) { lua_pushstring(L, "out of memory"); } catch (std::exception & e) { diff --git a/src/util/script_exception.cpp b/src/util/script_exception.cpp index c9491d8e9..58694aaad 100644 --- a/src/util/script_exception.cpp +++ b/src/util/script_exception.cpp @@ -55,7 +55,7 @@ script_exception::script_exception(char const * lua_error) { script_exception::~script_exception() { } -char const * script_exception::get_filename() const { +char const * script_exception::get_file_name() const { lean_assert(get_source() == source::File); return m_file.c_str(); } @@ -72,12 +72,30 @@ char const * script_exception::get_msg() const noexcept { char const * script_exception::what() const noexcept { static thread_local std::string buffer; std::ostringstream strm; + char const * msg = get_msg(); + char const * space = msg && *msg == ' ' ? "" : " "; switch (get_source()) { - case source::String: strm << "[string]:" << get_line() << ":" << get_msg() << "\n"; break; - case source::File: strm << get_filename() << ":" << get_line() << ":" << get_msg() << "\n"; break; + case source::String: strm << "[string]:" << get_line() << ":" << space << get_msg(); break; + case source::File: strm << get_file_name() << ":" << get_line() << ":" << space << get_msg(); break; case source::Unknown: return get_msg(); } buffer = strm.str(); return buffer.c_str(); } + +script_nested_exception::script_nested_exception(source s, std::string f, unsigned l, std::shared_ptr const & ex): + script_exception(s, f, l, "Lean exception"), + m_exception(ex) { + lean_assert(ex); +} + +script_nested_exception::~script_nested_exception() {} + +char const * script_nested_exception::what() const noexcept { + static thread_local std::string buffer; + std::ostringstream strm; + strm << script_exception::what() << "\n" << get_exception().what(); + buffer = strm.str(); + return buffer.c_str(); +} } diff --git a/src/util/script_exception.h b/src/util/script_exception.h index 073fcf7ac..c27db5cda 100644 --- a/src/util/script_exception.h +++ b/src/util/script_exception.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include +#include #include "util/exception.h" namespace lean { @@ -15,21 +16,36 @@ namespace lean { class script_exception : public exception { public: enum class source { String, File, Unknown }; -private: +protected: source m_source; std::string m_file; // if source == File, then this field contains the filename that triggered the error. unsigned m_line; // line number - script_exception(source s, std::string f, unsigned l):m_source(s), m_file(f), m_line(l) {} + script_exception(source s, std::string f, unsigned l, std::string const & msg):exception(msg), m_source(s), m_file(f), m_line(l) {} public: script_exception(char const * lua_error); virtual ~script_exception(); virtual char const * what() const noexcept; virtual source get_source() const { return m_source; } - virtual char const * get_filename() const; + virtual char const * get_file_name() const; virtual unsigned get_line() const; /** \brief Return error message without position information */ virtual char const * get_msg() const noexcept; - virtual exception * clone() const { return new script_exception(m_source, m_file, m_line); } + virtual exception * clone() const { return new script_exception(m_source, m_file, m_line, m_msg); } virtual void rethrow() const { throw *this; } }; + +/** + \brief Lean exception occurred inside of a script +*/ +class script_nested_exception : public script_exception { + std::shared_ptr m_exception; + script_nested_exception(source s, std::string f, unsigned l, std::shared_ptr const & ex); +public: + script_nested_exception(bool file, std::string f, unsigned l, std::shared_ptr const & ex):script_nested_exception(file ? source::File : source::String, f, l, ex) {} + virtual ~script_nested_exception(); + virtual char const * what() const noexcept; + virtual exception * clone() const { return new script_nested_exception(m_source, m_file, m_line, m_exception); } + virtual void rethrow() const { throw *this; } + exception const & get_exception() const { return *(m_exception.get()); } +}; } diff --git a/tests/lean/alias3.lean.expected.out b/tests/lean/alias3.lean.expected.out index 2b11bdf26..3f7fb648c 100644 --- a/tests/lean/alias3.lean.expected.out +++ b/tests/lean/alias3.lean.expected.out @@ -1,3 +1,3 @@ Set: pp::colors Set: pp::unicode -alias3.lean:2:13: error: alias 'A' was already defined +alias3.lean:2:0: error: alias 'A' was already defined diff --git a/tests/lean/coercion1.lean.expected.out b/tests/lean/coercion1.lean.expected.out index e3136d8cc..a46d25c58 100644 --- a/tests/lean/coercion1.lean.expected.out +++ b/tests/lean/coercion1.lean.expected.out @@ -7,12 +7,12 @@ variable f : T → R coercion f Assumed: g -coercion1.lean:8:0: error: invalid coercion declaration, frontend already has a coercion for the given types +coercion1.lean:7:0: error: invalid coercion declaration, frontend already has a coercion for the given types Assumed: h -coercion1.lean:10:0: error: invalid coercion declaration, a coercion must have an arrow type (i.e., a non-dependent functional type) +coercion1.lean:9:0: error: invalid coercion declaration, a coercion must have an arrow type (i.e., a non-dependent functional type) Defined: T2 Defined: R2 Assumed: f2 -coercion1.lean:14:0: error: invalid coercion declaration, frontend already has a coercion for the given types +coercion1.lean:13:0: error: invalid coercion declaration, frontend already has a coercion for the given types Assumed: id -coercion1.lean:16:0: error: invalid coercion declaration, 'from' and 'to' types are the same +coercion1.lean:15:0: error: invalid coercion declaration, 'from' and 'to' types are the same diff --git a/tests/lean/env_errors.lean.expected.out b/tests/lean/env_errors.lean.expected.out index d90e37fd7..6e26238f6 100644 --- a/tests/lean/env_errors.lean.expected.out +++ b/tests/lean/env_errors.lean.expected.out @@ -3,10 +3,14 @@ Assumed: x env_errors.lean:3:0: error: set_opaque failed, 'x' is not a definition before import -env_errors.lean:11:0: error: file 'tstblafoo.lean' not found in the LEAN_PATH +env_errors.lean:8: error: executing script +error: file 'tstblafoo.lean' not found in the LEAN_PATH before load1 -env_errors.lean:17:0: error: failed to open file 'tstblafoo.lean' +env_errors.lean:14: error: executing script +error: failed to open file 'tstblafoo.lean' before load2 -env_errors.lean:23:0: error: corrupted binary file +env_errors.lean:20: error: executing script +error: corrupted binary file before load3 -env_errors.lean:28:0: error: file 'fake2.olean' does not seem to be a valid object Lean file +env_errors.lean:26: error: executing script +error: file 'fake2.olean' does not seem to be a valid object Lean file diff --git a/tests/lean/explicit.lean.expected.out b/tests/lean/explicit.lean.expected.out index babbba8ae..93906b8db 100644 --- a/tests/lean/explicit.lean.expected.out +++ b/tests/lean/explicit.lean.expected.out @@ -9,4 +9,4 @@ module::@g : ∀ (A : Type), A → A → A h::1::explicit : ∀ (A B : Type), A → B → A Assumed: @h Assumed: h -explicit.lean:9:37: error: failed to mark implicit arguments for 'h', the frontend already has an object named '@h' +explicit.lean:9:0: error: failed to mark implicit arguments for 'h', the frontend already has an object named '@h' diff --git a/tests/lean/interactive/t1.lean.expected.out b/tests/lean/interactive/t1.lean.expected.out index edae1d5a9..b79b83c73 100644 --- a/tests/lean/interactive/t1.lean.expected.out +++ b/tests/lean/interactive/t1.lean.expected.out @@ -2,18 +2,18 @@ Set: pp::unicode Proof state: a : Bool, b : Bool, H : a, H::1 : b ⊢ a ∧ b -## stdin:5:0: error: invalid 'done' command, proof cannot be produced from this state +## [stdin]:5:0: error: invalid 'done' command, proof cannot be produced from this state Proof state: a : Bool, b : Bool, H : a, H::1 : b ⊢ a ∧ b -## stdin:6:0: error: invalid 'done' command, proof cannot be produced from this state +## [stdin]:6:0: error: invalid 'done' command, proof cannot be produced from this state Proof state: a : Bool, b : Bool, H : a, H::1 : b ⊢ a ∧ b -## stdin:7:0: error: unknown tactic 'imp_tac2' -## stdin:8:0: error: unknown tactic 'foo' +## [stdin]:7:0: error: unknown tactic 'imp_tac2' +## [stdin]:8:0: error: unknown tactic 'foo' ## Proof state: a : Bool, b : Bool, H : a, H::1 : b ⊢ a a : Bool, b : Bool, H : a, H::1 : b ⊢ b -## stdin:10:0: error: failed to backtrack +## [stdin]:10:0: error: failed to backtrack Proof state: a : Bool, b : Bool, H : a, H::1 : b ⊢ a a : Bool, b : Bool, H : a, H::1 : b ⊢ b diff --git a/tests/lean/interactive/t10.lean.expected.out b/tests/lean/interactive/t10.lean.expected.out index de8a20d17..9a8656017 100644 --- a/tests/lean/interactive/t10.lean.expected.out +++ b/tests/lean/interactive/t10.lean.expected.out @@ -6,15 +6,15 @@ A : Bool, B : Bool, H : A ∧ B ⊢ A no goals ## Proof state: A : Bool, B : Bool, H : A ∧ B, H1 : A ⊢ B -## stdin:15:3: error: unknown tactic 'simple2_tac' -## stdin:15:16: error: invalid 'done' command, proof cannot be produced from this state +## [stdin]:15:3: error: unknown tactic 'simple2_tac' +## [stdin]:15:16: error: invalid 'done' command, proof cannot be produced from this state Proof state: A : Bool, B : Bool, H : A ∧ B, H1 : A ⊢ B ## Proof state: no goals ## Proof state: A : Bool, B : Bool, H : A ∧ B, H1 : A, H2 : B ⊢ B ∧ A -## stdin:18:0: error: failed to prove theorem, proof has been aborted +## [stdin]:18:0: error: 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 06c3a125a..d06238b1f 100644 --- a/tests/lean/interactive/t2.lean.expected.out +++ b/tests/lean/interactive/t2.lean.expected.out @@ -2,8 +2,8 @@ Set: pp::unicode Proof state: a : Bool, b : Bool, H : a, H::1 : b ⊢ a ∧ b -## stdin:5:0: error: unknown tactic 'foo' -## stdin:6:5: error: failed to prove theorem, proof has been aborted +## [stdin]:5:0: error: unknown tactic 'foo' +## [stdin]:6:5: error: failed to prove theorem, proof has been aborted Proof state: a : Bool, b : Bool, H : a, H::1 : b ⊢ a ∧ b # Assumed: a diff --git a/tests/lean/interactive/t3.lean.expected.out b/tests/lean/interactive/t3.lean.expected.out index 628f44ff9..76d359055 100644 --- a/tests/lean/interactive/t3.lean.expected.out +++ b/tests/lean/interactive/t3.lean.expected.out @@ -6,7 +6,7 @@ a : Bool, b : Bool, H : b ⊢ a ∨ b a : Bool, b : Bool, H : b ⊢ a ## Proof state: a : Bool, b : Bool, H : b ⊢ b -## stdin:9:0: error: failed to backtrack +## [stdin]:9:0: error: failed to backtrack Proof state: a : Bool, b : Bool, H : b ⊢ b ## Proof state: diff --git a/tests/lean/interactive/t4.lean.expected.out b/tests/lean/interactive/t4.lean.expected.out index b3dd55724..0ba88bbf1 100644 --- a/tests/lean/interactive/t4.lean.expected.out +++ b/tests/lean/interactive/t4.lean.expected.out @@ -1,5 +1,5 @@ # Set: pp::colors Set: pp::unicode -stdin:4:8: error: invalid definition, identifier expected +[stdin]:4:8: error: invalid definition, identifier expected # done # \ No newline at end of file diff --git a/tests/lean/lua15.lean.expected.out b/tests/lean/lua15.lean.expected.out index a7de97e3f..1e167ea76 100644 --- a/tests/lean/lua15.lean.expected.out +++ b/tests/lean/lua15.lean.expected.out @@ -4,21 +4,23 @@ Assumed: i Assumed: j Assumed: p +[string]:5: Lean exception elaborator exception +lua15.lean:9: error: executing script Failed to solve ⊢ (?M::0 ≈ Nat::add) ⊕ (?M::0 ≈ Int::add) - Overloading at + [string]:1:3: Overloading at (Int::add | Nat::add) i p Failed to solve ⊢ ℤ ≺ ℕ - Type of argument 1 must be convertible to the expected type in the application of + [string]:1:3: Type of argument 1 must be convertible to the expected type in the application of Nat::add with arguments: i p Failed to solve ⊢ Bool ≺ ℤ - Type of argument 2 must be convertible to the expected type in the application of + [string]:1:3: Type of argument 2 must be convertible to the expected type in the application of Int::add with arguments: i diff --git a/tests/lean/lua15b.lean b/tests/lean/lua15b.lean new file mode 100644 index 000000000..2b766ae8a --- /dev/null +++ b/tests/lean/lua15b.lean @@ -0,0 +1,13 @@ +import Int. +variables i j : Int +variable p : Bool + +(* + local env = get_environment() + + parse_lean_cmds([[ + print "hello" + eval i + j + check i + p +]]) +*) diff --git a/tests/lean/lua15b.lean.expected.out b/tests/lean/lua15b.lean.expected.out new file mode 100644 index 000000000..7634b914c --- /dev/null +++ b/tests/lean/lua15b.lean.expected.out @@ -0,0 +1,27 @@ + Set: pp::colors + Set: pp::unicode + Imported 'Int' + Assumed: i + Assumed: j + Assumed: p +hello +i + j +lua15b.lean:8: error: executing script +Failed to solve + ⊢ (?M::0 ≈ Nat::add) ⊕ (?M::0 ≈ Int::add) + [string]:3:12: Overloading at + (Int::add | Nat::add) i p + Failed to solve + ⊢ ℤ ≺ ℕ + [string]:3:12: Type of argument 1 must be convertible to the expected type in the application of + Nat::add + with arguments: + i + p + Failed to solve + ⊢ Bool ≺ ℤ + [string]:3:12: Type of argument 2 must be convertible to the expected type in the application of + Int::add + with arguments: + i + p diff --git a/tests/lean/parser1.lean b/tests/lean/parser1.lean new file mode 100644 index 000000000..ed702a892 --- /dev/null +++ b/tests/lean/parser1.lean @@ -0,0 +1,20 @@ + + + +(* + +foo(10) + +*) + +print "checkpoint" + +(* + +parse_lean_cmds("(" .. "*" .. [[ + + foo(20) + +]] .. "*" .. ")") + +*) \ No newline at end of file diff --git a/tests/lean/parser1.lean.expected.out b/tests/lean/parser1.lean.expected.out new file mode 100644 index 000000000..729b684f9 --- /dev/null +++ b/tests/lean/parser1.lean.expected.out @@ -0,0 +1,6 @@ + Set: pp::colors + Set: pp::unicode +parser1.lean:6: error: executing script, attempt to call global 'foo' (a nil value) +checkpoint +parser1.lean:14: error: executing script +[string]:2: error: executing script, attempt to call global 'foo' (a nil value) diff --git a/tests/lua/threads/sleep1.lua b/tests/lua/threads/sleep1.lua index 0ffa964c2..4803896aa 100644 --- a/tests/lua/threads/sleep1.lua +++ b/tests/lua/threads/sleep1.lua @@ -8,4 +8,4 @@ T:interrupt() local ok, msg = pcall(function() T:wait() end) assert(not ok) assert(is_exception(msg)) -assert(msg:what() == "interrupted") +print(msg:what():find("interrupted")) diff --git a/tests/lua/threads/th5.lua b/tests/lua/threads/th5.lua index e87ae41fd..43d127060 100644 --- a/tests/lua/threads/th5.lua +++ b/tests/lua/threads/th5.lua @@ -31,6 +31,8 @@ assert(not pcall(function() S:eval([[ x = ]]) end)) local T2 = thread(S, [[ local x = ...; error("failed") ]], 10) local ok, msg = pcall(function() T2:wait() end) assert(not ok) -assert(string.sub(msg, -7) == "failed\n") +assert(is_exception(msg)) +print(msg:what()) +assert(msg:what():find("failed")) local T3 = thread(S, [[ local x = ...; return x + 10, x - 10 ]], 10) T3 = nil