Skip to content

Commit

Permalink
chore: more informative tests for debugging
Browse files Browse the repository at this point in the history
  • Loading branch information
david-christiansen committed Mar 5, 2024
1 parent 8c578eb commit 07957a2
Showing 1 changed file with 3 additions and 6 deletions.
9 changes: 3 additions & 6 deletions Tests.lean
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,10 @@ import Lean
open SubVerso.Examples (loadExamples Example)
open Lean.FromJson (fromJson?)

def assert (what : String) (cond : Unit -> Bool) : IO Unit := do
if !(cond ()) then
throw <| .userError what


def main : IO UInt32 := do
IO.println "Checking that the test project generates at least some deserializable JSON"
let examples ← loadExamples "demo"
assert "Examples are non-empty" fun () => !examples.isEmpty
if examples.isEmpty then
IO.eprintln "No examples found"
return 1
pure 0

0 comments on commit 07957a2

Please sign in to comment.