From c144d2ed985d3fc2d4017f514a5a935f066c3ad3 Mon Sep 17 00:00:00 2001
From: Serhii Khoma <sergey@nordicresults.com>
Date: Wed, 22 Apr 2026 12:53:18 +0700
Subject: [PATCH] feat: use lakefile.toml, move tests into separate dir

---
 QuerySMTTests.lean                            |  3 +++
 .../issues.lean => QuerySMTTests/Issues.lean  |  0
 .../tests.lean => QuerySMTTests/Tests.lean    |  0
 .../tests2.lean => QuerySMTTests/Tests2.lean  |  0
 lakefile.lean                                 | 16 ------------
 lakefile.toml                                 | 26 +++++++++++++++++++
 6 files changed, 29 insertions(+), 16 deletions(-)
 create mode 100644 QuerySMTTests.lean
 rename QuerySMT/issues.lean => QuerySMTTests/Issues.lean (100%)
 rename QuerySMT/tests.lean => QuerySMTTests/Tests.lean (100%)
 rename QuerySMT/tests2.lean => QuerySMTTests/Tests2.lean (100%)
 delete mode 100644 lakefile.lean
 create mode 100644 lakefile.toml

diff --git a/QuerySMTTests.lean b/QuerySMTTests.lean
new file mode 100644
index 0000000..066878e
--- /dev/null
+++ b/QuerySMTTests.lean
@@ -0,0 +1,3 @@
+import QuerySMTTests.Issues
+import QuerySMTTests.Tests
+import QuerySMTTests.Tests2
diff --git a/QuerySMT/issues.lean b/QuerySMTTests/Issues.lean
similarity index 100%
rename from QuerySMT/issues.lean
rename to QuerySMTTests/Issues.lean
diff --git a/QuerySMT/tests.lean b/QuerySMTTests/Tests.lean
similarity index 100%
rename from QuerySMT/tests.lean
rename to QuerySMTTests/Tests.lean
diff --git a/QuerySMT/tests2.lean b/QuerySMTTests/Tests2.lean
similarity index 100%
rename from QuerySMT/tests2.lean
rename to QuerySMTTests/Tests2.lean
diff --git a/lakefile.lean b/lakefile.lean
deleted file mode 100644
index 2ae3e43..0000000
--- a/lakefile.lean
+++ /dev/null
@@ -1,16 +0,0 @@
-import Lake
-open Lake DSL
-
-require «mathlib» from git "https://github.com/leanprover-community/mathlib4" @ "v4.29.0"
-
-require «Duper» from git "https://github.com/leanprover-community/duper.git" @ "a05206eadfece7682abf44d52e8fd8c7110ef58a"
-
-require «premise-selection» from git "https://github.com/hanwenzhu/premise-selection" @ "v4.29.0"
-
-package QuerySMT {
-  precompileModules := false
-  preferReleaseBuild := false
-}
-
-@[default_target]
-lean_lib QuerySMT
diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 0000000..6e51f45
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,26 @@
+name = "QuerySMT"
+version = "0.1.0"
+defaultTargets = ["QuerySMT"]
+precompileModules = false
+preferReleaseBuild = false
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4"
+rev = "v4.29.0"
+
+[[require]]
+name = "Duper"
+git = "https://github.com/leanprover-community/duper.git"
+rev = "a05206eadfece7682abf44d52e8fd8c7110ef58a"
+
+[[require]]
+name = "premise-selection"
+git = "https://github.com/hanwenzhu/premise-selection"
+rev = "v4.29.0"
+
+[[lean_lib]]
+name = "QuerySMT"
+
+[[lean_lib]]
+name = "QuerySMTTests"