feat(lua): improve error handling in Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/bindings/lua/justification.cpp

@@ -22,7 +22,7 @@ static int justification_tostring(lua_State * L) {
     if (jst) {
         formatter fmt  = get_global_formatter(L);
         options   opts = get_global_options(L);
-        out << mk_pair(jst.pp(fmt, opts, nullptr, false), opts);
+        out << mk_pair(jst.pp(fmt, opts), opts);
     } else {
         out << "<null-justification>";
     }

src/bindings/lua/util.cpp

@@ -6,8 +6,15 @@ Author: Leonardo de Moura
 */
 #include <lua.hpp>
 #include <string>
+#include <sstream>
+#include "kernel/kernel_exception.h"
+#include "library/elaborator/elaborator_exception.h"
 #include "bindings/lua/util.h"
 #include "bindings/lua/lua_exception.h"
+#include "bindings/lua/options.h"
+#include "bindings/lua/format.h"
+#include "bindings/lua/formatter.h"
+#include "bindings/lua/justification.h"
 
 namespace lean {
 /**
@@ -103,6 +110,15 @@ int safe_function_wrapper(lua_State * L, lua_CFunction f){
     char const * error_msg;
     try {
         return f(L);
+    } catch (kernel_exception & e) {
+        std::ostringstream out;
+        options o = get_global_options(L);
+        out << mk_pair(e.pp(get_global_formatter(L), o), o);
+        _error_msg = out.str();
+        error_msg  = _error_msg.c_str();
+    } catch (elaborator_exception & e) {
+        push_justification(L, e.get_justification());
+        lua_error(L);
     } catch (exception & e) {
         _error_msg = e.what();
         error_msg  = _error_msg.c_str();

src/library/elaborator/elaborator_exception.h

@@ -21,6 +21,4 @@ public:
     virtual char const * what() const noexcept { return "elaborator exception"; }
     justification const & get_justification() const { return m_justification; }
 };
-
-
 }

tests/lean/lua15.lean

@@ -0,0 +1,14 @@
+Variables i j : Int
+Variable p : Bool
+
+(**
+ local env = get_environment()
+ ok, jst = pcall(
+    function()
+       print(parse_lean("i + p"))
+ end)
+ assert(not ok)
+ assert(is_justification(jst))
+ assert(not jst:is_null())
+ print(jst:pp{display_children = false})
+**)

tests/lean/lua15.lean.expected.out

@@ -0,0 +1,7 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: i
+  Assumed: j
+  Assumed: p
+Failed to solve
+ ⊢ (?M::0 ≈ Nat::add) ⊕ (?M::0 ≈ Int::add) ⊕ (?M::0 ≈ Real::add)