michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): include filename in error messages, use GNU error message style

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-09 11:01:27 -08:00
parent bcfd043a06
commit f7c7dd4ed4
44 changed files with 127 additions and 114 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/frontends/lean/parser.cpp
View file

@ -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;

8
src/frontends/lean/parser.h
View file

@ -18,8 +18,7 @@ class parser {
private:
std::unique_ptr<parser_imp> 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);
}

11
src/frontends/lean/parser_error.cpp
View file

@ -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<unsigned>(-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<void()> && f, std::function<void()
} catch (tactic_cmd_error & ex) {
CATCH(display_error(ex));
} catch (parser_exception & ex) {
CATCH(regular(m_io_state) << "Error " << ex.what() << endl;);
CATCH(regular(m_io_state) << ex.what() << endl;);
} catch (parser_error & ex) {
CATCH_CORE(display_error(ex.what(), ex.m_pos.first, ex.m_pos.second), throw parser_exception(ex.what(), ex.m_pos.first, ex.m_pos.second));
CATCH_CORE(display_error(ex.what(), ex.m_pos.first, ex.m_pos.second),
throw parser_exception(ex.what(), m_strm_name.c_str(), ex.m_pos.first, ex.m_pos.second));
} catch (kernel_exception & ex) {
CATCH(display_error(ex));
} catch (elaborator_exception & ex) {

7
src/frontends/lean/parser_imp.cpp
View file

@ -141,11 +141,12 @@ void parser_imp::sync_command() {
next();
}
parser_imp::parser_imp(environment const & env, io_state const & st, std::istream & in,
parser_imp::parser_imp(environment const & env, io_state const & st, std::istream & in, char const * strm_name,
script_state * S, bool use_exceptions, bool interactive):
m_env(env),
m_io_state(st),
m_scanner(in),
m_scanner(in, strm_name),
m_strm_name(strm_name),
m_elaborator(env),
m_use_exceptions(use_exceptions),
m_interactive(interactive),
@ -222,7 +223,7 @@ expr parser_imp::parse_expr_main() {
check_no_metavar(p, "invalid expression, it still contains metavariables after elaboration");
return p.first;
} catch (parser_error & ex) {
throw parser_exception(ex.what(), ex.m_pos.first, ex.m_pos.second);
throw parser_exception(ex.what(), m_strm_name.c_str(), ex.m_pos.first, ex.m_pos.second);
}
}
};

4
src/frontends/lean/parser_imp.h
View file

@ -59,6 +59,7 @@ class parser_imp {
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;
@ -423,7 +424,8 @@ private:
/*@}*/
public:
parser_imp(environment const & env, io_state const & st, std::istream & in, script_state * S, bool use_exceptions, bool interactive);
parser_imp(environment const & env, io_state const & st, std::istream & in, char const * strm_name,
script_state * S, bool use_exceptions, bool interactive);
~parser_imp();
static void show_prompt(bool interactive, io_state const & ios);
void show_prompt();

4
src/frontends/lean/register_module.cpp
View file

@ -23,7 +23,7 @@ static int parse_lean_expr_core(lua_State * L, rw_shared_environment const & env
script_state S = to_script_state(L);
expr r;
S.exec_unprotected([&]() {
r = parse_expr(env, st, in, &S);
r = parse_expr(env, st, in, "[string]", &S);
});
return push_expr(L, r);
}
@ -81,7 +81,7 @@ static void parse_lean_cmds_core(lua_State * L, rw_shared_environment const & en
std::istringstream in(src);
script_state S = to_script_state(L);
S.exec_unprotected([&]() {
parse_commands(env, st, in, &S);
parse_commands(env, st, in, "[string]", &S);
});
}

5
src/frontends/lean/scanner.cpp
View file

@ -92,12 +92,13 @@ char normalize(char c) {
return g_normalized[static_cast<unsigned char>(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() {

3
src/frontends/lean/scanner.h
View file

@ -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. */

4
src/frontends/lean/shell.cpp
View file

@ -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();
}

8
src/shell/CMakeLists.txt
View file

@ -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

11
src/shell/lean.cpp
View file

@ -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;
}

4
src/tests/frontends/lean/parser.cpp
View file

@ -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();

6
src/tests/frontends/lean/scanner.cpp
View file

@ -15,7 +15,7 @@ using namespace lean;
static void scan(char const * str, list<name> const & cmds = list<name>()) {
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<scanner::token> const & l, list<name> const & cmds = list<name>()) {
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<scanner::token> 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);

8
src/tests/util/exception.cpp
View file

@ -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());
}
}

11
src/util/exception.cpp
View file

@ -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) {

9
src/util/exception.h
View file

@ -28,17 +28,18 @@ public:
/** \brief Exception produced by a Lean parser. */
class parser_exception : public exception {
protected:
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 */

2
tests/lean/alias3.lean.expected.out
View file

@ -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

2
tests/lean/cast1.lean.expected.out
View file

@ -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 → ℤ

8
tests/lean/coercion1.lean.expected.out
View file

@ -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

4
tests/lean/elab1.lean.expected.out
View file

@ -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'

10
tests/lean/env_errors.lean.expected.out
View file

@ -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

6
tests/lean/errmsg1.lean.expected.out
View file

@ -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)

8
tests/lean/ex2.lean.expected.out
View file

@ -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

2
tests/lean/explicit.lean.expected.out
View file

@ -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'

2
tests/lean/implicit2.lean.expected.out
View file

@ -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 : ℝ → ℝ → ℝ

10
tests/lean/interactive/t1.lean.expected.out
View file

@ -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

6
tests/lean/interactive/t10.lean.expected.out
View file

@ -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

4
tests/lean/interactive/t2.lean.expected.out
View file

@ -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

2
tests/lean/interactive/t3.lean.expected.out
View file

@ -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:

2
tests/lean/interactive/t4.lean.expected.out
View file

@ -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
#

6
tests/lean/kernel_ex1.lean.expected.out
View file

@ -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

6
tests/lean/let4.lean.expected.out
View file

@ -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

2
tests/lean/lua2.lean.expected.out
View file

@ -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

2
tests/lean/nbug1.lean.expected.out
View file

@ -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

2
tests/lean/ns1.lean.expected.out
View file

@ -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

6
tests/lean/push.lean.expected.out
View file

@ -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

2
tests/lean/scan_error1.lean.expected.out
View file

@ -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

2
tests/lean/scan_error2.lean.expected.out
View file

@ -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

2
tests/lean/scan_error3.lean.expected.out
View file

@ -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

2
tests/lean/scan_test2.lean.expected.out
View file

@ -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

2
tests/lean/tst9.lean.expected.out
View file

@ -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

2
tests/lean/ty1.lean.expected.out
View file

@ -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 : ℤ

4
tests/lean/univ.lean.expected.out
View file

@ -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

2
tests/lean/vars1.lean.expected.out
View file

@ -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