From b9c49ea9fe71fec3f94432e4cb203cb2fe46c404 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 1 Jul 2024 12:40:53 +1000
Subject: [PATCH] chore: switch to Lakefile.toml

---
 lakefile.toml              | 10 ++++++++++
 test/Mathlib/lakefile.toml | 11 +++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 lakefile.toml
 create mode 100644 test/Mathlib/lakefile.toml

diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 0000000..589e047
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,10 @@
+name = "REPL"
+defaultTargets = ["repl"]
+
+[[lean_lib]]
+name = "REPL"
+
+[[lean_exe]]
+name = "repl"
+root = "REPL.Main"
+supportInterpreter = true
diff --git a/test/Mathlib/lakefile.toml b/test/Mathlib/lakefile.toml
new file mode 100644
index 0000000..1546899
--- /dev/null
+++ b/test/Mathlib/lakefile.toml
@@ -0,0 +1,11 @@
+name = "«repl-mathlib-tests»"
+defaultTargets = ["ReplMathlibTests"]
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4"
+rev = "master"
+
+[[lean_lib]]
+name = "ReplMathlibTests"
+globs = ["test.+"]