diff --git a/src/bindings/lua/context.cpp b/src/bindings/lua/context.cpp
index 0510649301..56a818594d 100644
--- a/src/bindings/lua/context.cpp
+++ b/src/bindings/lua/context.cpp
@@ -114,7 +114,7 @@ static int context_pred(lua_State * L) {
 static int context_extend(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs != 3 && nargs != 4)
-        luaL_error(L, "extend expect 3 or 4 arguments");
+        throw exception("extend expect 3 or 4 arguments");
     return mk_context(L);
 }
 
diff --git a/src/bindings/lua/environment.cpp b/src/bindings/lua/environment.cpp
index 95e86498d8..598c39d4ca 100644
--- a/src/bindings/lua/environment.cpp
+++ b/src/bindings/lua/environment.cpp
@@ -173,7 +173,7 @@ int get_environment(lua_State * L) {
     lua_pushlightuserdata(L, static_cast<void *>(&g_set_environment_key));
     lua_gettable(L, LUA_REGISTRYINDEX);
     if (!is_environment(L, -1))
-        luaL_error(L, "Lua registry does not contain a Lean environment");
+        throw exception("Lua registry does not contain a Lean environment");
     return push_environment(L, to_environment(L, -1));
 }
 
diff --git a/src/bindings/lua/expr.cpp b/src/bindings/lua/expr.cpp
index 0bf21c56a8..2bb6fe652d 100644
--- a/src/bindings/lua/expr.cpp
+++ b/src/bindings/lua/expr.cpp
@@ -32,7 +32,7 @@ expr & to_expr(lua_State * L, int idx) {
 expr & to_nonnull_expr(lua_State * L, int idx) {
     expr & r = to_expr(L, idx);
     if (!r)
-        luaL_error(L, "non-null Lean expression expected");
+        throw exception("non-null Lean expression expected");
     return r;
 }
 
@@ -83,7 +83,7 @@ static int expr_mk_var(lua_State * L) {
 static int expr_mk_app(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs < 2)
-        luaL_error(L, "application must have at least two arguments");
+        throw exception("application must have at least two arguments");
     buffer<expr> args;
     for (int i = 1; i <= nargs; i++)
         args.push_back(to_nonnull_expr(L, i));
@@ -126,7 +126,7 @@ static std::pair<expr, expr> get_expr_pair_from_table(lua_State * L, int t, int
     lua_pushinteger(L, i);
     lua_gettable(L, -2); // now table {ai, bi} is on the top
     if (!lua_istable(L, -1) || objlen(L, -1) != 2)
-        luaL_error(L, "arg #1 must be of the form '{{expr, expr}, ...}'");
+        throw exception("arg #1 must be of the form '{{expr, expr}, ...}'");
     expr ai = get_expr_from_table(L, -1, 1);
     expr bi = get_expr_from_table(L, -1, 2);
     lua_pop(L, 2); // pop table {ai, bi} and t from stack
@@ -137,16 +137,16 @@ typedef expr (*MkAbst1)(expr const & n, expr const & t, expr const & b);
 typedef expr (*MkAbst2)(name const & n, expr const & t, expr const & b);
 
 template<MkAbst1 F1, MkAbst2 F2>
-int expr_abst(lua_State * L, char const * fname) {
+int expr_abst(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs < 2)
-        luaL_error(L, "Lean %s must have at least 2 arguments", fname);
+        throw exception("function must have at least 2 arguments");
     if (nargs == 2) {
         if (!lua_istable(L, 1))
-            luaL_error(L, "Lean %s expects arg #1 to be of the form '{{expr, expr}, ...}'", fname);
+            throw exception("function expects arg #1 to be of the form '{{expr, expr}, ...}'");
         int len = objlen(L, 1);
         if (len == 0)
-            luaL_error(L, "Lean %s expects arg #1 to be a non-empty table", fname);
+            throw exception("function expects arg #1 to be a non-empty table");
         expr r = to_nonnull_expr(L, 2);
         for (int i = len; i >= 1; i--) {
             auto p = get_expr_pair_from_table(L, 1, i);
@@ -155,7 +155,7 @@ int expr_abst(lua_State * L, char const * fname) {
         return push_expr(L, r);
     } else {
         if (nargs % 2 == 0)
-            luaL_error(L, "Lean %s must have an odd number of arguments", fname);
+            throw exception("function must have an odd number of arguments");
         expr r = to_nonnull_expr(L, nargs);
         for (int i = nargs - 1; i >= 1; i-=2) {
             if (is_expr(L, i - 1))
@@ -167,9 +167,9 @@ int expr_abst(lua_State * L, char const * fname) {
     }
 }
 
-static int expr_fun(lua_State * L) { return expr_abst<Fun, Fun>(L, "fun"); }
-static int expr_pi(lua_State * L)  { return expr_abst<Pi, Pi>(L, "Pi"); }
-static int expr_let(lua_State * L) { return expr_abst<Let, Let>(L, "Let"); }
+static int expr_fun(lua_State * L) { return expr_abst<Fun, Fun>(L); }
+static int expr_pi(lua_State * L)  { return expr_abst<Pi, Pi>(L); }
+static int expr_let(lua_State * L) { return expr_abst<Let, Let>(L); }
 
 static int expr_type(lua_State * L) {
     int nargs = lua_gettop(L);
diff --git a/src/bindings/lua/format.cpp b/src/bindings/lua/format.cpp
index d4cd3d4108..c5966dffc7 100644
--- a/src/bindings/lua/format.cpp
+++ b/src/bindings/lua/format.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <lua.hpp>
 #include <cstring>
 #include "util/debug.h"
+#include "util/sstream.h"
 #include "util/sexpr/format.h"
 #include "bindings/lua/util.h"
 #include "bindings/lua/name.h"
@@ -103,7 +104,7 @@ static int format_highlight(lua_State * L) {
     } else if (strcmp(color_str, "grey") == 0) {
         color = format::GREY;
     } else {
-        return luaL_error(L, "unknown color '%s'", color_str);
+        throw exception(sstream() << "unknown color '" << color_str << "'");
     }
     return push_format(L, highlight(to_format(L, 1), color));
 }
diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp
index fa4e5adc22..ccb874ba04 100644
--- a/src/bindings/lua/leanlua_state.cpp
+++ b/src/bindings/lua/leanlua_state.cpp
@@ -159,7 +159,7 @@ static int print(lua_State * L) {
         lua_call(L, 1, 1);
         s = lua_tolstring(L, -1, &l);
         if (s == NULL)
-            return luaL_error(L, "'to_string' must return a string to 'print'");
+            throw exception("'to_string' must return a string to 'print'");
         if (i > 1) {
             std::cout << "\t";
         }
diff --git a/src/bindings/lua/level.cpp b/src/bindings/lua/level.cpp
index eeb4a87b3c..ca3d043791 100644
--- a/src/bindings/lua/level.cpp
+++ b/src/bindings/lua/level.cpp
@@ -96,33 +96,33 @@ static int level_is_max(lua_State * L) {
 
 static int level_name(lua_State * L) {
     if (!is_uvar(to_level(L, 1)))
-        luaL_error(L, "arg #1 must be a Lean level universal variable");
+        throw exception("arg #1 must be a Lean level universal variable");
     return push_name(L, uvar_name(to_level(L, 1)));
 }
 
 static int level_lift_of(lua_State * L) {
     if (!is_lift(to_level(L, 1)))
-        luaL_error(L, "arg #1 must be a Lean level lift");
+        throw exception("arg #1 must be a Lean level lift");
     return push_level(L, lift_of(to_level(L, 1)));
 }
 
 static int level_lift_offset(lua_State * L) {
     if (!is_lift(to_level(L, 1)))
-        luaL_error(L, "arg #1 must be a Lean level lift");
+        throw exception("arg #1 must be a Lean level lift");
     lua_pushinteger(L, lift_offset(to_level(L, 1)));
     return 1;
 }
 
 static int level_max_size(lua_State * L) {
     if (!is_max(to_level(L, 1)))
-        luaL_error(L, "arg #1 must be a Lean level max");
+        throw exception("arg #1 must be a Lean level max");
     lua_pushinteger(L, max_size(to_level(L, 1)));
     return 1;
 }
 
 static int level_max_level(lua_State * L) {
     if (!is_max(to_level(L, 1)))
-        luaL_error(L, "arg #1 must be a Lean level max");
+        throw exception("arg #1 must be a Lean level max");
     return push_level(L, max_level(to_level(L, 1), luaL_checkinteger(L, 2)));
 }
 
diff --git a/src/bindings/lua/local_context.cpp b/src/bindings/lua/local_context.cpp
index 08d54a8f5a..3dc01c6c52 100644
--- a/src/bindings/lua/local_context.cpp
+++ b/src/bindings/lua/local_context.cpp
@@ -71,7 +71,7 @@ static int local_entry_s(lua_State * L) {
 static int local_entry_n(lua_State * L) {
     local_entry & e = to_local_entry(L, 1);
     if (!e.is_lift())
-        luaL_error(L, "Lean lift local entry expected");
+        throw exception("Lean lift local entry expected");
     lua_pushinteger(L, to_local_entry(L, 1).n());
     return 1;
 }
@@ -79,7 +79,7 @@ static int local_entry_n(lua_State * L) {
 static int local_entry_v(lua_State * L) {
     local_entry & e = to_local_entry(L, 1);
     if (!e.is_inst())
-        luaL_error(L, "Lean inst local entry expected");
+        throw exception("Lean inst local entry expected");
     return push_expr(L, to_local_entry(L, 1).v());
     return 1;
 }
diff --git a/src/bindings/lua/numerics.cpp b/src/bindings/lua/numerics.cpp
index 94af591e48..7a61552347 100644
--- a/src/bindings/lua/numerics.cpp
+++ b/src/bindings/lua/numerics.cpp
@@ -83,7 +83,7 @@ static int mpz_mul(lua_State * L) {
 
 static int mpz_div(lua_State * L) {
     mpz const & arg2 = to_mpz<2>(L);
-    if (arg2 == 0) luaL_error(L, "division by zero");
+    if (arg2 == 0) throw exception("division by zero");
     return push_mpz(L, to_mpz<1>(L) / arg2);
 }
 
@@ -93,7 +93,7 @@ static int mpz_umn(lua_State * L) {
 
 static int mpz_power(lua_State * L) {
     int k = luaL_checkinteger(L, 2);
-    if (k < 0) luaL_error(L, "argument #2 must be positive");
+    if (k < 0) throw exception("argument #2 must be positive");
     return push_mpz(L, pow(to_mpz<1>(L), k));
 }
 
@@ -200,7 +200,7 @@ static int mpq_mul(lua_State * L) {
 
 static int mpq_div(lua_State * L) {
     mpq const & arg2 = to_mpq<2>(L);
-    if (arg2 == 0) luaL_error(L, "division by zero");
+    if (arg2 == 0) throw exception("division by zero");
     return push_mpq(L, to_mpq<1>(L) / arg2);
 }
 
@@ -210,7 +210,7 @@ static int mpq_umn(lua_State * L) {
 
 static int mpq_power(lua_State * L) {
     int k = luaL_checkinteger(L, 2);
-    if (k < 0) luaL_error(L, "argument #2 must be positive");
+    if (k < 0) throw exception("argument #2 must be positive");
     return push_mpq(L, pow(to_mpq<1>(L), k));
 }
 
diff --git a/src/bindings/lua/options.cpp b/src/bindings/lua/options.cpp
index eb91113649..999fcd5023 100644
--- a/src/bindings/lua/options.cpp
+++ b/src/bindings/lua/options.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <lua.hpp>
 #include "util/debug.h"
 #include "util/name.h"
+#include "util/sstream.h"
 #include "util/sexpr/options.h"
 #include "util/sexpr/option_declarations.h"
 #include "bindings/lua/util.h"
@@ -133,7 +134,7 @@ static int options_get(lua_State * L) {
     name k = to_key(L, 2);
     auto it = get_option_declarations().find(k);
     if (it == get_option_declarations().end()) {
-        return luaL_error(L, "unknown option '%s'", k.to_string().c_str());
+        throw exception(sstream() << "unknown option '" << k.to_string().c_str() << "'");
     } else {
         option_declaration const & d = it->second;
         switch (d.kind()) {
@@ -142,7 +143,7 @@ static int options_get(lua_State * L) {
         case UnsignedOption:  return options_get_unsigned(L);
         case DoubleOption:    return options_get_double(L);
         case StringOption:    return options_get_string(L);
-        default:              return luaL_error(L, "unsupported option kind for '%s'", k.to_string().c_str());
+        default:              throw exception(sstream() << "unsupported option kind for '" << k.to_string().c_str() << "'");
         }
     }
 }
@@ -151,7 +152,7 @@ static int options_update(lua_State * L) {
     name k = to_key(L, 2);
     auto it = get_option_declarations().find(k);
     if (it == get_option_declarations().end()) {
-        return luaL_error(L, "unknown option '%s'", k.to_string().c_str());
+        throw exception(sstream() << "unknown option '" << k.to_string().c_str() << "'");
     } else {
         option_declaration const & d = it->second;
         switch (d.kind()) {
@@ -160,7 +161,7 @@ static int options_update(lua_State * L) {
         case UnsignedOption:  return options_update_unsigned(L);
         case DoubleOption:    return options_update_double(L);
         case StringOption:    return options_update_string(L);
-        default:              return luaL_error(L, "unsupported option kind for '%s'", k.to_string().c_str());
+        default:              throw exception(sstream() << "unsupported option kind for '" << k.to_string().c_str() << "'");
         }
     }
 }
diff --git a/src/bindings/lua/sexpr.cpp b/src/bindings/lua/sexpr.cpp
index 71989bf2e7..65c6032def 100644
--- a/src/bindings/lua/sexpr.cpp
+++ b/src/bindings/lua/sexpr.cpp
@@ -97,7 +97,7 @@ static int sexpr_is_mpq(lua_State * L)    { lua_pushboolean(L, is_mpq(to_sexpr(L
 static int sexpr_length(lua_State * L) {
     sexpr const & e = to_sexpr(L, 1);
     if (!is_list(e))
-        return luaL_error(L, "s-expression is not a list");
+        throw exception("s-expression is not a list");
     lua_pushinteger(L, length(e));
     return 1;
 }
@@ -105,21 +105,21 @@ static int sexpr_length(lua_State * L) {
 static int sexpr_head(lua_State * L) {
     sexpr const & e = to_sexpr(L, 1);
     if (!is_cons(e))
-        return luaL_error(L, "s-expression is not a cons cell");
+        throw exception("s-expression is not a cons cell");
     return push_sexpr(L, head(e));
 }
 
 static int sexpr_tail(lua_State * L) {
     sexpr const & e = to_sexpr(L, 1);
     if (!is_cons(e))
-        return luaL_error(L, "s-expression is not a cons cell");
+        throw exception("s-expression is not a cons cell");
     return push_sexpr(L, tail(e));
 }
 
 static int sexpr_to_bool(lua_State * L) {
     sexpr const & e = to_sexpr(L, 1);
     if (!is_bool(e))
-        return luaL_error(L, "s-expression is not a Boolean");
+        throw exception("s-expression is not a Boolean");
     lua_pushboolean(L, to_bool(e));
     return 1;
 }
@@ -127,7 +127,7 @@ static int sexpr_to_bool(lua_State * L) {
 static int sexpr_to_string(lua_State * L) {
     sexpr const & e = to_sexpr(L, 1);
     if (!is_string(e))
-        return luaL_error(L, "s-expression is not a string");
+        throw exception("s-expression is not a string");
     lua_pushfstring(L, to_string(e).c_str());
     return 1;
 }
@@ -135,7 +135,7 @@ static int sexpr_to_string(lua_State * L) {
 static int sexpr_to_int(lua_State * L) {
     sexpr const & e = to_sexpr(L, 1);
     if (!is_int(e))
-        return luaL_error(L, "s-expression is not an integer");
+        throw exception("s-expression is not an integer");
     lua_pushinteger(L, to_int(e));
     return 1;
 }
@@ -143,7 +143,7 @@ static int sexpr_to_int(lua_State * L) {
 static int sexpr_to_double(lua_State * L) {
     sexpr const & e = to_sexpr(L, 1);
     if (!is_double(e))
-        return luaL_error(L, "s-expression is not a double");
+        throw exception("s-expression is not a double");
     lua_pushnumber(L, to_double(e));
     return 1;
 }
@@ -151,21 +151,21 @@ static int sexpr_to_double(lua_State * L) {
 static int sexpr_to_name(lua_State * L) {
     sexpr const & e = to_sexpr(L, 1);
     if (!is_name(e))
-        return luaL_error(L, "s-expression is not a name");
+        throw exception("s-expression is not a name");
     return push_name(L, to_name(e));
 }
 
 static int sexpr_to_mpz(lua_State * L) {
     sexpr const & e = to_sexpr(L, 1);
     if (!is_mpz(e))
-        return luaL_error(L, "s-expression is not a multi-precision integer");
+        throw exception("s-expression is not a multi-precision integer");
     return push_mpz(L, to_mpz(e));
 }
 
 static int sexpr_to_mpq(lua_State * L) {
     sexpr const & e = to_sexpr(L, 1);
     if (!is_mpq(e))
-        return luaL_error(L, "s-expression is not a multi-precision rational");
+        throw exception("s-expression is not a multi-precision rational");
     return push_mpq(L, to_mpq(e));
 }
 
diff --git a/tests/lua/expr5.lua b/tests/lua/expr5.lua
index d52bb8536f..e8342baa4a 100644
--- a/tests/lua/expr5.lua
+++ b/tests/lua/expr5.lua
@@ -15,8 +15,3 @@ check_error(function() Pi({{"x"}}, Const("x")) end)
 check_error(function() Pi(Const("x")) end)
 check_error(function() Pi(Const("x"), Const("N"), Const("x"), Const("a")) end)
 check_error(function() Pi({}, Const("x")) end)
-
-
-
-
-