From f7c7dd4ed4846c3d1a9afdd1e448c07d02811c69 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Jan 2014 11:01:27 -0800 Subject: [PATCH] feat(frontends/lean): include filename in error messages, use GNU error message style Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 24 ++++++++++++-------- src/frontends/lean/parser.h | 8 +++---- src/frontends/lean/parser_error.cpp | 11 +++++---- src/frontends/lean/parser_imp.cpp | 7 +++--- src/frontends/lean/parser_imp.h | 4 +++- src/frontends/lean/register_module.cpp | 4 ++-- src/frontends/lean/scanner.cpp | 5 ++-- src/frontends/lean/scanner.h | 3 ++- src/frontends/lean/shell.cpp | 4 ++-- src/shell/CMakeLists.txt | 8 +++---- src/shell/lean.cpp | 11 ++++----- src/tests/frontends/lean/parser.cpp | 4 ++-- src/tests/frontends/lean/scanner.cpp | 6 ++--- src/tests/util/exception.cpp | 8 +++---- src/util/exception.cpp | 11 +++++---- src/util/exception.h | 13 ++++++----- tests/lean/alias3.lean.expected.out | 2 +- tests/lean/cast1.lean.expected.out | 2 +- tests/lean/coercion1.lean.expected.out | 8 +++---- tests/lean/elab1.lean.expected.out | 4 ++-- tests/lean/env_errors.lean.expected.out | 10 ++++---- tests/lean/errmsg1.lean.expected.out | 6 ++--- tests/lean/ex2.lean.expected.out | 8 +++---- tests/lean/explicit.lean.expected.out | 2 +- tests/lean/implicit2.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/kernel_ex1.lean.expected.out | 6 ++--- tests/lean/let4.lean.expected.out | 6 ++--- tests/lean/lua2.lean.expected.out | 2 +- tests/lean/nbug1.lean.expected.out | 2 +- tests/lean/ns1.lean.expected.out | 2 +- tests/lean/push.lean.expected.out | 6 ++--- tests/lean/scan_error1.lean.expected.out | 2 +- tests/lean/scan_error2.lean.expected.out | 2 +- tests/lean/scan_error3.lean.expected.out | 2 +- tests/lean/scan_test2.lean.expected.out | 2 +- tests/lean/tst9.lean.expected.out | 2 +- tests/lean/ty1.lean.expected.out | 2 +- tests/lean/univ.lean.expected.out | 4 ++-- tests/lean/vars1.lean.expected.out | 2 +- 44 files changed, 127 insertions(+), 114 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 893779f60..375d260b9 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -4,19 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/sstream.h" #include "library/io_state_stream.h" #include "frontends/lean/parser.h" #include "frontends/lean/pp.h" #include "frontends/lean/parser_imp.h" namespace lean { -parser::parser(environment const & env, io_state const & ios, std::istream & in, script_state * S, bool use_exceptions, bool interactive) { +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, S, use_exceptions, interactive)); -} - -parser::parser(environment const & env, std::istream & in, script_state * S, bool use_exceptions, bool interactive): - parser(env, io_state(mk_pp_formatter(m_ptr->m_env)), in, S, use_exceptions, interactive) { + m_ptr.reset(new parser_imp(env, ios, in, strm_name, S, use_exceptions, interactive)); } parser::~parser() { @@ -34,15 +31,22 @@ io_state parser::get_io_state() const { return m_ptr->m_io_state; } -bool parse_commands(environment const & env, io_state & ios, std::istream & in, script_state * S, bool use_exceptions, bool interactive) { - parser p(env, ios, in, S, use_exceptions, interactive); +bool parse_commands(environment const & env, io_state & ios, std::istream & in, char const * strm_name, script_state * S, bool use_exceptions, bool interactive) { + parser p(env, ios, in, strm_name, S, use_exceptions, interactive); bool r = p(); ios = p.get_io_state(); return r; } -expr parse_expr(environment const & env, io_state & ios, std::istream & in, script_state * S, bool use_exceptions) { - parser p(env, ios, in, S, use_exceptions); +bool parse_commands(environment const & env, io_state & ios, char const * fname, script_state * S, bool use_exceptions, bool interactive) { + std::ifstream in(fname); + if (in.bad() || in.fail()) + throw exception(sstream() << "failed to open file '" << fname << "'"); + return parse_commands(env, ios, in, fname, S, use_exceptions, interactive); +} + +expr parse_expr(environment const & env, io_state & ios, std::istream & in, char const * strm_name, script_state * S, bool use_exceptions) { + parser p(env, ios, in, strm_name, S, use_exceptions); expr r = p.parse_expr(); ios = p.get_io_state(); return r; diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 0f59ec278..11bbac355 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -18,8 +18,7 @@ class parser { private: std::unique_ptr m_ptr; public: - parser(environment const & env, io_state const & st, std::istream & in, script_state * S, bool use_exceptions = true, bool interactive = false); - parser(environment const & env, std::istream & in, script_state * S, bool use_exceptions = true, bool interactive = false); + 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(); /** \brief Parse a sequence of commands */ @@ -31,7 +30,8 @@ public: io_state get_io_state() const; }; -bool parse_commands(environment const & env, io_state & st, std::istream & in, script_state * S = nullptr, bool use_exceptions = true, bool interactive = false); -expr parse_expr(environment const & env, io_state & st, std::istream & in, script_state * S = nullptr, bool use_exceptions = true); +bool parse_commands(environment const & env, io_state & st, std::istream & in, char const * strm_name, script_state * S = nullptr, bool use_exceptions = true, bool interactive = false); +bool parse_commands(environment const & env, io_state & st, char const * fname, script_state * S = nullptr, bool use_exceptions = true, bool interactive = false); +expr parse_expr(environment const & env, io_state & st, std::istream & in, char const * strm_name, script_state * S = nullptr, bool use_exceptions = true); void open_macros(lua_State * L); } diff --git a/src/frontends/lean/parser_error.cpp b/src/frontends/lean/parser_error.cpp index a848a85b6..e18578f6d 100644 --- a/src/frontends/lean/parser_error.cpp +++ b/src/frontends/lean/parser_error.cpp @@ -12,10 +12,10 @@ Author: Leonardo de Moura namespace lean { void parser_imp::display_error_pos(unsigned line, unsigned pos) { - regular(m_io_state) << "Error (line: " << line; + regular(m_io_state) << m_strm_name << ":" << line; if (pos != static_cast(-1)) - regular(m_io_state) << ", pos: " << pos; - regular(m_io_state) << ")"; + regular(m_io_state) << ":" << pos; + regular(m_io_state) << " error:"; } void parser_imp::display_error_pos(pos_info const & p) { display_error_pos(p.first, p.second); } @@ -116,9 +116,10 @@ void parser_imp::protected_call(std::function && f, std::function(c)]; } -scanner::scanner(std::istream& stream): +scanner::scanner(std::istream& stream, char const * strm_name): m_spos(0), m_curr(0), m_line(1), m_pos(0), m_stream(stream), + m_stream_name(strm_name), m_script_line(1), m_script_pos(0) { next(); @@ -111,7 +112,7 @@ void scanner::add_command_keyword(name const & n) { } void scanner::throw_exception(char const * msg) { - throw parser_exception(msg, m_line, m_spos); + throw parser_exception(msg, m_stream_name.c_str(), m_line, m_spos); } void scanner::next() { diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h index 9a8ffbf84..404d7a6a1 100644 --- a/src/frontends/lean/scanner.h +++ b/src/frontends/lean/scanner.h @@ -30,6 +30,7 @@ protected: int m_line; // line int m_pos; // start position of the token std::istream & m_stream; + std::string m_stream_name; int m_script_line; // hack for saving beginning of script block line and pos int m_script_pos; @@ -57,7 +58,7 @@ protected: bool is_command(name const & n) const; public: - scanner(std::istream& stream); + scanner(std::istream& stream, char const * strm_name); ~scanner(); /** \brief Register a new command keyword. */ diff --git a/src/frontends/lean/shell.cpp b/src/frontends/lean/shell.cpp index af15ec566..91813f264 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, 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, 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/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 815abad53..cfabe3c89 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -36,7 +36,7 @@ FOREACH(T ${LEANTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leantest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" - COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T}) + COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) ENDFOREACH(T) # LEAN PP TESTS @@ -55,7 +55,7 @@ FOREACH(T ${LEANINTERACTIVETESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leaninteractivetest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive" - COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T}) + COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) ENDFOREACH(T) # LEAN SLOW TESTS @@ -64,7 +64,7 @@ FOREACH(T ${LEANSLOWTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanslowtest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/slow" - COMMAND "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T}) + COMMAND "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) ENDFOREACH(T) # LEAN LUA TESTS @@ -73,7 +73,7 @@ FOREACH(T ${LEANLUATESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanluatest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua" - COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T}) + COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) ENDFOREACH(T) # LEAN DOCS diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 4514cab12..1f96f9b25 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -183,6 +183,7 @@ int main(int argc, char ** argv) { lean_assert(default_k == input_kind::Lua); script_state S; S.import("repl"); + return 0; } } else { environment env; @@ -203,12 +204,7 @@ int main(int argc, char ** argv) { } } if (k == input_kind::Lean) { - std::ifstream in(argv[i]); - if (in.bad() || in.fail()) { - std::cerr << "Failed to open file '" << argv[i] << "'\n"; - return 1; - } - if (!parse_commands(env, ios, in, &S, false, false)) + if (!parse_commands(env, ios, argv[i], &S, false, false)) ok = false; } else if (k == input_kind::OLean) { try { @@ -234,7 +230,10 @@ int main(int argc, char ** argv) { } } 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"; } + return 1; } diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp index e1336fa13..2c33377a1 100644 --- a/src/tests/frontends/lean/parser.cpp +++ b/src/tests/frontends/lean/parser.cpp @@ -22,7 +22,7 @@ static void parse(environment const & env, io_state const & ios, char const * st environment child = env->mk_child(); io_state ios_copy = ios; std::istringstream in(str); - if (parse_commands(child, ios_copy, in)) { + if (parse_commands(child, ios_copy, in, "[string]")) { formatter fmt = mk_pp_formatter(env); std::for_each(child->begin_local_objects(), child->end_local_objects(), @@ -56,7 +56,7 @@ static void tst1() { static void check(environment const & env, io_state & ios, char const * str, expr const & expected) { std::istringstream in(str); try { - expr got = parse_expr(env, ios, in); + expr got = parse_expr(env, ios, in, "[string]"); lean_assert(expected == got); } catch (exception &) { lean_unreachable(); diff --git a/src/tests/frontends/lean/scanner.cpp b/src/tests/frontends/lean/scanner.cpp index b8f4bf381..f60b2d62f 100644 --- a/src/tests/frontends/lean/scanner.cpp +++ b/src/tests/frontends/lean/scanner.cpp @@ -15,7 +15,7 @@ using namespace lean; static void scan(char const * str, list const & cmds = list()) { std::istringstream in(str); - scanner s(in); + scanner s(in, "[string]"); for (name const & n : cmds) s.add_command_keyword(n); while (true) { st t = s.scan(); @@ -45,7 +45,7 @@ static void scan_error(char const * str) { static void check(char const * str, std::initializer_list const & l, list const & cmds = list()) { auto it = l.begin(); std::istringstream in(str); - scanner s(in); + scanner s(in, "[string]"); for (name const & n : cmds) s.add_command_keyword(n); while (true) { st t = s.scan(); @@ -61,7 +61,7 @@ static void check(char const * str, std::initializer_list const static void check_name(char const * str, name const & expected) { std::istringstream in(str); - scanner s(in); + scanner s(in, "[string]"); st t = s.scan(); lean_assert(t == st::Id); lean_assert(s.get_name_val() == expected); diff --git a/src/tests/util/exception.cpp b/src/tests/util/exception.cpp index 5b9b90b81..62f192860 100644 --- a/src/tests/util/exception.cpp +++ b/src/tests/util/exception.cpp @@ -20,17 +20,17 @@ static void tst1() { static void tst2() { try { - throw parser_exception(std::string("foo"), 10, 100); + throw parser_exception(std::string("foo"), "[string]", 10, 100); } catch (parser_exception & ex) { - lean_assert(std::string("(line: 10, pos: 100) foo") == ex.what()); + lean_assert(std::string("[string]:10:100 error: foo") == ex.what()); } } static void tst3() { try { - throw parser_exception(sstream() << "msg " << 10 << " " << 20, 10, 100); + throw parser_exception(sstream() << "msg " << 10 << " " << 20, "[stream]", 10, 100); } catch (parser_exception & ex) { - lean_assert(std::string("(line: 10, pos: 100) msg 10 20") == ex.what()); + lean_assert(std::string("[stream]:10:100 error: msg 10 20") == ex.what()); } } diff --git a/src/util/exception.cpp b/src/util/exception.cpp index 020e74c05..2652d7e31 100644 --- a/src/util/exception.cpp +++ b/src/util/exception.cpp @@ -17,15 +17,18 @@ exception::exception(sstream const & strm):m_msg(strm.str()) {} exception::~exception() noexcept {} char const * exception::what() const noexcept { return m_msg.c_str(); } -parser_exception::parser_exception(char const * msg, unsigned l, unsigned p):exception(msg), m_line(l), m_pos(p) {} -parser_exception::parser_exception(std::string const & msg, unsigned l, unsigned p):exception(msg), m_line(l), m_pos(p) {} -parser_exception::parser_exception(sstream const & msg, unsigned l, unsigned p):exception(msg), m_line(l), m_pos(p) {} +parser_exception::parser_exception(char const * msg, char const * fname, unsigned l, unsigned p): + exception(msg), m_fname(fname), m_line(l), m_pos(p) {} +parser_exception::parser_exception(std::string const & msg, char const * fname, unsigned l, unsigned p): + exception(msg), m_fname(fname), m_line(l), m_pos(p) {} +parser_exception::parser_exception(sstream const & msg, char const * fname, unsigned l, unsigned p): + exception(msg), m_fname(fname), m_line(l), m_pos(p) {} parser_exception::~parser_exception() noexcept {} char const * parser_exception::what() const noexcept { try { static LEAN_THREAD_LOCAL std::string buffer; std::ostringstream s; - s << "(line: " << m_line << ", pos: " << m_pos << ") " << m_msg; + s << m_fname << ":" << m_line << ":" << m_pos << " error: " << m_msg; buffer = s.str(); return buffer.c_str(); } catch (std::exception & ex) { diff --git a/src/util/exception.h b/src/util/exception.h index 9fa627b14..ce9838c61 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -28,17 +28,18 @@ public: /** \brief Exception produced by a Lean parser. */ class parser_exception : public exception { protected: - unsigned m_line; - unsigned m_pos; + std::string m_fname; + unsigned m_line; + unsigned m_pos; public: - parser_exception(char const * msg, unsigned l, unsigned p); - parser_exception(std::string const & msg, unsigned l, unsigned p); - parser_exception(sstream const & strm, unsigned l, unsigned p); + parser_exception(char const * msg, char const * fname, unsigned l, unsigned p); + parser_exception(std::string const & msg, char const * fname, unsigned l, unsigned p); + parser_exception(sstream const & strm, char const * fname, unsigned l, unsigned p); virtual ~parser_exception() noexcept; virtual char const * what() const noexcept; unsigned get_line() const { return m_line; } unsigned get_pos() const { return m_pos; } - virtual exception * clone() const { return new parser_exception(m_msg, m_line, m_pos); } + virtual exception * clone() const { return new parser_exception(m_msg, m_fname.c_str(), m_line, m_pos); } virtual void rethrow() const { throw *this; } }; /** \brief Exception used to sign that a computation was interrupted */ diff --git a/tests/lean/alias3.lean.expected.out b/tests/lean/alias3.lean.expected.out index 2c4f79c4e..25b8c5fdc 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 -Error (line: 2, pos: 13) alias 'A' was already defined +alias3.lean:2:13 error: alias 'A' was already defined diff --git a/tests/lean/cast1.lean.expected.out b/tests/lean/cast1.lean.expected.out index ea66abcba..35cfddb5d 100644 --- a/tests/lean/cast1.lean.expected.out +++ b/tests/lean/cast1.lean.expected.out @@ -8,7 +8,7 @@ Assumed: f Assumed: m Assumed: v1 -Error (line: 13, pos: 7) type mismatch at application +cast1.lean:13:7 error: type mismatch at application f m v1 Function type: ∀ (n : ℕ), vector ℤ n → ℤ diff --git a/tests/lean/coercion1.lean.expected.out b/tests/lean/coercion1.lean.expected.out index 27689cbb1..f9796de16 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 -Error (line: 8, pos: 0) invalid coercion declaration, frontend already has a coercion for the given types +coercion1.lean:8:0 error: invalid coercion declaration, frontend already has a coercion for the given types Assumed: h -Error (line: 10, pos: 0) invalid coercion declaration, a coercion must have an arrow type (i.e., a non-dependent functional type) +coercion1.lean:10: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 -Error (line: 14, pos: 0) invalid coercion declaration, frontend already has a coercion for the given types +coercion1.lean:14:0 error: invalid coercion declaration, frontend already has a coercion for the given types Assumed: id -Error (line: 16, pos: 0) invalid coercion declaration, 'from' and 'to' types are the same +coercion1.lean:16:0 error: invalid coercion declaration, 'from' and 'to' types are the same diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out index 351e67846..d0f6b8b17 100644 --- a/tests/lean/elab1.lean.expected.out +++ b/tests/lean/elab1.lean.expected.out @@ -10,7 +10,7 @@ Failed to solve 10 ⊤ Assumed: g -Error (line: 5, pos: 8) invalid expression, it still contains metavariables after elaboration, metavariable: ?M::1, type: +elab1.lean:5:8 error: invalid expression, it still contains metavariables after elaboration, metavariable: ?M::1, type: Type Assumed: h Failed to solve @@ -54,4 +54,4 @@ Failed to solve ?M::0 Bool Bool -Error (line: 25, pos: 18) unknown identifier 'EM' +elab1.lean:25:18 error: unknown identifier 'EM' diff --git a/tests/lean/env_errors.lean.expected.out b/tests/lean/env_errors.lean.expected.out index 2f63bdc47..b84d4399b 100644 --- a/tests/lean/env_errors.lean.expected.out +++ b/tests/lean/env_errors.lean.expected.out @@ -1,12 +1,12 @@ Set: pp::colors Set: pp::unicode Assumed: x -Error (line: 3, pos: 0) set_opaque failed, 'x' is not a definition +env_errors.lean:3:0 error: set_opaque failed, 'x' is not a definition before import -Error (line: 11, pos: 0) file 'tstblafoo.lean' not found in the LEAN_PATH +env_errors.lean:11:0 error: file 'tstblafoo.lean' not found in the LEAN_PATH before load1 -Error (line: 17, pos: 0) failed to open file 'tstblafoo.lean' +env_errors.lean:17:0 error: failed to open file 'tstblafoo.lean' before load2 -Error (line: 23, pos: 0) corrupted binary file +env_errors.lean:23:0 error: corrupted binary file before load3 -Error (line: 28, pos: 0) file 'fake2.olean' does not seem to be a valid object Lean file +env_errors.lean:28:0 error: file 'fake2.olean' does not seem to be a valid object Lean file diff --git a/tests/lean/errmsg1.lean.expected.out b/tests/lean/errmsg1.lean.expected.out index 9c0be009d..f819a4519 100644 --- a/tests/lean/errmsg1.lean.expected.out +++ b/tests/lean/errmsg1.lean.expected.out @@ -2,9 +2,9 @@ Set: pp::unicode λ x : ?M::0, x λ x : ?M::0, x -Error (line: 4, pos: 10) invalid expression, it still contains metavariables after elaboration, metavariable: ?M::0, type: +errmsg1.lean:4:10 error: invalid expression, it still contains metavariables after elaboration, metavariable: ?M::0, type: (Type U) -Error (line: 6, pos: 3) failed to synthesize metavar, its type is not a proposition, metavariable: ?M::0, type: +errmsg1.lean:6:3 error: failed to synthesize metavar, its type is not a proposition, metavariable: ?M::0, type: A : Type, x : A ⊢ A → A -Error (line: 8, pos: 34) invalid definition, type still contains metavariables after elaboration, metavariable: ?M::3, type: +errmsg1.lean:8:34 error: invalid definition, type still contains metavariables after elaboration, metavariable: ?M::3, type: (Type U) diff --git a/tests/lean/ex2.lean.expected.out b/tests/lean/ex2.lean.expected.out index faa3e3168..d37f920df 100644 --- a/tests/lean/ex2.lean.expected.out +++ b/tests/lean/ex2.lean.expected.out @@ -6,11 +6,11 @@ and ⊤ ⊥ Set: pp::unicode and true false Assumed: a -Error (line: 8, pos: 0) invalid object declaration, environment already has an object named 'a' +ex2.lean:8:0 error: invalid object declaration, environment already has an object named 'a' Assumed: b and a b Assumed: A -Error (line: 12, pos: 8) type mismatch at application +ex2.lean:12:8 error: type mismatch at application and a A Function type: Bool -> Bool -> Bool @@ -19,7 +19,7 @@ Arguments types: A : Type variable A : Type (lean::pp::notation := false, pp::unicode := false, pp::colors := false) -Error (line: 15, pos: 11) unknown option 'lean::p::notation', type 'Help Options.' for list of available options -Error (line: 16, pos: 30) invalid option value, given option is not an integer +ex2.lean:15:11 error: unknown option 'lean::p::notation', type 'Help Options.' for list of available options +ex2.lean:16:30 error: invalid option value, given option is not an integer Set: lean::pp::notation a /\ b diff --git a/tests/lean/explicit.lean.expected.out b/tests/lean/explicit.lean.expected.out index 89041fe0d..5ed35aefe 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 -Error (line: 9, pos: 37) failed to mark implicit arguments for 'h', the frontend already has an object named '@h' +explicit.lean:9:37 error: failed to mark implicit arguments for 'h', the frontend already has an object named '@h' diff --git a/tests/lean/implicit2.lean.expected.out b/tests/lean/implicit2.lean.expected.out index 9964848de..59bb1551b 100644 --- a/tests/lean/implicit2.lean.expected.out +++ b/tests/lean/implicit2.lean.expected.out @@ -8,6 +8,6 @@ f 10 : ℕ → ℕ Assumed: g g 10 20 ⊤ : Bool → Bool let r : ℝ → ℝ → ℝ := g 10 20 in r : ℝ → ℝ → ℝ -Error (line: 11, pos: 0) invalid expression, unexpected token +implicit2.lean:11:0 error: invalid expression, unexpected token Set: lean::pp::implicit let r : ℝ → ℝ → ℝ := @g ℕ 10 20 ℝ in r : ℝ → ℝ → ℝ diff --git a/tests/lean/interactive/t1.lean.expected.out b/tests/lean/interactive/t1.lean.expected.out index c38116d22..01fc033e2 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 -## Error (line: 5, pos: 0) 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 -## Error (line: 6, pos: 0) 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 -## Error (line: 7, pos: 0) unknown tactic 'imp_tac2' -## Error (line: 8, pos: 0) 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 -## Error (line: 10, pos: 0) 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 9be33bea0..42821a9ac 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 -## Error (line: 15, pos: 3) unknown tactic 'simple2_tac' -## Error (line: 15, pos: 16) 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 -## Error (line: 18, pos: 0) 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 4161b2172..434225ef9 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 -## Error (line: 5, pos: 0) unknown tactic 'foo' -## Error (line: 6, pos: 5) 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 be347473a..1d552bcfe 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 -## Error (line: 9, pos: 0) 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 2c2853842..3695d252b 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 -Error (line: 4, pos: 8) invalid definition, identifier expected +stdin:4:8 error: invalid definition, identifier expected # done # \ No newline at end of file diff --git a/tests/lean/kernel_ex1.lean.expected.out b/tests/lean/kernel_ex1.lean.expected.out index be5da0b38..93dfaf2ec 100644 --- a/tests/lean/kernel_ex1.lean.expected.out +++ b/tests/lean/kernel_ex1.lean.expected.out @@ -2,12 +2,12 @@ Set: pp::unicode Assumed: N Assumed: a -Error (line: 3, pos: 14) type expected, got +kernel_ex1.lean:3:14 error: type expected, got a -Error (line: 4, pos: 6) function expected at +kernel_ex1.lean:4:6 error: function expected at a a Assumed: f -Error (line: 6, pos: 6) type mismatch at application +kernel_ex1.lean:6:6 error: type mismatch at application f (λ x : N, x) Function type: N → N diff --git a/tests/lean/let4.lean.expected.out b/tests/lean/let4.lean.expected.out index fbb63c0b6..9a35a02a9 100644 --- a/tests/lean/let4.lean.expected.out +++ b/tests/lean/let4.lean.expected.out @@ -7,18 +7,18 @@ let b := ⊤, a : ℤ := b in a let a := 10, v1 := const a ⊤, v2 := v1 in v2 : vector Bool 10 let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2 let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2 : vector Bool 10 -Error (line: 32, pos: 26) type mismatch at definition 'v2', expected type +let4.lean:32:26 error: type mismatch at definition 'v2', expected type vector ℤ a Given type: vector Bool a Assumed: foo Coercion foo -Error (line: 41, pos: 26) type mismatch at definition 'v2', expected type +let4.lean:41:26 error: type mismatch at definition 'v2', expected type vector ℤ a Given type: vector Bool a Set: lean::pp::coercion -Error (line: 49, pos: 26) type mismatch at definition 'v2', expected type +let4.lean:49:26 error: type mismatch at definition 'v2', expected type vector ℤ a Given type: vector Bool a diff --git a/tests/lean/lua2.lean.expected.out b/tests/lean/lua2.lean.expected.out index 3844e379d..166ed560d 100644 --- a/tests/lean/lua2.lean.expected.out +++ b/tests/lean/lua2.lean.expected.out @@ -3,5 +3,5 @@ Assumed: x hello world ok -Error (line: 11) executing script, attempt to call global 'rint' (a nil value) +lua2.lean:11 error: executing script, attempt to call global 'rint' (a nil value) Assumed: y diff --git a/tests/lean/nbug1.lean.expected.out b/tests/lean/nbug1.lean.expected.out index 1eb06161c..961f654c0 100644 --- a/tests/lean/nbug1.lean.expected.out +++ b/tests/lean/nbug1.lean.expected.out @@ -1,3 +1,3 @@ Set: pp::colors Set: pp::unicode -Error (line: 1, pos: 1) invalid notation declaration, at least one placeholder expected +nbug1.lean:1:1 error: invalid notation declaration, at least one placeholder expected diff --git a/tests/lean/ns1.lean.expected.out b/tests/lean/ns1.lean.expected.out index d3c5f7e1e..1dbccb73e 100644 --- a/tests/lean/ns1.lean.expected.out +++ b/tests/lean/ns1.lean.expected.out @@ -13,4 +13,4 @@ foo::T : foo::a = foo::b foo::H : foo::b ≥ foo::a foo::a : ℕ foo::bla::a : ℤ -Error (line: 19, pos: 0) invalid 'end', not inside of a scope or namespace +ns1.lean:19:0 error: invalid 'end', not inside of a scope or namespace diff --git a/tests/lean/push.lean.expected.out b/tests/lean/push.lean.expected.out index 9444e0128..3af5aeeb5 100644 --- a/tests/lean/push.lean.expected.out +++ b/tests/lean/push.lean.expected.out @@ -7,8 +7,8 @@ Assumed: c Assumed: f f a -Error (line: 11, pos: 5) unknown identifier 'f' +push.lean:11:5 error: unknown identifier 'f' variable first : Bool 10 ++ 20 : ℤ -Error (line: 20, pos: 9) unknown identifier '++' -Error (line: 22, pos: 0) main scope cannot be removed +push.lean:20:9 error: unknown identifier '++' +push.lean:22:0 error: main scope cannot be removed diff --git a/tests/lean/scan_error1.lean.expected.out b/tests/lean/scan_error1.lean.expected.out index 2b1577cee..d1ae89a23 100644 --- a/tests/lean/scan_error1.lean.expected.out +++ b/tests/lean/scan_error1.lean.expected.out @@ -1,3 +1,3 @@ Set: pp::colors Set: pp::unicode -Error (line: 1, pos: 3) invalid character sequence, '...' ellipsis expected +scan_error1.lean:1:3 error: invalid character sequence, '...' ellipsis expected diff --git a/tests/lean/scan_error2.lean.expected.out b/tests/lean/scan_error2.lean.expected.out index c4b6a5301..9f8791a70 100644 --- a/tests/lean/scan_error2.lean.expected.out +++ b/tests/lean/scan_error2.lean.expected.out @@ -1,3 +1,3 @@ Set: pp::colors Set: pp::unicode -Error (line: 1, pos: 21) unexpected end of script +scan_error2.lean:1:21 error: unexpected end of script diff --git a/tests/lean/scan_error3.lean.expected.out b/tests/lean/scan_error3.lean.expected.out index 3adacfe19..b445fcb29 100644 --- a/tests/lean/scan_error3.lean.expected.out +++ b/tests/lean/scan_error3.lean.expected.out @@ -1,3 +1,3 @@ Set: pp::colors Set: pp::unicode -Error (line: 1, pos: 23) unexpected end of script +scan_error3.lean:1:23 error: unexpected end of script diff --git a/tests/lean/scan_test2.lean.expected.out b/tests/lean/scan_test2.lean.expected.out index 70a136889..af4ec05a7 100644 --- a/tests/lean/scan_test2.lean.expected.out +++ b/tests/lean/scan_test2.lean.expected.out @@ -1,4 +1,4 @@ Set: pp::colors Set: pp::unicode a -Error (line: 7, pos: 0) Command expected +scan_test2.lean:7:0 error: Command expected diff --git a/tests/lean/tst9.lean.expected.out b/tests/lean/tst9.lean.expected.out index 0a66300da..b6d8becf1 100644 --- a/tests/lean/tst9.lean.expected.out +++ b/tests/lean/tst9.lean.expected.out @@ -4,7 +4,7 @@ Assumed: N Assumed: g Assumed: a -Error (line: 5, pos: 6) type mismatch at application +tst9.lean:5:6 error: type mismatch at application g ⊤ (f ?M::0 a a) Function type: N → N → Bool diff --git a/tests/lean/ty1.lean.expected.out b/tests/lean/ty1.lean.expected.out index f6525d2c1..a1e9a125f 100644 --- a/tests/lean/ty1.lean.expected.out +++ b/tests/lean/ty1.lean.expected.out @@ -4,7 +4,7 @@ Assumed: i λ x : ℤ, x + i : ℤ → ℤ λ x : ℕ, x + 1 : ℕ → ℕ -Error (line: 5, pos: 10) invalid expression, it still contains metavariables after elaboration, metavariable: ?M::0, type: +ty1.lean:5:10 error: invalid expression, it still contains metavariables after elaboration, metavariable: ?M::0, type: (Type U) λ x y : ℤ, y + i + 1 + x : ℤ → ℤ → ℤ (λ x : ℤ, x) i : ℤ diff --git a/tests/lean/univ.lean.expected.out b/tests/lean/univ.lean.expected.out index 7f48b94fc..134db08c3 100644 --- a/tests/lean/univ.lean.expected.out +++ b/tests/lean/univ.lean.expected.out @@ -1,5 +1,5 @@ Set: pp::colors Set: pp::unicode Defined: TypeM -Error (line: 29, pos: 0) universe constraint produces an integer overflow: Z2 >= Z1 + 1073741824 -Error (line: 42, pos: 0) universe constraint inconsistency: U1 >= U4 + 0 +univ.lean:29:0 error: universe constraint produces an integer overflow: Z2 >= Z1 + 1073741824 +univ.lean:42:0 error: universe constraint inconsistency: U1 >= U4 + 0 diff --git a/tests/lean/vars1.lean.expected.out b/tests/lean/vars1.lean.expected.out index 066e2b474..2ed0a461f 100644 --- a/tests/lean/vars1.lean.expected.out +++ b/tests/lean/vars1.lean.expected.out @@ -4,7 +4,7 @@ Assumed: a Assumed: b Assumed: c -Error (line: 3, pos: 0) invalid object declaration, environment already has an object named 'b' +vars1.lean:3:0 error: invalid object declaration, environment already has an object named 'b' Assumed: d Assumed: e Assumed: f