71 | module Test.Golden

 73 | import Control.ANSI

 75 | import Data.Either

 76 | import Data.Maybe

 77 | import Data.List

 78 | import Data.List1

 79 | import Data.String

 80 | import Data.String.Extra

 82 | import System

 83 | import System.Clock

 84 | import System.Directory

 85 | import System.File

 86 | import System.Info

 87 | import System.Path

 88 | import System.Concurrency

 93 | public export

 94 | record Options where

 95 |   constructor MkOptions

 96 |   ||| Name of the idris2 executable

 97 |   exeUnderTest : String

 98 |   ||| Which codegen should we use?

 99 |   codegen      : Maybe String

100 |   ||| Should we only run some specific cases?

101 |   onlyNames    : Maybe (String -> Bool)

102 |   ||| Should we run the test suite interactively?

103 |   interactive  : Bool

104 |   ||| Should we use colors?

105 |   color        : Bool

106 |   ||| Should we time and display the tests

107 |   timing       : Bool

108 |   ||| How many threads should we use?

109 |   threads      : Nat

110 |   ||| Should we write the list of failing cases to a file?

111 |   failureFile     : Maybe String

114 | initOptions : String -> Bool -> Options

115 | initOptions exe color

116 |   = MkOptions exe

117 |               Nothing

118 |               Nothing

119 |               False

120 |               color

121 |               False

122 |               1

123 |               Nothing

126 | usage : String

127 | usage = unwords

128 |   ["Usage:"

129 |   , "runtests <path>"

130 |   , "[--timing]"

131 |   , "[--interactive]"

132 |   , "[--[no-]color, --[no-]colour]"

133 |   , "[--cg CODEGEN]"

134 |   , "[--threads N]"

135 |   , "[--failure-file PATH]"

136 |   , "[--only-file PATH]"

137 |   , "[[--only|--except] [NAMES]]"

138 |   ]

140 | optionsTestsFilter : List String -> List String -> Maybe (String -> Bool)

141 | optionsTestsFilter [] [] = Nothing

142 | optionsTestsFilter only except = Just $ \ name =>

143 |   let onlyCheck = null only || any (`isInfixOf` name) only in

144 |   let exceptCheck = all (not . (`isInfixOf` name)) except in

145 |   onlyCheck && exceptCheck

147 | record Acc where

148 |   constructor MkAcc

149 |   onlyFile : Maybe String

150 |   onlyNames : List String

151 |   exceptNames : List String

152 | initAcc : Acc

153 | initAcc = MkAcc Nothing [] []

157 | options : List String -> IO (Maybe Options)

158 | options args = case args of

159 |     (_ :: exe :: rest) => mkOptions exe rest

160 |     _ => pure Nothing

162 |   where

164 |     isFlag : String -> Bool

165 |     isFlag str = "--" `isPrefixOf` str

167 |     go : List String -> Acc -> Options -> Maybe (Acc, Options)

168 |     go rest acc opts = case rest of

169 |       []                            => pure (acc, opts)

170 |       ("--timing" :: xs)            => go xs acc ({ timing := True} opts)

171 |       ("--interactive" :: xs)       => go xs acc ({ interactive := True } opts)

172 |       ("--color"  :: xs)            => go xs acc ({ color := True } opts)

173 |       ("--colour" :: xs)            => go xs acc ({ color := True } opts)

174 |       ("--no-color"  :: xs)         => go xs acc ({ color := False } opts)

175 |       ("--no-colour" :: xs)         => go xs acc ({ color := False } opts)

176 |       ("--cg" :: cg :: xs)          => go xs acc ({ codegen := Just cg } opts)

177 |       ("--threads" :: n :: xs)      => do let pos : Nat = !(parsePositive n)

178 |                                           go xs acc ({ threads := pos } opts)

179 |       ("--failure-file" :: p :: xs) => go  xs acc ({ failureFile := Just p } opts)

180 |       ("--only" :: p :: xs)         =>

181 |         ifThenElse (isFlag p)

182 |           (go (p :: xs) acc opts)

183 |           (go xs ({ onlyNames $= (words p ++) } acc) opts)

184 |       ("--except" :: p :: xs)       =>

185 |         ifThenElse (isFlag p)

186 |           (go (p :: xs) acc opts)

187 |           (go xs ({ exceptNames $= (words p ++) } acc) opts)

188 |       ("--only-file" :: p :: xs)    => go xs ({ onlyFile := Just p } acc) opts

