feat: add set_option debug.skipKernelTC true

The new option `set_option debug.skipKernelTC true` is meant for
temporarily working around kernel performance issues.
It compromises soundness because a buggy tactic may produce an invalid
proof, and the kernel will not catch it if the new option is set to true.

src/Lean/AddDecl.lean

@@ -8,8 +8,17 @@ import Lean.CoreM
 
 namespace Lean
 
+register_builtin_option debug.skipKernelTC : Bool := {
+  defValue := false
+  group    := "debug"
+  descr    := "skip kernel type checker. WARNING: setting this option to true may compromise soundness because your proofs will not be checked by the Lean kernel"
+}
+
 def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment :=
-  addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl
+  if debug.skipKernelTC.get opts then
+    addDeclWithoutChecking env decl
+  else
+    addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl
 
 def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment := do
   let env ← addDecl env opts decl

src/Lean/Environment.lean

@@ -244,10 +244,21 @@ inductive KernelException where
 
 namespace Environment
 
-/-- Type check given declaration and add it to the environment -/
+/--
+Type check given declaration and add it to the environment
+-/
 @[extern "lean_add_decl"]
 opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration) : Except KernelException Environment
 
+/--
+Add declaration to kernel without type checking it.
+**WARNING** This function is meant for temporarily working around kernel performance issues.
+It compromises soundness because, for example, a buggy tactic may produce an invalid proof,
+and the kernel will not catch it if the new option is set to true.
+-/
+@[extern "lean_add_decl_without_checking"]
+opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) : Except KernelException Environment
+
 end Environment
 
 namespace ConstantInfo

src/kernel/environment.cpp

@@ -299,6 +299,12 @@ extern "C" LEAN_EXPORT object * lean_add_decl(object * env, size_t max_heartbeat
         });
 }
 
+extern "C" LEAN_EXPORT object * lean_add_decl_without_checking(object * env, object * decl) {
+    return catch_kernel_exceptions<environment>([&]() {
+            return environment(env).add(declaration(decl, true), false);
+        });
+}
+
 void environment::for_each_constant(std::function<void(constant_info const & d)> const & f) const {
     smap_foreach(cnstr_get(raw(), 1), [&](object *, object * v) {
             constant_info cinfo(v, true);