test: add lspec testing framework

Changes

4 changed files (+61/-2)

• .github/workflows/lspec.yml (new)
  • @@ -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 (new)
  • @@ -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"