189 |       [p] => do guard (p `elem` ["--only", "--except"])

190 |                 pure (acc, opts)

191 |                 -- ^ we accept trailing only or except flags as unused (do not filter out any tests)

192 |                 -- for the convenience of populating these options from shell scripts.

193 |       _ => Nothing

195 |     mkOptions : String -> List String -> IO (Maybe Options)

196 |     mkOptions exe rest

197 |       = do color <- [ (isNothing noc) && tty | noc <- getEnv "NO_COLOR", tty <- isTTY stdout ]

198 |            let Just (acc, opts) = go rest initAcc (initOptions exe color)

199 |                  | Nothing => pure Nothing

200 |            extraOnlyNames <- the (IO (List String)) $ case acc.onlyFile of

201 |                                Nothing => pure []

202 |                                Just fp => do Right only <- readFile fp

203 |                                                | Left err => die (show err)

204 |                                              pure (lines only)

205 |            pure $ Just $ { onlyNames := optionsTestsFilter (extraOnlyNames ++ acc.onlyNames) acc.exceptNames } opts

212 | normalize : String -> String

213 | normalize str =

214 |     if isWindows

215 |       then pack $ filter (\ch => ch /= '/' && ch /= '\\') (unpack str)

216 |       else str

220 | Result : Type

221 | Result = Either String String

227 | runTest : Options -> (testPath : String) -> IO Result

228 | runTest opts testPath = do

229 |   start <- clockTime UTC

230 |   let cg = maybe "" (" --cg " ++) (codegen opts)

231 |   let exe = "\"" ++ exeUnderTest opts ++ cg ++ "\""

232 |   ignore $ system $ "cd " ++ escapeArg testPath ++ " && " ++

233 |     "sh ./run " ++ exe ++ " | tr -d '\\r' > output"

234 |   end <- clockTime UTC

236 |   Right out <- readFile $ testPath ++ "/output"

237 |     | Left err => do putStrLn $ (testPath ++ "/output") ++ ": " ++ show err

238 |                      pure (Left testPath)

240 |   Right exp <- readFile $ testPath ++ "/expected"

241 |     | Left FileNotFound => do

242 |         if interactive opts

243 |           then mayOverwrite Nothing out

244 |           else putStrLn $ (testPath ++ "/expected") ++ ": " ++ show FileNotFound

245 |         pure (Left testPath)

246 |     | Left err => do putStrLn $ (testPath ++ "/expected") ++ ": " ++ show err

247 |                      pure (Left testPath)

249 |   let result = normalize out == normalize exp

250 |   let time = timeDifference end start

252 |   if result

253 |     then printTiming opts.timing time testPath $ maybeColored BrightGreen "success"

254 |     else do

255 |       printTiming opts.timing time testPath $ maybeColored BrightRed "FAILURE"

256 |       if interactive opts

257 |         then mayOverwrite (Just exp) out

258 |         else putStr . unlines $ expVsOut exp out

260 |   pure $ if result then Right testPath else Left testPath

262 |   where

263 |     getAnswer : IO Bool

264 |     getAnswer = do

265 |       str <- getLine

266 |       case str of

267 |         "y" => pure True

268 |         "n" => pure False

269 |         "N" => pure False

270 |         ""  => pure False

271 |         _   => do putStrLn "Invalid answer."

272 |                   getAnswer

274 |     maybeColored : Color -> String -> String

275 |     maybeColored c = if opts.color then show . colored c else id

277 |     expVsOut : String -> String -> List String

278 |     expVsOut exp out = ["Expected:", maybeColored Green exp, "Given:", maybeColored Red out]

280 |     badSystemExitCode : Int -> Bool

