From f1b274279bf841c7bf3a1d32cea5f3a4591a44d4 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 21 Nov 2023 20:31:26 +1100 Subject: [PATCH] feat: helpful error message about supportInterpreter (#2912) Following [@Kha's suggestion](https://github.com/leanprover/lean4/issues/2897#issuecomment-1816043031) from #2897. --------- Co-authored-by: Mario Carneiro --- src/library/compiler/ir_interpreter.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp index d684373409..a25a9c65ac 100644 --- a/src/library/compiler/ir_interpreter.cpp +++ b/src/library/compiler/ir_interpreter.cpp @@ -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) {