From 93aa0427136ec68f17694fc42591e65e56ec839d Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Sat, 17 Jan 2026 16:28:56 -0500
Subject: [PATCH] Change lakefile.lean to lakefile.toml

---
 lakefile.lean | 16 ----------------
 lakefile.toml | 21 +++++++++++++++++++++
 2 files changed, 21 insertions(+), 16 deletions(-)
 delete mode 100644 lakefile.lean
 create mode 100644 lakefile.toml

diff --git a/lakefile.lean b/lakefile.lean
deleted file mode 100644
index 2a69fad..0000000
--- a/lakefile.lean
+++ /dev/null
@@ -1,16 +0,0 @@
-import Lake
-open Lake DSL
-
-require «premise-selection» from git "https://github.com/hanwenzhu/premise-selection" @ "v4.26.0"
-
-require «Qq» from git "https://github.com/leanprover-community/quote4.git" @ "v4.26.0"
-
-require «HammerCore» from "./HammerCore"
-
-package Hammer {
-  precompileModules := true
-  preferReleaseBuild := true
-}
-
-@[default_target]
-lean_lib Hammer
diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 0000000..6d74bb6
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,21 @@
+name = "Hammer"
+precompileModules = true
+preferReleaseBuild = true
+defaultTargets = ["Hammer"]
+
+[[require]]
+name = "«premise-selection»"
+git = "https://github.com/hanwenzhu/premise-selection"
+rev = "v4.26.0"
+
+[[require]]
+name = "Qq"
+git = "https://github.com/leanprover-community/quote4.git"
+rev = "v4.26.0"
+
+[[require]]
+name = "HammerCore"
+path = "./HammerCore"
+
+[[lean_lib]]
+name = "Hammer"