From 8a448fb114a8a952129c6fe137a63fdd2359553e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 22 May 2023 11:47:46 -0700
Subject: [PATCH] Add testing stub

---
 Test/Main.lean     | 8 ++++++++
 lake-manifest.json | 6 ++++++
 lakefile.lean      | 9 +++++++++
 3 files changed, 23 insertions(+)
 create mode 100644 Test/Main.lean

diff --git a/Test/Main.lean b/Test/Main.lean
new file mode 100644
index 0000000..5f5fb23
--- /dev/null
+++ b/Test/Main.lean
@@ -0,0 +1,8 @@
+import LSpec
+import Pantograph.Symbols
+
+open Pantograph
+
+def main := do
+  LSpec.lspecIO $
+    LSpec.test "Symbol parsing" (Lean.Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run")
diff --git a/lake-manifest.json b/lake-manifest.json
index 675b62b..6a4ca4f 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -2,6 +2,12 @@
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
+   {"url": "https://github.com/lurk-lab/LSpec.git",
+    "subDir?": null,
+    "rev": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
+    "name": "LSpec",
+    "inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41"}},
+  {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
     "rev": "8e5a00a8afc8913c0584cb85f37951995275fd87",
diff --git a/lakefile.lean b/lakefile.lean
index 62ca33c..83efa04 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -17,6 +17,15 @@ lean_exe pantograph {
   supportInterpreter := true
 }
 
+require LSpec from git
+  "https://github.com/lurk-lab/LSpec.git" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41"
+lean_exe test {
+  root := `Test.Main
+  -- Somehow solves the native symbol not found problem
+  supportInterpreter := true
+
+}
+
 lean_exe examples_proof {
   root := `Examples.Proof
   -- Somehow solves the native symbol not found problem