From 6cd793ea329b5ba1bd042a4e690d3cd5a0e557f8 Mon Sep 17 00:00:00 2001
From: Stephen Huan <stephen.huan@cgdct.moe>
Date: Thu, 4 Jun 2026 03:09:03 -0400
Subject: [PATCH 1/2] build: remove lean4checker

lean4checker is deprecated and can be replaced with
Lean.Replay from the Lean repository since Lean v4.28.0.
---
 Main.lean          |  4 ++--
 lake-manifest.json | 10 ----------
 lakefile.toml      |  5 -----
 3 files changed, 2 insertions(+), 17 deletions(-)

diff --git a/Main.lean b/Main.lean
index 3fe7c54..bd1c143 100644
--- a/Main.lean
+++ b/Main.lean
@@ -5,7 +5,7 @@ Authors: Henrik Böving
 -/
 import Lean
 import Comparator
-import Lean4Checker.Replay
+import Lean.Replay
 import Export.Parse
 
 namespace Comparator
@@ -198,7 +198,7 @@ def runKernel (solution : Export.ExportedEnv) : M Unit := do
   -- Lean's kernel interprets just the addition of `Quot as adding all of these so adding them
   -- multiple times leads to errors.
   constMap := constMap.erase `Quot.mk |>.erase `Quot.lift |>.erase `Quot.ind
-  discard <| env.replay' constMap
+  discard <| env.replay constMap
   IO.println "Lean default kernel accepts the solution"
 
 def primitiveTargets : M (Array Lean.Name) := do
diff --git a/lake-manifest.json b/lake-manifest.json
index af32031..af47a1b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -10,16 +10,6 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": false,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/lean4checker",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover",
-   "rev": "b7398199245524275543dec6113229c9bb4902e5",
-   "name": "Lean4Checker",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "b7398199245524275543dec6113229c9bb4902e5",
-   "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "Comparator",
  "lakeDir": ".lake",
diff --git a/lakefile.toml b/lakefile.toml
index 1865ae8..8b55152 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -9,11 +9,6 @@ name = "Comparator"
 name = "comparator"
 root = "Main"
 
-[[require]]
-scope = "leanprover"
-name = "Lean4Checker"
-rev = "b7398199245524275543dec6113229c9bb4902e5"
-
 [[require]]
 scope = "leanprover"
 name = "lean4export"

From c4d57e37eba21b77589e4ffe2a7e498dacfc5c69 Mon Sep 17 00:00:00 2001
From: Stephen Huan <stephen.huan@cgdct.moe>
Date: Thu, 4 Jun 2026 04:59:08 -0400
Subject: [PATCH 2/2] chore(.gitignore): ignore .lake anywhere

---
 .gitignore | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index bfb30ec..01f8cdb 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1 @@
-/.lake
+.lake/