feat(library/init/lean/runtime): expose runtime limit

library/init/lean/default.lean

@@ -9,3 +9,4 @@ import init.lean.frontend
 import init.lean.extern
 import init.lean.environment
 import init.lean.modifiers
+import init.lean.runtime

library/init/lean/runtime.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.core
+
+namespace Lean
+
+@[extern "lean_closure_max_args"]
+constant closureMaxArgsFn : Unit → Nat := default _
+
+def closureMaxArgs : Nat :=
+closureMaxArgsFn ()
+
+end Lean

src/runtime/object.cpp

@@ -1953,6 +1953,13 @@ obj_res fixpoint6(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, o
     return r;
 }
 
+// =======================================
+// Runtime info
+
+extern "C" object * lean_closure_max_args(object *) {
+    return mk_nat_obj(static_cast<unsigned>(LEAN_CLOSURE_MAX_ARGS));
+}
+
 // =======================================
 // Debugging helper functions