From ab276a5ae3b60d70e4816ee7ec241423f45fb71c Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 17 Jan 2022 21:04:03 +0100 Subject: [PATCH] chore: show declaration with sorry in `#eval` --- src/library/compiler/ir_interpreter.cpp | 5 +++-- tests/lean/277a.lean.expected.out | 2 +- tests/lean/277b.lean.expected.out | 2 +- tests/lean/440.lean.expected.out | 2 +- tests/lean/evalSorry.lean.expected.out | 4 ++-- 5 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp index 3065373d0b..d4e6cdca3b 100644 --- a/src/library/compiler/ir_interpreter.cpp +++ b/src/library/compiler/ir_interpreter.cpp @@ -1047,8 +1047,9 @@ optional 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 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(env, opts, fn, [&](interpreter & interp) { return interp.call_boxed(fn, n, args); }); } diff --git a/tests/lean/277a.lean.expected.out b/tests/lean/277a.lean.expected.out index d6624f9adf..6e15b41861 100644 --- a/tests/lean/277a.lean.expected.out +++ b/tests/lean/277a.lean.expected.out @@ -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 diff --git a/tests/lean/277b.lean.expected.out b/tests/lean/277b.lean.expected.out index eacaf7afe1..3abe48b75b 100644 --- a/tests/lean/277b.lean.expected.out +++ b/tests/lean/277b.lean.expected.out @@ -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 diff --git a/tests/lean/440.lean.expected.out b/tests/lean/440.lean.expected.out index 83e710faac..20febf6cb4 100644 --- a/tests/lean/440.lean.expected.out +++ b/tests/lean/440.lean.expected.out @@ -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 diff --git a/tests/lean/evalSorry.lean.expected.out b/tests/lean/evalSorry.lean.expected.out index 1fe725f310..984c2973ca 100644 --- a/tests/lean/evalSorry.lean.expected.out +++ b/tests/lean/evalSorry.lean.expected.out @@ -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