From d30e39430e003ae5bc99bcf909527426e2ab83ee Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Wed, 15 Jul 2026 17:51:15 +0200
Subject: [PATCH 1/2] chore: adaptations from downstream-lean4

---
 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 96c7a90..795d7e8 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 66123e5ff8181eb3807753ddec4231e3856fc76a Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Wed, 15 Jul 2026 17:51:17 +0200
Subject: [PATCH 2/2] chore: bump toolchain to v4.33.0-rc1

---
 lake-manifest.json | 2 +-
 lean-toolchain     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 795d7e8..cb87e1f 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "4e7915201d3f9f04470d9eae002fa695f7cdc589",
+   "rev": "af5aa64bb914c3c2c781f378088dbd38acf4f804",
    "name": "lean4export",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
diff --git a/lean-toolchain b/lean-toolchain
index 94b9f49..fd85b26 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.32.0
+leanprover/lean4:v4.33.0-rc1