From 3dcb579c8f431fca8fca8f965c5d18cf6e865591 Mon Sep 17 00:00:00 2001
From: mt0-svg <311859884+mt0-svg@users.noreply.github.com>
Date: Thu, 1 Oct 2026 11:53:51 +0200
Subject: [PATCH] Add a lean_kernel option to skip the builtin kernel replay

With "lean_kernel": false in the config, comparator does not replay the
solution in the Lean kernel and leaves the replay to the external kernels.
The statement comparison, the axiom check and the external kernels are
unchanged. The default is true, so existing configs behave as before. A
config with lean_kernel false and no external kernel is rejected at
startup, so a solution never passes without a kernel replay.

Tests: lean_kernel_off_nanoda (accepted), lean_kernel_off_mismatch (wrong
statement, rejected), lean_kernel_off_unchecked (a theorem added with
debug.skipKernelTC whose value does not prove its type, rejected by nanoda)
and lean_kernel_off_no_kernel (refused at startup).
---
 Main.lean                                           | 13 ++++++++++++-
 README.md                                           |  6 ++++++
 .../lean_kernel_off_mismatch/Challenge.lean         |  2 ++
 .../projects/lean_kernel_off_mismatch/Solution.lean |  1 +
 tests/projects/lean_kernel_off_mismatch/config.json |  8 ++++++++
 tests/projects/lean_kernel_off_mismatch/test.json   |  3 +++
 .../projects/lean_kernel_off_nanoda/Challenge.lean  |  2 ++
 tests/projects/lean_kernel_off_nanoda/Solution.lean |  2 ++
 tests/projects/lean_kernel_off_nanoda/config.json   |  8 ++++++++
 tests/projects/lean_kernel_off_nanoda/test.json     |  3 +++
 .../lean_kernel_off_no_kernel/Challenge.lean        |  2 ++
 .../lean_kernel_off_no_kernel/Solution.lean         |  2 ++
 .../projects/lean_kernel_off_no_kernel/config.json  |  7 +++++++
 tests/projects/lean_kernel_off_no_kernel/test.json  |  3 +++
 .../lean_kernel_off_unchecked/Challenge.lean        |  2 ++
 .../lean_kernel_off_unchecked/Solution.lean         | 13 +++++++++++++
 .../projects/lean_kernel_off_unchecked/config.json  |  8 ++++++++
 tests/projects/lean_kernel_off_unchecked/test.json  |  3 +++
 18 files changed, 87 insertions(+), 1 deletion(-)
 create mode 100644 tests/projects/lean_kernel_off_mismatch/Challenge.lean
 create mode 100644 tests/projects/lean_kernel_off_mismatch/Solution.lean
 create mode 100644 tests/projects/lean_kernel_off_mismatch/config.json
 create mode 100644 tests/projects/lean_kernel_off_mismatch/test.json
 create mode 100644 tests/projects/lean_kernel_off_nanoda/Challenge.lean
 create mode 100644 tests/projects/lean_kernel_off_nanoda/Solution.lean
 create mode 100644 tests/projects/lean_kernel_off_nanoda/config.json
 create mode 100644 tests/projects/lean_kernel_off_nanoda/test.json
 create mode 100644 tests/projects/lean_kernel_off_no_kernel/Challenge.lean
 create mode 100644 tests/projects/lean_kernel_off_no_kernel/Solution.lean
 create mode 100644 tests/projects/lean_kernel_off_no_kernel/config.json
 create mode 100644 tests/projects/lean_kernel_off_no_kernel/test.json
 create mode 100644 tests/projects/lean_kernel_off_unchecked/Challenge.lean
 create mode 100644 tests/projects/lean_kernel_off_unchecked/Solution.lean
 create mode 100644 tests/projects/lean_kernel_off_unchecked/config.json
 create mode 100644 tests/projects/lean_kernel_off_unchecked/test.json

diff --git a/Main.lean b/Main.lean
index 8560511..232d1cf 100644
--- a/Main.lean
+++ b/Main.lean
@@ -21,6 +21,7 @@ structure Context where
   whichLandrun : String
   whichLean4Export : String
   externalKernels : (Std.TreeMap String (Array String))
+  leanKernel : Bool
 
 abbrev M := ReaderT Context IO
 
@@ -36,6 +37,9 @@ structure LandrunArgs where
 @[inline]
 def getExternalKernels : M (Std.TreeMap String (Array String)) := do return (← read).externalKernels
 
+@[inline]
+def getLeanKernel : M Bool := do return (← read).leanKernel
+
 @[inline]
 def getTheoremNames : M (Array Lean.Name) := do return (← read).theoremNames
 
@@ -297,7 +301,8 @@ def verifyMatch (challengeExport : String) (solutionExport : String) :
   let mut result := none
   for (kernelName, kernelCommand) in ← getExternalKernels do
     result := result <|> (← runExternalKernel kernelName kernelCommand solutionExport)
