Skip to content
This repository has been archived by the owner on Aug 24, 2024. It is now read-only.

Commit

Permalink
fix: run all tests so we can report how many tests failed
Browse files Browse the repository at this point in the history
  • Loading branch information
lovettchris committed Sep 1, 2022
1 parent f548a15 commit 93447fd
Showing 1 changed file with 5 additions and 2 deletions.
7 changes: 5 additions & 2 deletions lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,7 @@ different. -/
def execute (capture : Bool) : IO UInt32 := do
let root : FilePath := "." / "test"
let dirs ← walkDir root
let mut retVal : UInt32 := 0
for test in dirs do
if test.extension = "lean" && test.fileName != "lakefile.lean" && !test.components.contains "lean_packages" then
if let some fileName := test.fileName then
Expand All @@ -76,8 +77,10 @@ def execute (capture : Bool) : IO UInt32 := do
IO.println s!" SUCCESS"
else
IO.println s!" FAILED: diff {expected} {actual}"
return 1
return 0
retVal := retVal + 1
if retVal > 0 then
IO.println s!"FAILED: {retVal} tests failed!"
return retVal

script tests (args) do
IO.println "Running diff tests for leanInk"
Expand Down

0 comments on commit 93447fd

Please sign in to comment.