From 3c972ca2d4e3fb5f336bd2c153e3bd744913b714 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 7 Jul 2026 16:44:52 +0000
Subject: [PATCH] chore: replace lean4checker dependency with upstreamed
 `replay`

`Lean.Environment.replay` has been re-upstreamed into Lean core (available
via `import Lean`), so the lean4checker fork `replay'` is no longer needed.
Drop the `Lean4Checker` require and use `env.replay` directly.
---
 Main.lean          |  3 +--
 lake-manifest.json | 10 ----------
 lakefile.toml      |  5 -----
 3 files changed, 1 insertion(+), 17 deletions(-)

diff --git a/Main.lean b/Main.lean
index 3fe7c54..284f7a3 100644
--- a/Main.lean
+++ b/Main.lean
@@ -5,7 +5,6 @@ Authors: Henrik Böving
 -/
 import Lean
 import Comparator
-import Lean4Checker.Replay
 import Export.Parse
 
 namespace Comparator
@@ -198,7 +197,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 3cbb6ab..4f014bf 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"