-  result := result <|> (← runBuiltinKernel solution)
+  if ← getLeanKernel then
+    result := result <|> (← runBuiltinKernel solution)
   if let some error := result then
     throw <| IO.userError error
 
@@ -325,6 +330,7 @@ structure Config where
   permitted_axioms : Array String
   enable_nanoda? : Option Bool
   external_kernels? : Option (Std.TreeMap String (Array String))
+  lean_kernel? : Option Bool
   deriving Lean.FromJson, Lean.ToJson, Repr
 
 def M.run (x : M α) (cfg : Config) : IO α := do
@@ -350,6 +356,10 @@ def M.run (x : M α) (cfg : Config) : IO α := do
   else if let some nanodaOverride := nanodaOverride? then
     externalKernels := externalKernels.modify "nanoda" fun cmd => cmd.set! 0 nanodaOverride
 
+  let leanKernel := cfg.lean_kernel?.getD true
+  if !leanKernel && externalKernels.isEmpty then
+    throw <| .userError "lean_kernel is false and no external kernel is set: nothing would check the solution."
+
   ReaderT.run x {
     projectDir := cwd
     challengeModule := cfg.challenge_module.toName,
@@ -362,6 +372,7 @@ def M.run (x : M α) (cfg : Config) : IO α := do
     whichLean4Export := whichLean4Export,
     whichLandrun := whichLandrun,
     externalKernels := externalKernels
+    leanKernel := leanKernel
   }
 
 end Comparator
diff --git a/README.md b/README.md
index e1d67f6..77bdeb7 100644
--- a/README.md
+++ b/README.md
@@ -85,6 +85,12 @@ moves toward having an option to receive the input file as a `CLI` argument.
 
 For development purposes, comparator supports overriding `nanoda` specifically using the
 `COMPARATOR_NANODA` environment variable.
+
+Setting `lean_kernel: false` skips the replay of the solution in the Lean kernel inside comparator
+and leaves the check of the proofs to the external kernels; it is an error when no external kernel
+is set. The statement comparison and the axiom check run as before. This is meant for solutions
+whose build has already run the Lean kernel on every declaration and which are large enough that a
+second replay matters.
 ## Definition Holes
 Sometimes challenges want to leave open definitions for solutions to fill in. This can range from
 simple things like filling in a `Prop` valued definition to resolve whether a conjecture is true or
