[ test ] cosmetic changes & retest capability (#1394)

* Banners for test pools
* Summary with the list of failing tests at the end
* Option to write the list of failing tests to a file
* Option to read the list of tests to run from a file
* Using these two latest features to add a new make target to rerun precisely the tests that failed last time

Author: gallais

.gitignore

@@ -21,6 +21,7 @@ idris2docs_venv
 /tests/**/*.so
 /tests/**/*.dylib
 /tests/**/*.dll
+/tests/failures
 
 /benchmark/**/build
 /benchmark/*.csv

Makefile

@@ -112,6 +112,13 @@ test: testenv
 	@echo
 	@${MAKE} -C tests only=$(only) IDRIS2=${TARGET} IDRIS2_PREFIX=${TEST_PREFIX}
 
+retest: testenv
+	@echo
+	@echo "NOTE: \`${MAKE} retest\` does not rebuild Idris or the libraries packaged with it; to do that run \`${MAKE}\`"
+	@if [ ! -x "${TARGET}" ]; then echo "ERROR: Missing IDRIS2 executable. Cannot run tests!\n"; exit 1; fi
+	@echo
+	@${MAKE} -C tests retest only=$(only) IDRIS2=${TARGET} IDRIS2_PREFIX=${TEST_PREFIX}
+
 
 support:
 	@${MAKE} -C support/c

libs/prelude/Prelude/Interfaces.idr

@@ -221,12 +221,17 @@ public export
 guard : Alternative f => Bool -> f ()
 guard x = if x then pure () else empty
 
-||| Conditionally execute an applicative expression.
+||| Conditionally execute an applicative expression when the boolean is true.
 public export
 when : Applicative f => Bool -> Lazy (f ()) -> f ()
 when True f = f
 when False f = pure ()
 
+||| Execute an applicative expression unless the boolean is true.
+%inline public export
+unless : Applicative f => Bool -> Lazy (f ()) -> f ()
+unless = when . not
+
 ---------------------------
 -- FOLDABLE, TRAVERSABLE --
 ---------------------------

libs/prelude/Prelude/Types.idr

@@ -157,6 +157,12 @@ maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
 maybe n j Nothing  = n
 maybe n j (Just x) = j x
 
+||| Execute an applicative expression when the Maybe is Just
+%inline public export
+whenJust : Applicative f => Maybe a -> (a -> f ()) -> f ()
+whenJust (Just a) k = k a
+whenJust Nothing k = pure ()
+
 public export
 Eq a => Eq (Maybe a) where
   Nothing  == Nothing  = True

libs/test/Test/Golden.idr

@@ -43,9 +43,11 @@
 ||| + `idris2`       The path of the executable we are testing.
 ||| + `codegen`      The backend to use for code generation.
 ||| + `onlyNames`    The tests to run relative to the generated executable.
+||| + `onlyFile`     The file listing the tests to run relative to the generated executable.
 ||| + `interactive`  Whether to offer to update the expected file or not.
 ||| + `timing`       Whether to display time taken for each test.
 ||| + `threads`      The maximum numbers to use (default: number of cores).
+||| + `failureFile`  The file in which to write the list of failing tests.
 |||
 ||| We provide an options parser (`options`) that takes the list of command line
 ||| arguments and constructs this for you.
@@ -62,6 +64,7 @@
 
 module Test.Golden
 
+import Data.Either
 import Data.Maybe
 import Data.List
 import Data.List1
@@ -93,6 +96,8 @@ record Options where
   timing       : Bool
   ||| How many threads should we use?
   threads      : Nat
+  ||| Should we write the list of failing cases from a file?
+  failureFile     : Maybe String
 
 export
 initOptions : String -> Options
@@ -103,6 +108,7 @@ initOptions exe
               False
               False
               1
+              Nothing
 
 export
 usage : String -> String
@@ -113,37 +119,48 @@ usage exe = unwords
   , "[--interactive]"
   , "[--cg CODEGEN]"
   , "[--threads N]"
+  , "[--failure-file PATH]"
+  , "[--only-file PATH]"
   , "[--only [NAMES]]"
   ]
 
+export
+fail : String -> IO a
+fail err
+    = do putStrLn err
+         exitWith (ExitFailure 1)
+
 ||| Process the command line options.
 export
-options : List String -> Maybe Options
+options : List String -> IO (Maybe Options)
 options args = case args of
-    (_ :: exe :: rest) => go rest (initOptions exe)
-    _ => Nothing
+    (_ :: exe :: rest) => mkOptions exe rest
+    _ => pure Nothing
 
   where
 
-    go : List String -> Options -> Maybe Options
-    go rest opts = case rest of
-      []                       => pure opts
-      ("--timing" :: xs)       => go xs (record { timing = True} opts)
-      ("--interactive" :: xs)  => go xs (record { interactive = True } opts)
-      ("--cg" :: cg :: xs)     => go xs (record { codegen = Just cg } opts)
-      ("--threads" :: n :: xs) => do let pos : Nat = !(parsePositive n)
-                                     go xs (record { threads = pos } opts)
-      ("--only" :: xs)         => pure $ record { onlyNames = xs } opts
+    go : List String -> Maybe String -> Options -> Maybe (Maybe String, Options)
+    go rest only opts = case rest of
+      []                            => pure (only, opts)
+      ("--timing" :: xs)            => go xs only (record { timing = True} opts)
+      ("--interactive" :: xs)       => go xs only (record { interactive = True } opts)
+      ("--cg" :: cg :: xs)          => go xs only (record { codegen = Just cg } opts)
+      ("--threads" :: n :: xs)      => do let pos : Nat = !(parsePositive n)
+                                          go xs only (record { threads = pos } opts)
+      ("--failure-file" :: p :: xs) => go  xs only (record { failureFile = Just p } opts)
+      ("--only" :: xs)              => pure (only, record { onlyNames = xs } opts)
+      ("--only-file" :: p :: xs)    => go xs (Just p) opts
       _ => Nothing
 
--- [ Core ]
-
-export
-fail : String -> IO ()
-fail err
-    = do putStrLn err
-         exitWith (ExitFailure 1)
-
+    mkOptions : String -> List String -> IO (Maybe Options)
+    mkOptions exe rest
+      = do let Just (mfp, opts) = go rest Nothing (initOptions exe)
+                 | Nothing => pure Nothing
+           let Just fp = mfp
+                 | Nothing => pure (Just opts)
+           Right only <- readFile fp
+             | Left err => fail (show err)
+           pure $ Just $ record { onlyNames $= (forget (lines only) ++) } opts
 
 ||| Normalise strings between different OS.
 |||
@@ -156,13 +173,18 @@ normalize str =
       then pack $ filter (\ch => ch /= '/' && ch /= '\\') (unpack str)
       else str
 
+||| The result of a test run
+||| `Left` corresponds to a failure, and `Right` to a success
+Result : Type
+Result = Either String String
+
 ||| Run the specified Golden test with the supplied options.
 |||
 ||| See the module documentation for more information.
 |||
 ||| @testPath the directory that contains the test.
 export
-runTest : Options -> String -> IO (Future Bool)
+runTest : Options -> String -> IO (Future Result)
 runTest opts testPath = forkIO $ do
   start <- clockTime Thread
   let cg = case codegen opts of
@@ -174,16 +196,16 @@ runTest opts testPath = forkIO $ do
 
   Right out <- readFile $ testPath ++ "/output"
     | Left err => do print err
-                     pure False
+                     pure (Left testPath)
 
   Right exp <- readFile $ testPath ++ "/expected"
     | Left FileNotFound => do
         if interactive opts
           then mayOverwrite Nothing out
           else print FileNotFound
-        pure False
+        pure (Left testPath)
     | Left err => do print err
-                     pure False
+                     pure (Left testPath)
 
   let result = normalize out == normalize exp
   let time = timeDifference end start
@@ -196,7 +218,7 @@ runTest opts testPath = forkIO $ do
         then mayOverwrite (Just exp) out
         else putStrLn . unlines $ expVsOut exp out
 
-  pure result
+  pure $ if result then Right testPath else Left testPath
 
   where
     getAnswer : IO Bool
@@ -298,6 +320,7 @@ findCG
 public export
 record TestPool where
   constructor MkTestPool
+  poolName : String
   constraints : List Requirement
   testCases : List String
 
@@ -308,14 +331,43 @@ filterTests opts = case onlyNames opts of
   [] => id
   xs => filter (\ name => any (`isInfixOf` name) xs)
 
+||| The summary of a test pool run
+public export
+record Summary where
+  constructor MkSummary
+  success : List String
+  failure : List String
+
+export
+initSummary : Summary
+initSummary = MkSummary [] []
+
+export
+updateSummary : List Result -> Summary -> Summary
+updateSummary res =
+  let (ls, ws) = partitionEithers res in
+  { success $= (ws ++)
+  , failure $= (ls ++)
+  }
+
+export
+Semigroup Summary where
+  MkSummary ws1 ls1 <+> MkSummary ws2 ls2
+    = MkSummary (ws1 ++ ws2) (ls1 ++ ls2)
+
+export
+Monoid Summary where
+  neutral = initSummary
+
 ||| A runner for a test pool
 export
-poolRunner : Options -> TestPool -> IO (List Bool)
+poolRunner : Options -> TestPool -> IO Summary
 poolRunner opts pool
   = do -- check that we indeed want to run some of these tests
        let tests = filterTests opts (testCases pool)
        let (_ :: _) = tests
-             | [] => pure []
+             | [] => pure initSummary
+       putStrLn banner
        -- if so make sure the constraints are satisfied
        cs <- for (constraints pool) $ \ req => do
           mfp <- checkRequirement req
@@ -324,37 +376,60 @@ poolRunner opts pool
             Just fp => "Found " ++ show req ++ " at " ++ fp
           pure mfp
        let Just _ = the (Maybe (List String)) (sequence cs)
-             | Nothing => pure []
+             | Nothing => pure initSummary
        -- if so run them all!
-       loop [] tests
+       loop initSummary tests
 
   where
-    loop : List (List Bool) -> List String -> IO (List Bool)
-    loop acc [] = pure (concat $ reverse acc)
+
+    banner : String
+    banner =
+      let separator = fastPack $ replicate 72 '-' in
+      fastUnlines [ "", separator, pool.poolName, separator, "" ]
+
+    loop : Summary -> List String -> IO Summary
+    loop acc [] = pure acc
     loop acc tests
       = do let (now, later) = splitAt opts.threads tests
            bs <- map await <$> traverse (runTest opts) now
-           loop (bs :: acc) later
+           loop (updateSummary bs acc) later
 
 
 ||| A runner for a whole test suite
 export
 runner : List TestPool -> IO ()
 runner tests
     = do args <- getArgs
-         let (Just opts) = options args
-              | _ => do print args
-                        putStrLn (usage "runtests")
+         Just opts <- options args
+            | _ => do print args
+                      putStrLn (usage "runtests")
          -- if no CG has been set, find a sensible default based on what is available
          opts <- case codegen opts of
                    Nothing => pure $ record { codegen = !findCG } opts
                    Just _ => pure opts
          -- run the tests
          res <- concat <$> traverse (poolRunner opts) tests
-         putStrLn (show (length (filter id res)) ++ "/" ++ show (length res)
-                       ++ " tests successful")
-         if (any not res)
-            then exitWith (ExitFailure 1)
-            else exitWith ExitSuccess
+
+         -- report the result
+         let nsucc  = length res.success
+         let nfail  = length res.failure
+         let ntotal = nsucc + nfail
+         putStrLn (show nsucc ++ "/" ++ show ntotal ++ " tests successful")
+
+         -- deal with failures
+         let list = fastUnlines res.failure
+         when (nfail > 0) $
+           do putStrLn "Failing tests:"
+              putStrLn list
+         -- always overwrite the failure file, if it is given
+         whenJust opts.failureFile $ \ path =>
+           do Right _ <- writeFile path list
+                | Left err => fail (show err)
+              pure ()
+
+         -- exit
+         if nfail == 0
+           then exitWith ExitSuccess
+           else exitWith (ExitFailure 1)
 
 -- [ EOF ]