test: add lspec testing framework

Author: brenno.rodrigues

.github/workflows/lspec.yml

@@ -0,0 +1,20 @@
+name: "LSpec CI"
+on:
+  pull_request:
+  push:
+    branches:
+      - master
+jobs:
+  build:
+    name: Build
+    runs-on: ubuntu-latest
+    steps:
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+      - uses: actions/checkout@v2
+      - name: run LSpec binary
+        run: lake exe lspec

Tests/Sqlite.lean

@@ -0,0 +1,23 @@
+import LSpec
+
+open LSpec
+
+def fourIO : IO Nat :=
+  pure 4
+
+def fiveIO : IO Nat :=
+  pure 5
+
+def main := do
+  let four ← fourIO
+  let five ← fiveIO
+  lspecIO $
+    test "fourIO equals 4" (four = 4) $
+    test "fiveIO equals 5" (five = 5)
+
+#check main
+#eval main
+
+#lspec
+  test "four equals four" (4 = 4) $
+  test "five equals five" (5 = 5)

lake-manifest.json

@@ -1,5 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages": [],
- "name": "ffi",
+ "packages":
+ [{"url": "https://github.com/argumentcomputer/lspec/",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "8a51034d049c6a229d88dd62f490778a377eec06",
+   "name": "LSpec",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "8a51034d049c6a229d88dd62f490778a377eec06",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "sqlite",
  "lakeDir": ".lake"}

lakefile.lean

@@ -10,6 +10,9 @@ lean_exe sqlite where
   root := `Main
   moreLinkArgs := #["-lsqlite3"]
 
+lean_exe Tests.Sqlite where
+  moreLinkArgs := #["-lsqlite3"]
+
 target sqliteffi.o pkg : FilePath := do
   let oFile := pkg.buildDir / "native" / "sqliteffi.o"
   let srcJob ← inputTextFile <| pkg.dir / "native" / "ffi.c"
@@ -20,3 +23,6 @@ extern_lib libsqliteffi pkg := do
   let ffiO ← sqliteffi.o.fetch
   let name := nameToStaticLib "sqliteffi"
   buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
+
+require LSpec from git
+  "https://github.com/argumentcomputer/lspec/" @ "8a51034d049c6a229d88dd62f490778a377eec06"