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

chore: show declaration with sorry in #eval

Browse source
This commit is contained in:
Gabriel Ebner 2022-01-17 21:04:03 +01:00 • committed by Leonardo de Moura
parent 03a5c5034f
commit ab276a5ae3
5 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/compiler/ir_interpreter.cpp
View file

@ -1047,8 +1047,9 @@ optional<name> get_sorry_dep(environment const & env, name const & n) {
}
object * run_boxed(environment const & env, options const & opts, name const & fn, unsigned n, object **args) {
if (get_sorry_dep(env, fn)) {
throw exception("cannot evaluate code because it uses 'sorry' and/or contains errors");
if (optional<name> decl_with_sorry = get_sorry_dep(env, fn)) {
throw exception(sstream() << "cannot evaluate code because '" << *decl_with_sorry
<< "' uses 'sorry' and/or contains errors");
}
return interpreter::with_interpreter<object *>(env, opts, fn, [&](interpreter & interp) { return interp.call_boxed(fn, n, args); });
}

2
tests/lean/277a.lean.expected.out
View file

@ -1,2 +1,2 @@
277a.lean:4:7-4:15: error: unknown identifier 'nonexistant'
277a.lean:4:0-4:25: error: cannot evaluate code because it uses 'sorry' and/or contains errors
277a.lean:4:0-4:25: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors

2
tests/lean/277b.lean.expected.out
View file

@ -1,3 +1,3 @@
277b.lean:8:10-8:16: error: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor
List Point
277b.lean:8:0-8:16: error: cannot evaluate code because it uses 'sorry' and/or contains errors
277b.lean:8:0-8:16: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors

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

@ -6,4 +6,4 @@ context:
x : Nat
⊢ Nat
f : Nat → Nat
440.lean:11:0-11:9: error: cannot evaluate code because it uses 'sorry' and/or contains errors
440.lean:11:0-11:9: error: cannot evaluate code because 'g' uses 'sorry' and/or contains errors

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

@ -7,5 +7,5 @@ has type
String : Type
but is expected to have type
Nat : Type
evalSorry.lean:7:0-7:15: error: cannot evaluate code because it uses 'sorry' and/or contains errors
evalSorry.lean:11:0-11:15: error: cannot evaluate code because it uses 'sorry' and/or contains errors
evalSorry.lean:7:0-7:15: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
evalSorry.lean:11:0-11:15: error: cannot evaluate code because 'h' uses 'sorry' and/or contains errors