max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages

Browse source 
Summary:

We minimize the number of "'sorry' used warning messages".  We also
re-target the error to the main declaration. Example: foo._main ==> foo
We do not report for auxiliary declarations such as "_example" and
"foo.equations._eqn_1"

Get rid of the redundant error message "error : failed" for tactics.
We added "silent failures" in the tactic framework.

We do not store line/col information for tactics nested in notation
declarations.  Before this commit, we would have tactics such
as (tactic.save_info line col) nested inside of notation declarations.
This commit is contained in:
Leonardo de Moura 2017-02-07 20:25:28 -08:00
parent 38557b5d6c
commit 54f7bf9391
59 changed files with 179 additions and 241 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
library/init/meta/async_tactic.lean
View file

@ -9,26 +9,29 @@ import init.meta.interactive
namespace tactic
private meta def report {α} (s : tactic_state) : option (unit → format) → α
| (some fmt) := undefined_core $ to_string $ fmt () ++ format.line ++ to_fmt s
| none := undefined_core "silent failure"
private meta def run_or_fail {α} (s : tactic_state) (tac : tactic α) : α :=
match tac s with
| (tactic_result.success a s) := a
| (tactic_result.exception .α fmt _ s') :=
undefined_core $ to_string $ fmt () ++ format.line ++ to_fmt s'
| (tactic_result.exception fmt _ s') := report s' fmt
end
meta def run_async {α : Type} (tac : tactic α) : tactic (task α) := do
s ← read, return $ task.delay $ λ _,
match tac s with
| (tactic_result.success a s) := a
| (tactic_result.exception .α fmt _ s') :=
undefined_core $ to_string $ fmt () ++ format.line ++ to_fmt s'
| (tactic_result.exception fmt _ s') := report s' fmt
end
meta def prove_goal_async (tac : tactic unit) : tactic unit := do
ctx ← local_context, revert_lst ctx,
tgt ← target, tgt ← instantiate_mvars tgt,
env ← get_env, tgt ← return $ env^.unfold_untrusted_macros tgt,
when tgt^.has_meta_var (fail $ "goal contains metavariables"),
when tgt^.has_meta_var (fail "goal contains metavariables"),
params ← return tgt^.collect_univ_params,
lemma_name ← new_aux_decl_name,
proof ← run_async (do

4
library/init/meta/smt/interactive.lean
View file

@ -26,9 +26,7 @@ meta def istep {α : Type} (line : nat) (col : nat) (tac : smt_tactic α) : smt_
meta def rstep {α : Type} (line : nat) (col : nat) (tac : smt_tactic α) : smt_tactic unit :=
λ ss ts, tactic_result.cases_on (istep line col tac ss ts)
(λ ⟨a, new_ss⟩ new_ts, tactic_result.success ((), new_ss) new_ts)
(λ msg_thunk e ts,
let msg := msg_thunk () ++ format.line ++ to_fmt "state:" ++ format.line ++ ts^.to_format in
(tactic.report_error line col msg >> tactic.failed) ts)
(λ msg_thunk e, tactic.report_exception line col msg_thunk)
meta def execute (tac : smt_tactic unit) : tactic unit :=
using_smt tac

2
library/init/meta/smt/smt_tactic.lean
View file

@ -76,7 +76,7 @@ meta def smt_tactic_orelse {α : Type} (t₁ t₂ : smt_tactic α) : smt_tactic
tactic_result.success
(λ e₁ ref₁ s', tactic_result.cases_on (t₂ ss ts)
tactic_result.success
(tactic_result.exception (α × smt_state)))
tactic_result.exception)
meta instance : monad_fail smt_tactic :=
{ smt_tactic.monad with fail := λ α s, (tactic.fail (to_fmt s) : smt_tactic α) }

55
library/init/meta/tactic.lean
View file

@ -27,8 +27,8 @@ meta instance : has_to_format tactic_state :=
⟨tactic_state.to_format⟩
meta inductive tactic_result (α : Type u)
| success : α → tactic_state → tactic_result
| exception : (unit → format) → option expr → tactic_state → tactic_result
| success : α → tactic_state → tactic_result
| exception {} : option (unit → format) → option expr → tactic_state → tactic_result
open tactic_result
@ -37,8 +37,9 @@ variables {α : Type u}
variables [has_to_string α]
meta def tactic_result_to_string : tactic_result α → string
| (success a s) := to_string a
| (exception .α t ref s) := "Exception: " ++ to_string (t ())
| (success a s) := to_string a
| (exception (some t) ref s) := "Exception: " ++ to_string (t ())
| (exception none ref s) := "[silent exception]"
meta instance : has_to_string (tactic_result α) :=
⟨tactic_result_to_string⟩
@ -54,12 +55,12 @@ variables {α : Type u} {β : Type v}
@[inline] meta def tactic_fmap (f : α → β) (t : tactic α) : tactic β :=
λ s, tactic_result.cases_on (t s)
(λ a s', success (f a) s')
(λ e s', exception β e s')
(λ e s', exception e s')
@[inline] meta def tactic_bind (t₁ : tactic α) (t₂ : α → tactic β) : tactic β :=
λ s, tactic_result.cases_on (t₁ s)
(λ a s', t₂ a s')
(λ e s', exception β e s')
(λ e s', exception e s')
@[inline] meta def tactic_return (a : α) : tactic α :=
λ s, success a s
@ -69,7 +70,7 @@ meta def tactic_orelse {α : Type u} (t₁ t₂ : tactic α) : tactic α :=
success
(λ e₁ ref₁ s', tactic_result.cases_on (t₂ s)
success
(exception α))
exception)
@[inline] meta def tactic_seq (t₁ : tactic α) (t₂ : tactic β) : tactic β :=
tactic_bind t₁ (λ a, t₂)
@ -81,8 +82,14 @@ end
meta instance : monad tactic :=
{map := @tactic_fmap, ret := @tactic_return, bind := @tactic_bind}
meta def tactic.mk_exception {α : Type u} {β : Type v} [has_to_format β] (msg : β) (ref : option expr) (s : tactic_state) : tactic_result α :=
exception (some (λ _, to_fmt msg)) none s
meta def tactic.fail {α : Type u} {β : Type v} [has_to_format β] (msg : β) : tactic α :=
λ s, exception α (λ u, to_fmt msg) none s
λ s, tactic.mk_exception msg none s
meta def tactic.silent_fail {α : Type u} : tactic α :=
λ s, exception none none s
meta def tactic.failed {α : Type u} : tactic α :=
tactic.fail "failed"
@ -95,14 +102,14 @@ meta instance : alternative tactic :=
meta def {u₁ u₂} tactic.up {α : Type u₂} (t : tactic α) : tactic (ulift.{u₁} α) :=
λ s, match t s with
| success a s' := success (ulift.up a) s'
| exception .α t ref s := exception (ulift α) t ref s
| success a s' := success (ulift.up a) s'
| exception t ref s := exception t ref s
end
meta def {u₁ u₂} tactic.down {α : Type u₂} (t : tactic (ulift.{u₁} α)) : tactic α :=
λ s, match t s with
| success (ulift.up a) s' := success a s'
| exception .(ulift α) t ref s := exception α t ref s
| exception t ref s := exception t ref s
end
namespace tactic
@ -121,7 +128,7 @@ try_core t >> skip
meta def fail_if_success {α : Type u} (t : tactic α) : tactic unit :=
λ s, tactic_result.cases_on (t s)
(λ a s, exception _ (λ _, to_fmt "fail_if_success combinator failed, given tactic succeeded") none s)
(λ a s, mk_exception "fail_if_success combinator failed, given tactic succeeded" none s)
(λ e ref s', success () s)
open list
@ -145,21 +152,25 @@ repeat_at_most 100000
meta def returnex {α : Type} (e : exceptional α) : tactic α :=
λ s, match e with
| (exceptional.success a) := tactic_result.success a s
| (exceptional.exception .α f) := tactic_result.exception α (λ u, f options.mk) none s -- TODO(Leo): extract options from environment
| exceptional.success a := success a s
| exceptional.exception .α f := exception (some (λ u, f options.mk)) none s -- TODO(Leo): extract options from environment
end
meta def returnopt (e : option α) : tactic α :=
λ s, match e with
| (some a) := tactic_result.success a s
| none := tactic_result.exception α (λ u, to_fmt "failed") none s
| (some a) := success a s
| none := mk_exception "failed" none s
end
/- Decorate t's exceptions with msg -/
meta def decorate_ex (msg : format) (t : tactic α) : tactic α :=
λ s, tactic_result.cases_on (t s)
success
(λ e, exception α (λ u, msg ++ format.nest 2 (format.line ++ e u)))
(λ opt_thunk,
match opt_thunk with
| some e := exception (some (λ u, msg ++ format.nest 2 (format.line ++ e u)))
| none := exception none
end)
@[inline] meta def write (s' : tactic_state) : tactic unit :=
λ s, success () s'
@ -461,14 +472,18 @@ t >>[tactic] cleanup
meta def istep {α : Type u} (line : nat) (col : nat) (t : tactic α) : tactic unit :=
λ s, @scope_trace _ line col ((t >>[tactic] cleanup) s)
meta def report_exception {α : Type} (line col : nat) : option (unit → format) → tactic α
| (some msg_thunk) := λ s,
let msg := msg_thunk () ++ format.line ++ to_fmt "state:" ++ format.line ++ s^.to_format in
(tactic.report_error line col msg >> silent_fail) s
| none := silent_fail
/- Auxiliary definition used to implement begin ... end blocks.
It is similar to step, but it reports an error at the given line/col if the tactic t fails. -/
meta def rstep {α : Type u} (line : nat) (col : nat) (t : tactic α) : tactic unit :=
λ s, tactic_result.cases_on (istep line col t s)
(λ a new_s, tactic_result.success () new_s)
(λ msg_thunk e new_s,
let msg := msg_thunk () ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
(tactic.report_error line col msg >> tactic.failed) new_s)
(λ msg_thunk e, report_exception line col msg_thunk)
meta def is_prop (e : expr) : tactic bool :=
do t ← infer_type e,

2
src/frontends/lean/decl_util.cpp
View file

@ -48,7 +48,7 @@ expr parse_single_header(parser & p, buffer<name> & lp_names, buffer<expr> & par
auto c_pos = p.pos();
name c_name;
if (is_example) {
c_name = get_this_tk();
c_name = "_example";
} else {
if (!is_instance)
parse_univ_params(p, lp_names);

25
src/frontends/lean/elaborator.cpp
View file

@ -2858,18 +2858,21 @@ void elaborator::invoke_tactic(expr const & mvar, expr const & tactic) {
tactic_state s = mk_tactic_state_for(mvar);
try {
tactic_state new_s = tactic_evaluator(m_ctx, m_opts)(s, tactic, ref);
metavar_context mctx = new_s.mctx();
expr val = mctx.instantiate_mvars(new_s.main());
if (has_expr_metavar(val)) {
val = recoverable_error(some_expr(type), ref,
unsolved_tactic_state(new_s, "tactic failed, result contains meta-variables", ref));
if (optional<tactic_state> new_s = tactic_evaluator(m_ctx, m_opts)(s, tactic, ref)) {
metavar_context mctx = new_s->mctx();
expr val = mctx.instantiate_mvars(new_s->main());
if (has_expr_metavar(val)) {
val = recoverable_error(some_expr(type), ref,
unsolved_tactic_state(*new_s, "tactic failed, result contains meta-variables", ref));
}
mctx.assign(mvar, val);
m_env = new_s->env();
m_ctx.set_env(m_env);
m_ctx.set_mctx(mctx);
} else {
m_ctx.assign(mvar, mk_sorry(some_expr(type), ref));
m_has_errors = true;
}
mctx.assign(mvar, val);
m_env = new_s.env();
m_ctx.set_env(m_env);
m_ctx.set_mctx(mctx);
} catch (std::exception & ex) {
if (try_report(ex, some_expr(ref))) {
m_ctx.assign(mvar, mk_sorry(some_expr(type), ref));

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

@ -24,6 +24,7 @@ Author: Leonardo de Moura
#include "library/module_mgr.h"
#include "library/export_decl.h"
#include "library/trace.h"
#include "library/quote.h"
#include "library/class.h"
#include "library/exception.h"
#include "library/aliases.h"
@ -341,16 +342,24 @@ expr parser::rec_save_pos(expr const & e, pos_info p) {
expr parser::copy_with_new_pos(expr const & e, pos_info p) {
switch (e.kind()) {
case expr_kind::Sort: case expr_kind::Constant: case expr_kind::Meta:
case expr_kind::Local: case expr_kind::Var:
case expr_kind::Var: case expr_kind::Local:
return save_pos(copy(e), p);
case expr_kind::App:
return save_pos(::lean::mk_app(copy_with_new_pos(app_fn(e), p),
copy_with_new_pos(app_arg(e), p)),
p);
case expr_kind::Lambda: case expr_kind::Pi:
return save_pos(update_binding(e,
copy_with_new_pos(binding_domain(e), p),
copy_with_new_pos(binding_body(e), p)),
case expr_kind::Lambda:
return save_pos(::lean::mk_lambda(binding_name(e),
copy_with_new_pos(binding_domain(e), p),
copy_with_new_pos(binding_body(e), p),
binding_info(e)),
p);
case expr_kind::Pi:
return save_pos(::lean::mk_pi(binding_name(e),
copy_with_new_pos(binding_domain(e), p),
copy_with_new_pos(binding_body(e), p),
binding_info(e)),
p);
case expr_kind::Let:
return save_pos(::lean::mk_let(let_name(e),
@ -358,12 +367,16 @@ expr parser::copy_with_new_pos(expr const & e, pos_info p) {
copy_with_new_pos(let_value(e), p),
copy_with_new_pos(let_body(e), p)),
p);
case expr_kind::Macro: {
buffer<expr> args;
for (unsigned i = 0; i < macro_num_args(e); i++)
args.push_back(copy_with_new_pos(macro_arg(e, i), p));
return save_pos(::lean::mk_macro(macro_def(e), args.size(), args.data()), p);
}}
case expr_kind::Macro:
if (is_quote(e)) {
return save_pos(mk_quote_core(copy_with_new_pos(get_quote_expr(e), p)), p);
} else {
buffer<expr> args;
for (unsigned i = 0; i < macro_num_args(e); i++)
args.push_back(copy_with_new_pos(macro_arg(e, i), p));
return save_pos(::lean::mk_macro(macro_def(e), args.size(), args.data()), p);
}
}
lean_unreachable(); // LCOV_EXCL_LINE
}

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

@ -498,6 +498,8 @@ public:
in_notation_ctx(parser & p):m_ctx(p.m_scanner) {}
};
bool in_notation() const { return m_scanner.in_notation(); }
public:
/* pos_info_provider API */
virtual optional<pos_info> get_pos_info(expr const & e) const override;

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

@ -103,6 +103,8 @@ public:
public:
in_notation_ctx(scanner & s):m_in_notation(s.m_in_notation, true) {}
};
bool in_notation() const { return m_in_notation; }
};
std::ostream & operator<<(std::ostream & out, token_kind k);
bool is_id_rest(char const * begin, char const * end);

18
src/frontends/lean/tactic_evaluator.cpp
View file

@ -82,29 +82,31 @@ static void process_failure(vm_state & S, vm_obj const & r, expr const & ref) {
else
throw_unsolved_tactic_state(s1, fmt, ref);
}
/* Do nothing if it is a silent failure */
lean_assert(is_tactic_silent_exception(r));
}
tactic_state tactic_evaluator::execute_tactic(expr const & tactic, tactic_state const & s, expr const & ref) {
optional<tactic_state> tactic_evaluator::execute_tactic(expr const & tactic, tactic_state const & s, expr const & ref) {
name tactic_name("_tactic");
environment new_env = compile_tactic(tactic_name, tactic);
vm_state S(new_env, m_opts);
vm_obj r = invoke_tactic(S, tactic_name, {to_obj(s)});
if (optional<tactic_state> new_s = is_tactic_success(r)) {
return *new_s;
return new_s;
}
process_failure(S, r, ref);
lean_unreachable();
return optional<tactic_state>();
}
tactic_state tactic_evaluator::execute_atomic(tactic_state const & s, expr const & tactic, expr const & ref) {
tactic_state new_s = execute_tactic(tactic, s, ref);
if (new_s.goals())
throw_unsolved_tactic_state(new_s, "tactic failed, there are unsolved goals", ref);
optional<tactic_state> tactic_evaluator::execute_atomic(tactic_state const & s, expr const & tactic, expr const & ref) {
optional<tactic_state> new_s = execute_tactic(tactic, s, ref);
if (new_s && new_s->goals())
throw_unsolved_tactic_state(*new_s, "tactic failed, there are unsolved goals", ref);
return new_s;
}
tactic_state tactic_evaluator::operator()(tactic_state const & s, expr const & tactic, expr const & ref) {
optional<tactic_state> tactic_evaluator::operator()(tactic_state const & s, expr const & tactic, expr const & ref) {
return execute_atomic(s, tactic, ref);
}

6
src/frontends/lean/tactic_evaluator.h
View file

@ -21,11 +21,11 @@ class tactic_evaluator {
environment compile_tactic(name const & tactic_name, expr const & tactic);
vm_obj invoke_tactic(vm_state & S, name const & tactic_name, std::initializer_list<vm_obj> const & args);
tactic_state execute_tactic(expr const & tactic, tactic_state const & s, expr const & ref);
tactic_state execute_atomic(tactic_state const & s, expr const & tactic, expr const & ref);
optional<tactic_state> execute_tactic(expr const & tactic, tactic_state const & s, expr const & ref);
optional<tactic_state> execute_atomic(tactic_state const & s, expr const & tactic, expr const & ref);
public:
tactic_evaluator(type_context & ctx, options const & opts);
tactic_state operator()(tactic_state const & s, expr const & tactic, expr const & ref);
optional<tactic_state> operator()(tactic_state const & s, expr const & tactic, expr const & ref);
};
}

6
src/frontends/lean/tactic_notation.cpp
View file

@ -60,6 +60,8 @@ static expr mk_tactic_step(parser & p, expr tac, pos_info const & pos, name cons
}
static expr mk_tactic_rstep(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool report_error) {
if (p.in_notation())
return mk_tactic_step(p, tac, pos, tac_class);
if (tac.get_tag() == nulltag)
tac = p.save_pos(tac, pos);
name c;
@ -570,8 +572,8 @@ expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
p.clear_expr_locals();
auto tac_pos = p.pos();
try {
bool use_rstep = false;
bool report_error = false;
bool use_rstep = true;
bool report_error = true;
expr tac = parse_tactic(p, get_tactic_name(), use_rstep, report_error);
expr type = mk_tactic_unit(get_tactic_name());
expr r = p.save_pos(mk_typed_expr(type, tac), tac_pos);

23
src/library/module.cpp
View file

@ -466,10 +466,29 @@ struct add_decl_sorry_check : public task<unit> {
bool is_tiny() const override { return true; }
task_kind get_kind() const override { return task_kind::elab; }
optional<name> should_report_sorry(name const & n) {
if (n.is_anonymous())
return optional<name>();
if (!is_internal_name(n))
return optional<name>(n);
if (!n.is_string() || n.is_atomic())
return optional<name>();
if (strcmp(n.get_string(), "_main") == 0)
return should_report_sorry(n.get_prefix());
if (strncmp(n.get_string(), "_match", 6) == 0) {
// TODO(Leo): we may report the same function multiple times,
// if it contains many nested match-expressions containing sorry.
return should_report_sorry(n.get_prefix());
}
return optional<name>();
}
unit execute() override {
if (has_sorry(m_decl)) {
report_message(message(get_module_id(), m_pos, WARNING,
(sstream() << "declaration '" << m_decl.get_name() << "' uses sorry").str()));
if (optional<name> n = should_report_sorry(m_decl.get_name())) {
report_message(message(get_module_id(), m_pos, WARNING,
(sstream() << "declaration '" << *n << "' uses sorry").str()));
}
}
return {};
}

1
src/library/quote.h
View file

@ -11,6 +11,7 @@ namespace lean {
expr mk_quote(expr const & e);
bool is_quote(expr const & e);
expr const & get_quote_expr(expr const & e);
expr mk_quote_core(expr const & e);
expr mk_antiquote(expr const & e);
bool is_antiquote(expr const & e);

12
src/library/tactic/tactic_state.cpp
View file

@ -273,8 +273,8 @@ optional<tactic_state> is_tactic_success(vm_obj const & o) {
}
optional<tactic_exception_info> is_tactic_exception(vm_state & S, vm_obj const & ex) {
if (is_constructor(ex) && cidx(ex) == 1) {
vm_obj fmt = S.invoke(cfield(ex, 0), mk_vm_unit());
if (is_constructor(ex) && cidx(ex) == 1 && !is_none(cfield(ex, 0))) {
vm_obj fmt = S.invoke(get_some_value(cfield(ex, 0)), mk_vm_unit());
optional<expr> ref;
if (!is_none(cfield(ex, 1)))
ref = to_expr(get_some_value(cfield(ex, 1)));
@ -284,6 +284,10 @@ optional<tactic_exception_info> is_tactic_exception(vm_state & S, vm_obj const &
}
}
bool is_tactic_silent_exception(vm_obj const & ex) {
return is_constructor(ex) && cidx(ex) == 1 && is_none(cfield(ex, 0));
}
vm_obj mk_tactic_result(vm_obj const & a, vm_obj const & s) {
lean_assert(is_tactic_state(s));
return mk_vm_constructor(0, a, s);
@ -316,11 +320,11 @@ vm_obj mk_tactic_success(tactic_state const & s) {
}
vm_obj mk_tactic_exception(vm_obj const & fn, tactic_state const & s) {
return mk_vm_constructor(1, fn, mk_vm_none(), to_obj(s));
return mk_vm_constructor(1, mk_vm_some(fn), mk_vm_none(), to_obj(s));
}
vm_obj mk_tactic_exception(vm_obj const & fn, vm_obj const & ref, tactic_state const & s) {
return mk_vm_constructor(1, fn, ref, to_obj(s));
return mk_vm_constructor(1, mk_vm_some(fn), ref, to_obj(s));
}
vm_obj mk_tactic_exception(throwable const & ex, tactic_state const & s) {

1
src/library/tactic/tactic_state.h
View file

@ -155,6 +155,7 @@ typedef std::tuple<format, optional<expr>, tactic_state> tactic_exception_info;
/* If ex is (base_tactic_result.exception fn), then return (fn ()).
The vm_state S is used to execute (fn ()). */
optional<tactic_exception_info> is_tactic_exception(vm_state & S, vm_obj const & ex);
bool is_tactic_silent_exception(vm_obj const & ex);
type_context mk_type_context_for(tactic_state const & s, transparency_mode m = transparency_mode::Semireducible);
type_context mk_type_context_for(tactic_state const & s, local_context const & lctx, transparency_mode m = transparency_mode::Semireducible);

1
tests/lean/1162.lean.expected.out
View file

@ -1,3 +1,2 @@
1162.lean:10:12: error: equation compiler error, equation #2 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
1162.lean:7:4: warning: declaration 'ppday' uses sorry
1162.lean:7:4: warning: declaration 'ppday.equations._eqn_1' uses sorry

7
tests/lean/1258.lean.expected.out
View file

@ -6,10 +6,3 @@ foo : ∀ (ns : list ℕ), P xs ns,
n : ℕ,
ns : list ℕ
⊢ P xs (n :: ns)
1258.lean:4:54: error: failed
state:
xs : list ℕ,
foo : ∀ (ns : list ℕ), P xs ns,
n : ℕ,
ns : list ℕ
⊢ P xs (n :: ns)

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

@ -8,11 +8,3 @@ f₁ : α₁ → α₁,
f₂ : Π ⦃a : α₁⦄, α₂ a → α₂ (f₁ a),
eq₁ : f₁ = id
⊢ map f₁ f₂ = id
1277.lean:9:0: error: failed
state:
α₁ : Type,
α₂ : α₁ → Type,
f₁ : α₁ → α₁,
f₂ : Π ⦃a : α₁⦄, α₂ a → α₂ (f₁ a),
eq₁ : f₁ = id
⊢ map f₁ f₂ = id

1
tests/lean/anc1.lean.expected.out
View file

@ -1,6 +1,5 @@
(1, 2) : ℕ × ℕ
and.intro trivial trivial : true ∧ true
anc1.lean:5:8: warning: declaration '_example' uses sorry
{fst := 1, snd := sorry} : Σ' (x : ℕ), x > 0
show true, from true.intro : true
Exists.intro 1 (id_locked (1 ≠ 0) (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0

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

@ -10,9 +10,3 @@ a b c : ℕ,
h1 : a = b,
h2 : b = c
⊢ c = a
auto_quote_error.lean:6:0: error: failed
state:
a b c : ℕ,
h1 : a = b,
h2 : b = c
⊢ c = a

35
tests/lean/auto_quote_error2.lean.expected.out
View file

@ -8,17 +8,6 @@ a_1 : a = b,
a_2 : b = c
⊢ a = c
a b c : ℕ,
a_1 : a = b,
a_2 : b = c
⊢ Sort ?
auto_quote_error2.lean:8:0: error: failed
state:
a b c : ℕ,
a_1 : a = b,
a_2 : b = c
⊢ a = c
a b c : ℕ,
a_1 : a = b,
a_2 : b = c
@ -30,12 +19,6 @@ a b c : ℕ,
a_1 : a = b,
a_2 : b = c
⊢ a = c
auto_quote_error2.lean:19:0: error: failed
state:
a b c : ℕ,
a_1 : a = b,
a_2 : b = c
⊢ a = c
hello world
auto_quote_error2.lean:28:2: error: focus tactic failed, focused goal has not been solved
state:
@ -43,12 +26,6 @@ a b c : ℕ,
a_1 : a = b,
a_2 : b = c
⊢ a = ?m_1
auto_quote_error2.lean:30:0: error: failed
state:
a b c : ℕ,
a_1 : a = b,
a_2 : b = c
⊢ a = ?m_1
auto_quote_error2.lean:37:22: error: don't know how to synthesize placeholder
context:
a b c : ℕ,
@ -61,15 +38,3 @@ a b c : ℕ,
h1 : a = b,
h2 : b = c
⊢ a = c
auto_quote_error2.lean:38:2: error: failed
state:
a b c : ℕ,
h1 : a = b,
h2 : b = c
⊢ a = c
auto_quote_error2.lean:39:0: error: failed
state:
a b c : ℕ,
h1 : a = b,
h2 : b = c
⊢ a = c

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

@ -8,6 +8,4 @@ has type
vec ℕ n
but is expected to have type
vec ℕ 10
aux_decl_zeta.lean:5:11: warning: declaration 'f._main' uses sorry
aux_decl_zeta.lean:5:11: warning: declaration 'f._main.equations._eqn_1' uses sorry
aux_decl_zeta.lean:5:11: warning: declaration 'f.equations._eqn_1' uses sorry
aux_decl_zeta.lean:5:11: warning: declaration 'f' uses sorry

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

@ -7,13 +7,3 @@ _match : (∃ (k_1 : ℕ), k + n + k_1 = k + m) → n ≤ m,
w : ℕ,
hw : (λ (k_1 : ℕ), k + n + k_1 = k + m) w
⊢ n + w = m
bad_error2.lean:10:4: error: failed
state:
k n m : ℕ,
h : k + n ≤ k + m,
_match : (∃ (k_1 : ℕ), k + n + k_1 = k + m) → n ≤ m,
w : ℕ,
hw : (λ (k_1 : ℕ), k + n + k_1 = k + m) w
⊢ n + w = m
bad_error2.lean:3:8: warning: declaration 'this._match_1' uses sorry
bad_error2.lean:3:8: warning: declaration 'this._match_1.equations._eqn_1' uses sorry

1
tests/lean/bad_error3.lean.expected.out
View file

@ -11,4 +11,3 @@ state:
p : ℕ → ℕ → Prop
⊢ sorry
bad_error3.lean:5:4: warning: declaration 'ex' uses sorry
bad_error3.lean:5:4: warning: declaration 'ex.equations._eqn_1' uses sorry

1
tests/lean/bad_error4.lean.expected.out
View file

@ -7,4 +7,3 @@ has type
but is expected to have type
unit → unit
bad_error4.lean:4:11: warning: declaration 'bar' uses sorry
bad_error4.lean:4:11: warning: declaration 'bar.equations._eqn_1' uses sorry

9
tests/lean/bad_error5.lean.expected.out
View file

@ -1,3 +1,8 @@
bad_error5.lean:13:10: error: _tactic._val_3: trying to evaluate sorry
bad_error5.lean:13:10: error: don't know how to synthesize placeholder
context:
c : S
⊢ Type ?
bad_error5.lean:13:10: error: failed to add declaration '_tactic' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
…
bad_error5.lean:9:11: warning: declaration 'V' uses sorry
bad_error5.lean:9:11: warning: declaration 'V.equations._eqn_1' uses sorry

3
tests/lean/bad_inaccessible.lean.expected.out
View file

@ -1,13 +1,10 @@
bad_inaccessible.lean:3:5: error: invalid use of inaccessible term, it is not fixed by other arguments
bad_inaccessible.lean:2:11: warning: declaration 'f1' uses sorry
bad_inaccessible.lean:2:11: warning: declaration 'f1.equations._eqn_1' uses sorry
bad_inaccessible.lean:6:7: error: invalid use of inaccessible term, the provided term is
b
but is expected to be
a
bad_inaccessible.lean:5:11: warning: declaration 'f2' uses sorry
bad_inaccessible.lean:5:11: warning: declaration 'f2.equations._eqn_1' uses sorry
bad_inaccessible.lean:14:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments
.?m_1 + 1
bad_inaccessible.lean:12:11: warning: declaration 'foo' uses sorry
bad_inaccessible.lean:12:11: warning: declaration 'foo.equations._eqn_1' uses sorry

1
tests/lean/bad_inaccessible2.lean.expected.out
View file

@ -8,4 +8,3 @@ but is expected to have type
vec A .(.?m_2 + 1)
bad_inaccessible2.lean:31:46: error: ill-formed match/equations expression
bad_inaccessible2.lean:29:11: warning: declaration 'map_head' uses sorry
bad_inaccessible2.lean:29:11: warning: declaration 'map_head.equations._eqn_1' uses sorry

1
tests/lean/cls_err.lean.expected.out
View file

@ -2,4 +2,3 @@ cls_err.lean:13:2: error: failed to synthesize type class instance for
A : Type u
⊢ H A
cls_err.lean:12:13: warning: declaration 'tst' uses sorry
cls_err.lean:12:13: warning: declaration 'tst.equations._eqn_1' uses sorry

1
tests/lean/crash.lean.expected.out
View file

@ -17,4 +17,3 @@ H : P,
H' : ¬P
⊢ sorry
crash.lean:6:11: warning: declaration 'crash' uses sorry
crash.lean:6:11: warning: declaration 'crash.equations._eqn_1' uses sorry

1
tests/lean/ctx.lean.expected.out
View file

@ -7,4 +7,3 @@ h : A = B,
p1 p2 : A × B
⊢ ℕ
ctx.lean:2:11: warning: declaration 'foo' uses sorry
ctx.lean:2:11: warning: declaration 'foo.equations._eqn_1' uses sorry

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

@ -4,10 +4,4 @@ p q : Prop,
a : p,
a_1 : q
⊢ p
do_match_fail.lean:9:0: error: failed
state:
p q : Prop,
a : p,
a_1 : q
⊢ p
do_match_fail.lean:20:3: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)

1
tests/lean/elab_error_msgs.lean.expected.out
View file

@ -9,7 +9,6 @@ but is expected to have type
Additional information:
elab_error_msgs.lean:2:0: context: 'eliminator' elaboration was not used for 'and.rec' because it is not fully applied, #2 explicit arguments expected
elab_error_msgs.lean:5:4: warning: declaration 'bogus_elim' uses sorry
elab_error_msgs.lean:5:4: warning: declaration 'bogus_elim.equations._eqn_1' uses sorry
elab_error_msgs.lean:9:0: error: type mismatch at application
bogus_elim trivial
term

26
tests/lean/elab_error_recovery.lean.expected.out
View file

@ -12,7 +12,13 @@ half_baked : ℕ → ℕ
elab_error_recovery.lean:8:8: error: failed to synthesize type class instance for
half_baked : ℕ → ℕ
⊢ decidable (2 ∈ 3)
elab_error_recovery.lean:10:11: error: undefined
elab_error_recovery.lean:10:11: error: don't know how to synthesize placeholder
context:
half_baked : ℕ → ℕ
⊢ Type ?
elab_error_recovery.lean:10:11: error: failed to add declaration '_tactic' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
…
elab_error_recovery.lean:12:14: error: invalid type ascription, expression has type
list ?m_1
but is expected to have type
@ -21,11 +27,6 @@ state:
half_baked : ℕ → ℕ,
_x : ℕ
⊢ ℕ
elab_error_recovery.lean:12:23: error: failed
state:
half_baked : ℕ → ℕ,
_x : ℕ
⊢ ℕ
elab_error_recovery.lean:6:8: error: don't know how to synthesize placeholder
context:
half_baked : ℕ → ℕ
@ -34,18 +35,7 @@ elab_error_recovery.lean:8:29: error: don't know how to synthesize placeholder
context:
half_baked : ℕ → ℕ
⊢ ℕ
elab_error_recovery.lean:1:4: warning: declaration 'half_baked._main' uses sorry
elab_error_recovery.lean:1:4: warning: declaration 'half_baked._main.equations._eqn_1' uses sorry
elab_error_recovery.lean:1:4: warning: declaration 'half_baked._main.equations._eqn_2' uses sorry
elab_error_recovery.lean:1:4: warning: declaration 'half_baked._main.equations._eqn_3' uses sorry
elab_error_recovery.lean:1:4: warning: declaration 'half_baked._main.equations._eqn_4' uses sorry
elab_error_recovery.lean:1:4: warning: declaration 'half_baked._main.equations._eqn_5' uses sorry
elab_error_recovery.lean:1:4: warning: declaration 'half_baked._main.equations._eqn_6' uses sorry
elab_error_recovery.lean:1:4: warning: declaration 'half_baked.equations._eqn_2' uses sorry
elab_error_recovery.lean:1:4: warning: declaration 'half_baked.equations._eqn_3' uses sorry
elab_error_recovery.lean:1:4: warning: declaration 'half_baked.equations._eqn_4' uses sorry
elab_error_recovery.lean:1:4: warning: declaration 'half_baked.equations._eqn_5' uses sorry
elab_error_recovery.lean:1:4: warning: declaration 'half_baked.equations._eqn_6' uses sorry
elab_error_recovery.lean:1:4: warning: declaration 'half_baked' uses sorry
def half_baked._main : ℕ → ℕ :=
λ (a : ℕ),
ite (a = 3) 2

1
tests/lean/empty.lean.expected.out
View file

@ -1,4 +1,3 @@
empty.lean:6:39: error: failed to synthesize type class instance for
⊢ nonempty Empty
empty.lean:6:25: warning: declaration 'v2' uses sorry
empty.lean:6:25: warning: declaration 'v2.equations._eqn_1' uses sorry

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

@ -4,7 +4,6 @@ f : ℕ → ℕ
⊢ ℕ
eqn_hole.lean:2:11: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
eqn_hole.lean:2:11: warning: declaration 'f' uses sorry
eqn_hole.lean:2:11: warning: declaration 'f.equations._eqn_1' uses sorry
eqn_hole.lean:8:13: error: don't know how to synthesize placeholder
context:
g : ℕ → ℕ,
@ -12,4 +11,3 @@ n : ℕ
⊢ ℕ
eqn_hole.lean:6:11: error: support for well-founded recursion has not been implemented yet, use 'set_option trace.eqn_compiler true' for additional information
eqn_hole.lean:6:11: warning: declaration 'g' uses sorry
eqn_hole.lean:6:11: warning: declaration 'g.equations._eqn_1' uses sorry

1
tests/lean/error_pos.lean.expected.out
View file

@ -1,6 +1,5 @@
error_pos.lean:1:39: error: type expected at
B
error_pos.lean:1:8: warning: declaration '_example' uses sorry
error_pos.lean:4:43: error: type expected at
B
error_pos.lean:9:39: error: type expected at

1
tests/lean/hole_in_fn.lean.expected.out
View file

@ -3,4 +3,3 @@ context:
n : ℕ
⊢ ℕ
hole_in_fn.lean:5:11: warning: declaration 'f' uses sorry
hole_in_fn.lean:5:11: warning: declaration 'f.equations._eqn_1' uses sorry

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

@ -1,5 +1,4 @@
hole_issue2.lean:12:25: warning: declaration 'count' uses sorry
hole_issue2.lean:12:25: warning: declaration 'count.equations._eqn_1' uses sorry
hole_issue2.lean:22:74: error: don't know how to synthesize placeholder
context:
A : Type,
@ -11,8 +10,7 @@ h : ⟦l₁⟧ ⊆ ⟦l₂⟧,
w : A,
hw : ¬list.count w l₁ ≤ list.count w l₂
⊢ false
hole_issue2.lean:18:25: warning: declaration 'decidable_subbag_1._match_1' uses sorry
hole_issue2.lean:18:25: warning: declaration 'decidable_subbag_1._match_1.equations._eqn_1' uses sorry
hole_issue2.lean:18:25: warning: declaration 'decidable_subbag_1' uses sorry
hole_issue2.lean:29:65: error: don't know how to synthesize placeholder
context:
A : Type,
@ -22,8 +20,7 @@ _match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦
H : subcount l₁ l₂ = ff,
h : ⟦l₁⟧ ⊆ ⟦l₂⟧
⊢ ∀ (a : A), ¬list.count a l₁ ≤ list.count a l₂ → false
hole_issue2.lean:25:25: warning: declaration 'decidable_subbag_2._match_1' uses sorry
hole_issue2.lean:25:25: warning: declaration 'decidable_subbag_2._match_1.equations._eqn_1' uses sorry
hole_issue2.lean:25:25: warning: declaration 'decidable_subbag_2' uses sorry
hole_issue2.lean:36:28: error: don't know how to synthesize placeholder
context:
A : Type,
@ -33,5 +30,4 @@ _match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦
H : subcount l₁ l₂ = ff,
h : ⟦l₁⟧ ⊆ ⟦l₂⟧
⊢ false
hole_issue2.lean:32:25: warning: declaration 'decidable_subbag_3._match_1' uses sorry
hole_issue2.lean:32:25: warning: declaration 'decidable_subbag_3._match_1.equations._eqn_1' uses sorry
hole_issue2.lean:32:25: warning: declaration 'decidable_subbag_3' uses sorry

3
tests/lean/inaccessible.lean.expected.out
View file

@ -4,7 +4,6 @@ inaccessible.lean:14:2: error: invalid occurrence of macro expression in pattern
sorry
inaccessible.lean:14:17: error: ill-formed match/equations expression
inaccessible.lean:13:11: warning: declaration 'inv_3' uses sorry
inaccessible.lean:13:11: warning: declaration 'inv_3.equations._eqn_1' uses sorry
inaccessible.lean:17:11: error: invalid inaccessible annotation, it cannot be used around functions in applications
inaccessible.lean:25:12: error: invalid pattern, 'a' already appeared in this pattern
inaccessible.lean:28:3: error: function expected at
@ -19,9 +18,7 @@ but is expected to have type
imf f sorry
inaccessible.lean:28:16: error: ill-formed match/equations expression
inaccessible.lean:27:11: warning: declaration 'inv_7' uses sorry
inaccessible.lean:27:11: warning: declaration 'inv_7.equations._eqn_1' uses sorry
inaccessible.lean:31:4: error: invalid pattern, 'a' already appeared in this pattern
inaccessible.lean:82:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments
.?m_1 + 1
inaccessible.lean:80:11: warning: declaration 'map_6' uses sorry
inaccessible.lean:80:11: warning: declaration 'map_6.equations._eqn_1' uses sorry

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

@ -4,10 +4,8 @@ inaccessible2.lean:5:4: error: invalid use of inaccessible term, the provided te
but is expected to be
f a
inaccessible2.lean:4:11: warning: declaration 'inv_1' uses sorry
inaccessible2.lean:4:11: warning: declaration 'inv_1.equations._eqn_1' uses sorry
inaccessible2.lean:8:10: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
inaccessible2.lean:11:11: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
inaccessible2.lean:14:9: error: invalid pattern, in a constructor application, the parameters of the inductive datatype must be marked as inaccessible
inaccessible2.lean:14:20: error: ill-formed match/equations expression
inaccessible2.lean:13:11: warning: declaration 'symm' uses sorry
inaccessible2.lean:13:11: warning: declaration 'symm.equations._eqn_1' uses sorry

3
tests/lean/instance_cache1.lean.expected.out
View file

@ -4,18 +4,15 @@ a : A,
this : has_add A
⊢ has_add A
instance_cache1.lean:1:11: warning: declaration 'f1' uses sorry
instance_cache1.lean:1:11: warning: declaration 'f1.equations._eqn_1' uses sorry
instance_cache1.lean:6:7: error: failed to synthesize type class instance for
A : Type ?,
a : A,
s : has_add A
⊢ has_add A
instance_cache1.lean:5:11: warning: declaration 'f2' uses sorry
instance_cache1.lean:5:11: warning: declaration 'f2.equations._eqn_1' uses sorry
instance_cache1.lean:9:19: error: failed to synthesize type class instance for
A : Type ?,
a : A,
s : has_add A
⊢ has_add A
instance_cache1.lean:8:11: warning: declaration 'f3' uses sorry
instance_cache1.lean:8:11: warning: declaration 'f3.equations._eqn_1' uses sorry

8
tests/lean/interactive/do_info.lean.expected.out
View file

@ -1,7 +1,7 @@
{"msg":{"caption":"trace output","file_name":"f","pos_col":0,"pos_line":3,"severity":"information","text":"a b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ a = ?m_1\n\na b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ ?m_1 = c\n"},"response":"additional_message"}
{"msg":{"caption":"trace output","file_name":"f","pos_col":3,"pos_line":4,"severity":"information","text":"a b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ a = ?m_1\n\na b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ ?m_1 = c\n"},"response":"additional_message"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"full-id":"tactic.intro","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":496},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"name → tactic expr"},"response":"ok","seq_num":6}
{"record":{"full-id":"tactic.intro","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":511},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"name → tactic expr"},"response":"ok","seq_num":6}
{"record":{"full-id":"tactic.transitivity","source":{"column":9,"file":"/library/init/meta/relation_tactics.lean","line":30},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":9}
{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":603},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":12}
{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":618},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":12}
{"record":{"full-id":"tactic.symmetry","source":{"column":9,"file":"/library/init/meta/relation_tactics.lean","line":27},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":14}
{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":603},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":16}
{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":618},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":16}

6
tests/lean/interactive/my_tac_class.lean
View file

@ -18,9 +18,9 @@ t >> return ()
meta def rstep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit :=
λ v s, tactic_result.cases_on (@scope_trace _ line col (t v s))
(λ ⟨a, v⟩ new_s, tactic_result.success ((), v) new_s)
(λ msg_thunk e new_s,
let msg := msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
(tactic.report_error line col msg >> tactic.failed) new_s)
(λ opt_msg_thunk e new_s, match opt_msg_thunk with
| some msg_thunk := let msg := msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
(tactic.report_error line col msg >> tactic.silent_fail) new_s | none := tactic.silent_fail new_s end)
meta def execute (tac : mytac unit) : tactic unit :=
tac 0 >> return ()

6
tests/lean/interactive/rb_map_ts.lean
View file

@ -18,9 +18,9 @@ t >> return ()
meta def rstep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit :=
λ v s, tactic_result.cases_on (@scope_trace _ line col (t v s))
(λ ⟨a, v⟩ new_s, tactic_result.success ((), v) new_s)
(λ msg_thunk e new_s,
let msg := msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
(tactic.report_error line col msg >> tactic.failed) new_s)
(λ opt_msg_thunk e new_s, match opt_msg_thunk with
| some msg_thunk := let msg := msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
(tactic.report_error line col msg >> tactic.silent_fail) new_s | none := tactic.silent_fail new_s end)
meta def execute (tac : mytac unit) : tactic unit :=
tac (name_map.mk nat) >> return ()

1
tests/lean/minimize_errors.lean.expected.out
View file

@ -5,7 +5,6 @@ has type
but is expected to have type
ℕ → ℕ → ℕ
minimize_errors.lean:1:4: warning: declaration 'f' uses sorry
minimize_errors.lean:1:4: warning: declaration 'f.equations._eqn_1' uses sorry
f : ℕ → ℕ → ℕ
g : ℕ → ℕ → ℕ
def g : ℕ → ℕ → ℕ :=

12
tests/lean/nested_errors.lean.expected.out
View file

@ -4,15 +4,3 @@ a b c : ℕ,
a_1 : a = b,
a_2 : c = b
⊢ a = c
nested_errors.lean:7:2: error: failed
state:
a b c : ℕ,
a_1 : a = b,
a_2 : c = b
⊢ a = c
nested_errors.lean:8:0: error: failed
state:
a b c : ℕ,
a_1 : a = b,
a_2 : c = b
⊢ a = c

1
tests/lean/non_exhaustive_error.lean.expected.out
View file

@ -1,3 +1,2 @@
non_exhaustive_error.lean:2:11: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
non_exhaustive_error.lean:2:11: warning: declaration 'f' uses sorry
non_exhaustive_error.lean:2:11: warning: declaration 'f.equations._eqn_1' uses sorry

1
tests/lean/quot_bug.lean.expected.out
View file

@ -1,2 +1 @@
λ (x : A), f x
quot_bug.lean:8:8: warning: declaration '_example' uses sorry

2
tests/lean/run/774.lean
View file

@ -3,4 +3,4 @@ example : ℕ → ℕ → Prop
| 0 0 := true
| (succ n) 0 := false
| 0 (succ m) := false
| (succ n) (succ m) := this n m
| (succ n) (succ m) := _example n m

2
tests/lean/run/isabelle.lean
View file

@ -52,7 +52,7 @@ open lazy_list
meta def of_tactic {α : Type u} (t : tactic α) : lazy_tactic α :=
λ s, match t s with
| tactic_result.success a new_s := lazy_list.singleton (a, new_s)
| tactic_result.exception .α f e s := lazy_list.nil
| tactic_result.exception f e s := lazy_list.nil
end
meta instance {α : Type} : has_coe (tactic α) (lazy_tactic α) :=

10
tests/lean/run/my_tac_class.lean
View file

@ -18,9 +18,13 @@ t >> return ()
meta def rstep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit :=
λ v s, tactic_result.cases_on (@scope_trace _ line col (t v s))
(λ ⟨a, v⟩ new_s, tactic_result.success ((), v) new_s)
(λ msg_thunk e new_s,
let msg := msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
(tactic.report_error line col msg >> tactic.failed) new_s)
(λ opt_msg_thunk e new_s,
match opt_msg_thunk with
| some msg_thunk :=
let msg := msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
(tactic.report_error line col msg >> tactic.silent_fail) new_s
| none := tactic.silent_fail new_s
end)
meta def execute (tac : mytac unit) : tactic unit :=
tac 0 >> return ()

4
tests/lean/run/using_smt3.lean
View file

@ -7,8 +7,8 @@ open tactic_result
meta def fail_if_success {α : Type} (t : smt_tactic α) : smt_tactic unit :=
λ ss ts, match t ss ts with
| success _ _ := failed ts
| exception .(α × smt_state) _ _ _ := success ((), ss) ts
| success _ _ := failed ts
| exception _ _ _ := success ((), ss) ts
end
def my_smt_config : smt_config :=

1
tests/lean/set_attr1.lean.expected.out
View file

@ -3,4 +3,3 @@ state:
n : ℕ
⊢ f n = n + 1
set_attr1.lean:13:11: warning: declaration 'ex2' uses sorry
set_attr1.lean:13:11: warning: declaration 'ex2.equations._eqn_1' uses sorry

1
tests/lean/structure_instance_bug.lean.expected.out
View file

@ -1,3 +1,2 @@
structure_instance_bug.lean:11:0: error: invalid structure value {...}, field 'B' is implicit and must not be provided
structure_instance_bug.lean:10:11: warning: declaration 'foo3' uses sorry
structure_instance_bug.lean:10:11: warning: declaration 'foo3.equations._eqn_1' uses sorry

1
tests/lean/structure_instance_bug2.lean.expected.out
View file

@ -1,3 +1,2 @@
structure_instance_bug2.lean:4:0: error: invalid structure instance, 'default_smt_pre_config' is not the name of a structure type
structure_instance_bug2.lean:3:4: warning: declaration 'my_pre_config1' uses sorry
structure_instance_bug2.lean:3:4: warning: declaration 'my_pre_config1.equations._eqn_1' uses sorry

4
tests/lean/tactic_state_pp.lean
View file

@ -16,8 +16,8 @@ do t ← target,
meta def pp_state (s : tactic_state) : format :=
match pp_state_core s with
| tactic_result.success r _ := r
| tactic_result.exception .format _ _ _ := "failed to pretty print"
| tactic_result.success r _ := r
| tactic_result.exception _ _ _ := "failed to pretty print"
end
meta instance i2 : has_to_format tactic_state :=

7
tests/lean/vm_sorry.lean.expected.out
View file

@ -1,10 +1,5 @@
vm_sorry.lean:1:4: warning: declaration 'half_baked._main' uses sorry
vm_sorry.lean:1:4: warning: declaration 'half_baked._main.equations._eqn_1' uses sorry
vm_sorry.lean:1:4: warning: declaration 'half_baked.equations._eqn_1' uses sorry
vm_sorry.lean:1:4: warning: declaration 'half_baked' uses sorry
42
vm_sorry.lean:6:0: error: half_baked._main._val_1: trying to evaluate sorry
vm_sorry.lean:12:0: error: undefined
(some nat)
vm_sorry.lean:18:8: warning: declaration '_example' uses sorry
vm_sorry.lean:19:8: warning: declaration '_example' uses sorry
vm_sorry.lean:20:8: warning: declaration '_example' uses sorry