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

feat: complain more verbosely

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-06-02 21:19:26 -04:00 • committed by Sebastian Ullrich
parent 7ca87e50ce
commit b7cd68a91e
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -827,7 +827,10 @@ private:
}
} else {
if (decl_tag(e.m_decl) == decl_kind::Extern) {
throw exception(sstream() << "could not find native implementation of external declaration '" << fn << "'");
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() << "')");
}
// evaluate args in old stack frame
for (const auto & arg : args) {