281 |     badSystemExitCode code = code < 0 || code == 127 {- 127 means shell couldn't start -}

283 |     mayOverwrite : Maybe String -> String -> IO ()

284 |     mayOverwrite mexp out = do

285 |       case mexp of

286 |         Nothing => putStr $ unlines

287 |           [ "Golden value missing. I computed the following result:"

288 |           , maybeColored BrightBlue out

289 |           , "Accept new golden value? [y/N]"

290 |           ]

291 |         Just exp => do

292 |           code <- system $ "git diff --no-index --exit-code --word-diff-regex=. " ++

293 |             (if opts.color then  "--color " else "") ++

294 |             escapeArg testPath ++ "/expected " ++ escapeArg testPath ++ "/output"

295 |           putStr . unlines $

296 |             ["Golden value differs from actual value."] ++

297 |             (if badSystemExitCode code then expVsOut exp out else []) ++

298 |             ["Accept actual value as new golden value? [y/N]"]

299 |       b <- getAnswer

300 |       when b $ do Right _ <- writeFile (testPath ++ "/expected") out

301 |                     | Left err => putStrLn $ (testPath ++ "/expected") ++ ": " ++ show err

302 |                   pure ()

304 |     printTiming : Bool -> Clock type -> String -> String -> IO ()

305 |     printTiming False _     path msg = putStrLn $ concat [path, ": ", msg]

306 |     printTiming True  clock path msg =

307 |       let time  = showTime 2 3 clock

308 |           width = 72

309 |           -- We use 9 instead of `String.length msg` because:

310 |           -- 1. ": success" and ": FAILURE" have the same length

311 |           -- 2. ANSI escape codes make the msg look longer than it is

312 |           msgl  = 9

313 |           path  = leftEllipsis (width `minus` (1 + msgl + length time)) "(...)" path

314 |           spent = length time + length path + msgl

315 |           pad   = pack $ replicate (width `minus` spent) ' '

316 |       in putStrLn $ concat [path, ": ", msg, pad, time]

320 | pathLookup : List String -> IO (Maybe String)

321 | pathLookup names = do

322 |   path <- getEnv "PATH"

323 |   let extensions = if isWindows then [".exe", ".cmd", ".bat", ""] else [""]

324 |   let pathList = forget $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path

325 |   let candidates = [p ++ "/" ++ x ++ y | p <- pathList,

328 |   firstExists candidates

333 | public export

334 | record Requirement where

335 |   constructor MkReq

336 |   name : String

337 |   satisfy : IO (Maybe String)

340 | Show Requirement where

341 |   show = name

344 | Eq Requirement where

345 |   (==) = (==) `on` name

349 | public export

350 | data BackendRequirement = ReqC | ReqChez | ReqNodeJS | ReqRacket | ReqGambit

353 | checkRequirement : BackendRequirement -> IO (Maybe String)

354 | checkRequirement req

355 |   = if platformSupport req

356 |       then do let (envvar, paths) = requirement req

357 |               Just exec <- getEnv envvar | Nothing => pathLookup paths

358 |               pure (Just exec)

359 |       else pure Nothing

360 |   where

361 |     requirement : BackendRequirement -> (String, List String)

362 |     requirement ReqC = ("CC", ["cc"])

363 |     requirement ReqChez = ("CHEZ", ["chez", "chezscheme9.5", "chezscheme", "chez-scheme", "scheme"])

364 |     requirement ReqNodeJS = ("NODE", ["node"])

365 |     requirement ReqRacket = ("RACKET", ["racket"])

366 |     requirement ReqGambit = ("GAMBIT", ["gsc"])

368 |     platformSupport : BackendRequirement -> Bool

369 |     platformSupport ReqC = not isWindows

370 |     platformSupport ReqRacket = not isWindows

371 |     platformSupport _ = True

374 | C : Requirement

375 | C = MkReq "refc" (checkRequirement ReqC)

378 | Chez : Requirement

379 | Chez = MkReq "chez" (checkRequirement ReqChez)

382 | Node : Requirement

383 | Node = MkReq "node" (checkRequirement ReqNodeJS)

386 | Racket : Requirement

387 | Racket = MkReq "racket" (checkRequirement ReqRacket)

390 | Gambit : Requirement

391 | Gambit = MkReq "gambit" (checkRequirement ReqGambit)

394 | findCG : IO (Maybe String)

396 |   = do Nothing <- getEnv "IDRIS2_TESTS_CG" | p => pure p

397 |        Nothing <- checkRequirement ReqChez    | p => pure (Just "chez")

398 |        Nothing <- checkRequirement ReqNodeJS  | p => pure (Just "node")

399 |        Nothing <- checkRequirement ReqRacket  | p => pure (Just "racket")

400 |        Nothing <- checkRequirement ReqGambit  | p => pure (Just "gsc")

401 |        Nothing <- checkRequirement ReqC       | p => pure (Just "refc")

402 |        pure Nothing

405 | public export

406 | data Codegen

407 |   = ||| Do NOT pass a cg argument to the executable being tested

408 |     Nothing

409 |   | ||| Use whatever the test runner was passed at the toplevel,

411 |     Default

412 |   | ||| Use exactly the given requirement

413 |     Just Requirement

416 | codegenRequirement : Codegen -> List Requirement

417 | codegenRequirement (Just r) = [r]

418 | codegenRequirement _ = []

425 | public export

426 | record TestPool where

427 |   constructor MkTestPool

428 |   poolName : String

429 |   constraints : List Requirement

430 |   codegen : Codegen

431 |   testCases : List String

433 | findTests : (String -> Bool) -> Codegen -> String -> String -> IO (List String)

434 | findTests pred codegen poolName dirName = do

435 |   Right names <- listDir dirName

436 |     | Left e => die $ "failed to list " ++ dirName ++ ": " ++ show e

437 |   let names = [n | n <- names, pred n]

438 |   let testNames = [dirName ++ "/" ++ n | n <- names]

439 |   filter testNames

440 |     where

441 |       -- Directory without `run` file is not a test

442 |       isTest : (path : String) -> IO Bool

443 |       isTest path = exists (path ++ "/run")

445 |       filter : (testPaths : List String) -> IO (List String)

446 |       filter [] = pure []

447 |       filter (p :: ps) =

448 |           do rem <- filter ps

449 |              case !(isTest p) of

450 |                True  => pure $ p :: rem

451 |                False => pure rem

456 | testsInDir :

457 |   (dirName : String) ->

458 |   {default (const True) pred : String -> Bool} ->

459 |   (poolName : String) ->

460 |   {default [] requirements : List Requirement} ->

461 |   {default Nothing codegen : Codegen} ->

462 |   Lazy (IO TestPool)

463 | testsInDir dirName poolName = do

464 |   testNames <- findTests pred codegen poolName dirName

465 |   when (length testNames == 0) $ die $ "no tests found in " ++ dirName

466 |   pure $ MkTestPool poolName requirements codegen testNames

470 | filterTests : Options -> List String -> List String

471 | filterTests opts = case onlyNames opts of

472 |   Nothing => id

473 |   Just f  => filter f

476 | public export

477 | record Summary where

478 |   constructor MkSummary

479 |   success : List String

480 |   failure : List String

484 | initSummary : Summary

485 | initSummary = MkSummary [] []

489 | updateSummary : (newRes : Result) -> Summary -> Summary

490 | updateSummary newRes =

491 |   case newRes of

492 |        Left l  => { failure $= (l ::) }

493 |        Right w => { success $= (w ::) }

497 | bulkUpdateSummary : (newRess : List Result) -> Summary -> Summary

498 | bulkUpdateSummary newRess =

499 |   let (ls, ws) = partitionEithers newRess in

500 |   { success $= (ws ++)

501 |   , failure $= (ls ++)

502 |   }

505 | Semigroup Summary where

506 |   MkSummary ws1 ls1 <+> MkSummary ws2 ls2

507 |     = MkSummary (ws1 ++ ws2) (ls1 ++ ls2)

510 | Monoid Summary where

511 |   neutral = initSummary

514 | public export

515 | data ThreadInstruction : Type where

516 |   ||| A test to run

517 |   Run : (test : String) -> ThreadInstruction

518 |   ||| An indication for the thread to stop

519 |   Stop : ThreadInstruction

528 | testSender : (testChan : Channel ThreadInstruction) -> (nThreads : Nat)

529 |            -> (tests : List String) -> IO ()

530 | testSender testChan 0 [] = pure ()

531 | testSender testChan (S k) [] =

532 |   -- out of tests, so the next thing for all the threads is to stop

533 |   do channelPut testChan Stop

534 |      testSender testChan k []

535 | testSender testChan nThreads (test :: tests) =

536 |   do channelPut testChan (Run test)

537 |      testSender testChan nThreads tests

540 | public export

541 | data ThreadResult : Type where

542 |   ||| The result of running a test

543 |   Res : (res : Result) -> ThreadResult

544 |   ||| An indication that the thread was told to stop

545 |   Done : ThreadResult

558 | testReceiver : (resChan : Channel ThreadResult) -> (acc : Summary)

559 |              -> (accChan : Channel Summary) -> (nThreads : Nat) -> IO ()

560 | testReceiver resChan acc accChan 0 = channelPut accChan acc

561 | testReceiver resChan acc accChan nThreads@(S k) =

562 |   do (Res res) <- channelGet resChan

563 |         | Done => testReceiver resChan acc accChan k

564 |      testReceiver resChan (updateSummary res acc) accChan nThreads

571 | testThread : (opts : Options) -> (testChan : Channel ThreadInstruction)

572 |               -> (resChan : Channel ThreadResult) -> IO ()

573 | testThread opts testChan resChan =

574 |   do (Run test) <- channelGet testChan

575 |         | Stop => channelPut resChan Done

576 |      res <- runTest opts test

577 |      channelPut resChan (Res res)

578 |      testThread opts testChan resChan

587 | poolRunner : Options -> TestPool -> IO Summary

588 | poolRunner opts pool

589 |   = do -- check that we indeed want to run some of these tests

590 |        let tests = filterTests opts (testCases pool)

591 |        let (_ :: _) = tests

592 |              | [] => pure initSummary

593 |        -- if so make sure the constraints are satisfied

594 |        cs <- for (codegenRequirement pool.codegen ++ pool.constraints) $ \ req => do

595 |           mfp <- satisfy req

596 |           let msg = case mfp of

597 |                       Nothing => "✗ " ++ req.name ++ " not found"

598 |                       Just fp => "✓ Found " ++ req.name ++ " at " ++ fp

599 |           pure (mfp, msg)

600 |        let (cs, msgs) = unzip cs

602 |        putStrLn (banner msgs)

604 |        let Just _ = the (Maybe (List String)) (sequence cs)

605 |              | Nothing => pure initSummary

607 |        -- if the test pool requires a specific codegen then use that

608 |        let opts = case pool.codegen of

609 |                     Nothing => { codegen := Nothing } opts

610 |                     Just cg => { codegen := Just cg.name } opts

611 |                     Default => opts

613 |        -- set up the channels

614 |        accChan <- makeChannel

615 |        resChan <- makeChannel

616 |        testChan <- makeChannel

618 |        -- and then run all the tests

620 |        for_ (replicate opts.threads 0) $ \_ =>

621 |          fork (testThread opts testChan resChan)

622 |        -- start sending tests

623 |        senderTID <- fork $ testSender testChan opts.threads tests

624 |        -- start receiving results

625 |        receiverTID <- fork $ testReceiver resChan initSummary accChan opts.threads

626 |        -- wait until things are done, i.e. until we receive the final acc

627 |        acc <- channelGet accChan

628 |        pure acc

630 |   where

632 |     checkReq : {0 req : Type} -> Requirement -> IO (Maybe String, String)

633 |     checkReq req = do

634 |       mfp <- satisfy req

635 |       let msg = case mfp of

636 |                   Nothing => "✗ \{name req}  not found"

637 |                   Just fp => "✓ Found \{name req} at \{fp}"

638 |       pure (mfp, msg)

640 |     separator : String

641 |     separator = fastPack $ replicate 72 '-'

643 |     banner : List String -> String

644 |     banner msgs = fastUnlines

645 |         $ [ "", separator, pool.poolName ]

646 |        ++ msgs

647 |        ++ [ separator ]

650 | runnerWith : Options -> List TestPool -> IO ()

651 | runnerWith opts tests = do

653 |          -- if no CG has been set, find a sensible default based on what is available

654 |          opts <- case codegen opts of

655 |                    Nothing => pure $ { codegen := !findCG } opts

656 |                    Just _ => pure opts

658 |          -- run the tests

659 |          res <- concat <$> traverse (poolRunner opts) tests

661 |          -- report the result

662 |          let nsucc  = length res.success

663 |          let nfail  = length res.failure

664 |          let ntotal = nsucc + nfail

665 |          putStrLn (show nsucc ++ "/" ++ show ntotal ++ " tests successful")

667 |          -- deal with failures

668 |          let list = fastUnlines res.failure

669 |          when (nfail > 0) $

670 |            do putStrLn "Failing tests:"

671 |               putStr list

672 |          -- always overwrite the failure file, if it is given

673 |          whenJust opts.failureFile $ \ path =>

674 |            do Right _ <- writeFile path list

675 |                 | Left err => die (show err)

676 |               pure ()

678 |          -- exit

679 |          if nfail == 0

680 |            then exitSuccess

681 |            else exitFailure

685 | runner : List TestPool -> IO ()

686 | runner tests

687 |     = do args <- getArgs

688 |          Just opts <- options args

689 |             | _ => do printLn args

690 |                       putStrLn usage

691 |          runnerWith opts tests