From 6a6c0e395049938d5d334dcbee39a1ff56588a34 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 1 Sep 2026 02:24:48 +0000
Subject: [PATCH] chore: add benchmark sidecar skeleton

---
 bench/lake-manifest.json | 63 ++++++++++++++++++++++++++++++++++++++++
 bench/lakefile.toml      | 25 ++++++++++++++++
 bench/lean-toolchain     |  1 +
 3 files changed, 89 insertions(+)
 create mode 100644 bench/lake-manifest.json
 create mode 100644 bench/lakefile.toml
 create mode 100644 bench/lean-toolchain

diff --git a/bench/lake-manifest.json b/bench/lake-manifest.json
new file mode 100644
index 0000000..6a2eb83
--- /dev/null
+++ b/bench/lake-manifest.json
@@ -0,0 +1,63 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/kim-em/lean-bench.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "a768ba6c889bab583fcf254f5657e3753ca29063",
+   "name": "«lean-bench»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/hex-test-kit.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5b3dc5d7789cb680d64f8f4046254f93b7424e4f",
+   "name": "«hex-test-kit»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "5b3dc5d7789cb680d64f8f4046254f93b7424e4f",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"type": "path",
+   "scope": "",
+   "name": "HexRowReduce",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "..",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/mhuisi/lean4-cli.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.33.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/hex-matrix.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "049bf8e57b33cb87b4012ed9d2da4cce0af296d9",
+   "name": "HexMatrix",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "049bf8e57b33cb87b4012ed9d2da4cce0af296d9",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/hex-basic.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "2d7f55d190cc2df9c9bf55437f344e65fbddc7c0",
+   "name": "HexBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "2d7f55d190cc2df9c9bf55437f344e65fbddc7c0",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "«hex-row-reduce-bench»",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/bench/lakefile.toml b/bench/lakefile.toml
new file mode 100644
index 0000000..6dd3e5f
--- /dev/null
+++ b/bench/lakefile.toml
@@ -0,0 +1,25 @@
+name = "hex-row-reduce-bench"
+defaultTargets = ["hexrowreduce_bench"]
+
+leanOptions = [
+  { name = "doc.verso", value = true },
+  { name = "doc.verso.suggestions", value = false },
+]
+
+[[require]]
+name = "HexRowReduce"
+path = ".."
+
+[[require]]
+name = "hex-test-kit"
+git = "https://github.com/leanprover/hex-test-kit.git"
+rev = "5b3dc5d7789cb680d64f8f4046254f93b7424e4f"
+
+[[require]]
+name = "lean-bench"
+git = "https://github.com/kim-em/lean-bench.git"
+rev = "master"
+
+[[lean_exe]]
+name = "hexrowreduce_bench"
+root = "HexRowReduce.Bench"
diff --git a/bench/lean-toolchain b/bench/lean-toolchain
new file mode 100644
index 0000000..b814d98
--- /dev/null
+++ b/bench/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.34.0-rc2