Add testing stub

This commit is contained in:
Leni Aniva 2023-05-22 11:47:46 -07:00
parent 2772a394cc
commit 8a448fb114
3 changed files with 23 additions and 0 deletions

8
Test/Main.lean Normal file
View File

@ -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")

View File

@ -2,6 +2,12 @@
"packagesDir": "lake-packages", "packagesDir": "lake-packages",
"packages": "packages":
[{"git": [{"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", {"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null, "subDir?": null,
"rev": "8e5a00a8afc8913c0584cb85f37951995275fd87", "rev": "8e5a00a8afc8913c0584cb85f37951995275fd87",

View File

@ -17,6 +17,15 @@ lean_exe pantograph {
supportInterpreter := true 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 { lean_exe examples_proof {
root := `Examples.Proof root := `Examples.Proof
-- Somehow solves the native symbol not found problem -- Somehow solves the native symbol not found problem