chore: switch to Lakefile.toml

leanprover-community · Jul 1, 2024 · b9c49ea · b9c49ea
1 parent ca6660a
commit b9c49ea
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 0 deletions.
diff --git a/lakefile.toml 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
@@ -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.+"]