From 08d5cf5b50e93c6eab130d75bc08f4d4dab42930 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 22 Oct 2024 09:23:39 +1100
Subject: [PATCH] chore: switch to lakefile.toml

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

diff --git a/lakefile.lean b/lakefile.lean
deleted file mode 100644
index 7c287c4c95..0000000000
--- a/lakefile.lean
+++ /dev/null
@@ -1,18 +0,0 @@
-import Lake
-
-open Lake DSL
-
-package batteries where
-  leanOptions := #[⟨`linter.missingDocs, true⟩]
-
-@[default_target]
-lean_lib Batteries
-
-@[default_target, lint_driver]
-lean_exe runLinter where
-  srcDir := "scripts"
-  supportInterpreter := true
-
-@[test_driver]
-lean_exe test where
-  srcDir := "scripts"
diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 0000000000..a8a658ef9f
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,19 @@
+name = "batteries"
+testDriver = "test"
+lintDriver = "runLinter"
+defaultTargets = ["Batteries", "runLinter"]
+
+[leanOptions]
+linter.missingDocs = true
+
+[[lean_lib]]
+name = "Batteries"
+
+[[lean_exe]]
+name = "runLinter"
+srcDir = "scripts"
+supportInterpreter = true
+
+[[lean_exe]]
+name = "test"
+srcDir = "scripts"