Add a lean_kernel option to skip the builtin kernel replay

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

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

tests/projects/lean_kernel_off_mismatch/Challenge.lean

@@ -0,0 +1,2 @@
+theorem comm (n m : Nat) : n + m = m + n := by
+  sorry

tests/projects/lean_kernel_off_mismatch/Solution.lean

@@ -0,0 +1 @@
+axiom comm (n m : Nat) : m + m = m + m

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
+}

tests/projects/lean_kernel_off_mismatch/test.json

@@ -0,0 +1,3 @@
+{
+        "exit_code": 1
+}

tests/projects/lean_kernel_off_nanoda/Challenge.lean

@@ -0,0 +1,2 @@
+theorem comm (n m : Nat) : n + m = m + n := by
+  sorry

tests/projects/lean_kernel_off_nanoda/Solution.lean

@@ -0,0 +1,2 @@
+theorem comm (n m : Nat) : n + m = m + n := by
+  grind

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
+}

tests/projects/lean_kernel_off_nanoda/test.json

@@ -0,0 +1,3 @@
+{
+        "exit_code": 0
+}

tests/projects/lean_kernel_off_no_kernel/Challenge.lean

@@ -0,0 +1,2 @@
+theorem comm (n m : Nat) : n + m = m + n := by
+  sorry

tests/projects/lean_kernel_off_no_kernel/Solution.lean

@@ -0,0 +1,2 @@
+theorem comm (n m : Nat) : n + m = m + n := by
+  grind

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
+}

tests/projects/lean_kernel_off_no_kernel/test.json

@@ -0,0 +1,3 @@
+{
+        "exit_code": 1
+}

tests/projects/lean_kernel_off_unchecked/Challenge.lean

@@ -0,0 +1,2 @@
+theorem zero_eq_one : (0 : Nat) = 1 := by
+  sorry

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)
+    }

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
+}

tests/projects/lean_kernel_off_unchecked/test.json

@@ -0,0 +1,3 @@
+{
+        "exit_code": 1
+}