diff --git a/tests/projects/lean_kernel_off_mismatch/Challenge.lean b/tests/projects/lean_kernel_off_mismatch/Challenge.lean
new file mode 100644
index 0000000..b45c299
--- /dev/null
+++ b/tests/projects/lean_kernel_off_mismatch/Challenge.lean
@@ -0,0 +1,2 @@
+theorem comm (n m : Nat) : n + m = m + n := by
+  sorry
diff --git a/tests/projects/lean_kernel_off_mismatch/Solution.lean b/tests/projects/lean_kernel_off_mismatch/Solution.lean
new file mode 100644
index 0000000..05d869d
--- /dev/null
+++ b/tests/projects/lean_kernel_off_mismatch/Solution.lean
@@ -0,0 +1 @@
+axiom comm (n m : Nat) : m + m = m + m
diff --git a/tests/projects/lean_kernel_off_mismatch/config.json b/tests/projects/lean_kernel_off_mismatch/config.json
new file mode 100644
index 0000000..a5932f0
--- /dev/null
+++ b/tests/projects/lean_kernel_off_mismatch/config.json
@@ -0,0 +1,8 @@
+{
+    "challenge_module": "Challenge",
+    "solution_module": "Solution",
+    "theorem_names": ["comm"],
+    "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
+    "enable_nanoda": true,
+    "lean_kernel": false
+}
diff --git a/tests/projects/lean_kernel_off_mismatch/test.json b/tests/projects/lean_kernel_off_mismatch/test.json
new file mode 100644
index 0000000..fe08d6a
--- /dev/null
+++ b/tests/projects/lean_kernel_off_mismatch/test.json
@@ -0,0 +1,3 @@
+{
+        "exit_code": 1
+}
diff --git a/tests/projects/lean_kernel_off_nanoda/Challenge.lean b/tests/projects/lean_kernel_off_nanoda/Challenge.lean
new file mode 100644
index 0000000..b45c299
--- /dev/null
+++ b/tests/projects/lean_kernel_off_nanoda/Challenge.lean
@@ -0,0 +1,2 @@
+theorem comm (n m : Nat) : n + m = m + n := by
+  sorry
diff --git a/tests/projects/lean_kernel_off_nanoda/Solution.lean b/tests/projects/lean_kernel_off_nanoda/Solution.lean
new file mode 100644
index 0000000..bd29d73
--- /dev/null
+++ b/tests/projects/lean_kernel_off_nanoda/Solution.lean
@@ -0,0 +1,2 @@
+theorem comm (n m : Nat) : n + m = m + n := by
+  grind
diff --git a/tests/projects/lean_kernel_off_nanoda/config.json b/tests/projects/lean_kernel_off_nanoda/config.json
new file mode 100644
index 0000000..a5932f0
--- /dev/null
+++ b/tests/projects/lean_kernel_off_nanoda/config.json
@@ -0,0 +1,8 @@
+{
+    "challenge_module": "Challenge",
+    "solution_module": "Solution",
+    "theorem_names": ["comm"],
+    "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
+    "enable_nanoda": true,
+    "lean_kernel": false
+}
diff --git a/tests/projects/lean_kernel_off_nanoda/test.json b/tests/projects/lean_kernel_off_nanoda/test.json
new file mode 100644
index 0000000..5d4bf27
--- /dev/null
+++ b/tests/projects/lean_kernel_off_nanoda/test.json
@@ -0,0 +1,3 @@
+{
+        "exit_code": 0
+}
diff --git a/tests/projects/lean_kernel_off_no_kernel/Challenge.lean b/tests/projects/lean_kernel_off_no_kernel/Challenge.lean
new file mode 100644
index 0000000..b45c299
--- /dev/null
+++ b/tests/projects/lean_kernel_off_no_kernel/Challenge.lean
@@ -0,0 +1,2 @@
+theorem comm (n m : Nat) : n + m = m + n := by
+  sorry
diff --git a/tests/projects/lean_kernel_off_no_kernel/Solution.lean b/tests/projects/lean_kernel_off_no_kernel/Solution.lean
new file mode 100644
index 0000000..bd29d73
--- /dev/null
+++ b/tests/projects/lean_kernel_off_no_kernel/Solution.lean
@@ -0,0 +1,2 @@
+theorem comm (n m : Nat) : n + m = m + n := by
+  grind
diff --git a/tests/projects/lean_kernel_off_no_kernel/config.json b/tests/projects/lean_kernel_off_no_kernel/config.json
new file mode 100644
index 0000000..57c1035
--- /dev/null
+++ b/tests/projects/lean_kernel_off_no_kernel/config.json
@@ -0,0 +1,7 @@
+{
+    "challenge_module": "Challenge",
+    "solution_module": "Solution",
+    "theorem_names": ["comm"],
+    "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
+    "lean_kernel": false
+}
diff --git a/tests/projects/lean_kernel_off_no_kernel/test.json b/tests/projects/lean_kernel_off_no_kernel/test.json
new file mode 100644
index 0000000..fe08d6a
--- /dev/null
+++ b/tests/projects/lean_kernel_off_no_kernel/test.json
@@ -0,0 +1,3 @@
+{
+        "exit_code": 1
+}
diff --git a/tests/projects/lean_kernel_off_unchecked/Challenge.lean b/tests/projects/lean_kernel_off_unchecked/Challenge.lean
new file mode 100644
index 0000000..c98302a
--- /dev/null
+++ b/tests/projects/lean_kernel_off_unchecked/Challenge.lean
@@ -0,0 +1,2 @@
+theorem zero_eq_one : (0 : Nat) = 1 := by
+  sorry
diff --git a/tests/projects/lean_kernel_off_unchecked/Solution.lean b/tests/projects/lean_kernel_off_unchecked/Solution.lean
new file mode 100644
index 0000000..bba7021
--- /dev/null
+++ b/tests/projects/lean_kernel_off_unchecked/Solution.lean
@@ -0,0 +1,13 @@
+import Lean
+
+open Lean Elab Term Meta
+
+-- A theorem whose value proves `0 = 0`, added without the kernel check: only a replay can reject it.
+run_elab
+  withOptions (fun o => o.setBool `debug.skipKernelTC true) <|
+    addDecl <| .thmDecl {
+      name        := `zero_eq_one
+      levelParams := []
+      type        := mkApp3 (.const ``Eq [1]) (.const ``Nat []) (mkNatLit 0) (mkNatLit 1)
+      value       := mkApp2 (.const ``Eq.refl [1]) (.const ``Nat []) (mkNatLit 0)
+    }
diff --git a/tests/projects/lean_kernel_off_unchecked/config.json b/tests/projects/lean_kernel_off_unchecked/config.json
new file mode 100644
index 0000000..a733cd7
--- /dev/null
+++ b/tests/projects/lean_kernel_off_unchecked/config.json
@@ -0,0 +1,8 @@
+{
+    "challenge_module": "Challenge",
+    "solution_module": "Solution",
+    "theorem_names": ["zero_eq_one"],
+    "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
+    "enable_nanoda": true,
+    "lean_kernel": false
+}
diff --git a/tests/projects/lean_kernel_off_unchecked/test.json b/tests/projects/lean_kernel_off_unchecked/test.json
new file mode 100644
index 0000000..fe08d6a
--- /dev/null
+++ b/tests/projects/lean_kernel_off_unchecked/test.json
@@ -0,0 +1,3 @@
+{
+        "exit_code": 1
+}