fix: replay kernel primitives before the rest of the solution

Comparator/Util.lean

@@ -25,4 +25,19 @@ def runForUsedConsts [Monad m] (info : Lean.ConstantInfo) (f : Lean.Name → m U
       f rule.ctor
       rule.rhs.getUsedConstants.forM f
 
+/--
+The names in `constMap` that `roots` depend on, transitively and including `roots` themselves.
+-/
+partial def dependencyClosure (constMap : Std.HashMap Lean.Name Lean.ConstantInfo)
+    (roots : Array Lean.Name) : Lean.NameSet :=
+  (roots.forM visit).run {} |>.snd
+where
+  visit (n : Lean.Name) : StateM Lean.NameSet Unit := do
+    if (← get).contains n then return
+    let some info := constMap[n]? | return
+    modify (·.insert n)
+    runForUsedConsts info visit
+    -- The kernel needs `Eq` to add `Quot`, without `Quot` mentioning it.
+    if info matches .quotInfo .. then visit ``Eq
+
 end Comparator

Main.lean

@@ -209,7 +209,8 @@ where
     -- TODO: get rid of this heuristic
     kernelName.contains "noda"
 
-def runBuiltinKernel (solution : Export.ExportedEnv) : M (Option String) := do
+def runBuiltinKernel (solution : Export.ExportedEnv) (primitives : Array Lean.Name) :
+    M (Option String) := do
   IO.println "Running Lean default kernel on solution."
   let env ← Lean.mkEmptyEnvironment
   let mut kernelEnv := env.toKernelEnv
@@ -218,8 +219,15 @@ def runBuiltinKernel (solution : Export.ExportedEnv) : M (Option String) := do
   -- multiple times leads to errors.
   let quotTargets := [`Quot.mk, `Quot.lift, `Quot.ind]
   let kernelConstMap := quotTargets.foldl (init := origConstMap) (·.erase ·)
+  -- The kernel can use primitives that no declaration mentions, e.g. it unfolds a string literal
+  -- to `String.ofList [Char.ofNat ..]`. `replay` only orders by mentioned constants, so add the
+  -- primitives and their dependencies first.
+  let primitiveClosure := dependencyClosure kernelConstMap primitives
+  let primitiveConstMap := kernelConstMap.filter fun n _ => primitiveClosure.contains n
+  let restConstMap := kernelConstMap.filter fun n _ => !primitiveClosure.contains n
   try
-    kernelEnv ← kernelEnv.replay kernelConstMap
+    kernelEnv ← kernelEnv.replay primitiveConstMap
+    kernelEnv ← kernelEnv.replay restConstMap
     IO.println "Lean default kernel accepts the solution"
   catch e =>
     IO.println "Lean default kernel rejects the solution"
@@ -297,7 +305,7 @@ 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)
+  result := result <|> (← runBuiltinKernel solution (← primitiveTargets))
   if let some error := result then
     throw <| IO.userError error
 

tests/projects/string_literal_decide/Challenge.lean

@@ -0,0 +1,2 @@
+theorem str_ne : ("live" = "dead") = False := by
+  sorry

tests/projects/string_literal_decide/Solution.lean

@@ -0,0 +1,2 @@
+theorem str_ne : ("live" = "dead") = False := by
+  decide

tests/projects/string_literal_decide/config.json

@@ -0,0 +1,7 @@
+{
+    "challenge_module": "Challenge",
+    "solution_module": "Solution",
+    "theorem_names": ["str_ne"],
+    "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
+    "enable_nanoda": false
+}

tests/projects/string_literal_decide/test.json

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

tests/projects/string_literal_match/Challenge.lean

@@ -0,0 +1,7 @@
+def strTag (s : String) : Nat :=
+  match s with
+  | "live" => 1
+  | _ => 0
+
+theorem strTag_live : strTag "live" = 1 := by
+  sorry

tests/projects/string_literal_match/Solution.lean

@@ -0,0 +1,6 @@
+def strTag (s : String) : Nat :=
+  match s with
+  | "live" => 1
+  | _ => 0
+
+theorem strTag_live : strTag "live" = 1 := rfl

tests/projects/string_literal_match/config.json

@@ -0,0 +1,7 @@
+{
+    "challenge_module": "Challenge",
+    "solution_module": "Solution",
+    "theorem_names": ["strTag_live"],
+    "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
+    "enable_nanoda": false
+}

tests/projects/string_literal_match/test.json

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