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

feat: helpful error message about supportInterpreter (#2912)

Browse source 
Following [@Kha's
suggestion](https://github.com/leanprover/lean4/issues/2897#issuecomment-1816043031)
from #2897.

---------

Co-authored-by: Mario Carneiro <di.gama@gmail.com>
This commit is contained in:
Scott Morrison 2023-11-21 20:31:26 +11:00 • committed by GitHub
parent 6a33afb745
commit f1b274279b
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -865,8 +865,10 @@ private:
if (decl_tag(e.m_decl) == decl_kind::Extern) {
string_ref mangled = name_mangle(fn, *g_mangle_prefix);
string_ref boxed_mangled(string_append(mangled.to_obj_arg(), g_boxed_mangled_suffix->raw()));
throw exception(sstream() << "could not find native implementation of external declaration '" << fn
<< "' (symbols '" << boxed_mangled.data() << "' or '" << mangled.data() << "')");
throw exception(sstream() << "Could not find native implementation of external declaration '" << fn
<< "' (symbols '" << boxed_mangled.data() << "' or '" << mangled.data() << "').\n"
<< "For declarations from `Init` or `Lean`, you need to set `supportInterpreter := true` "
<< "in the relevant `lean_exe` statement in your `lakefile.lean`.");
}
// evaluate args in old stack frame
for (const auto & arg : args) {