------------------------------------------------------------------------
-- The Agda standard library
--
-- Golden testing framework
------------------------------------------------------------------------
-- This is a port of the golden testing framework used by the Idris2
-- compiler and various Idris2 libraries.
-- It provides the core features required to perform golden file testing.
--
-- We provide the core functionality to run a *single* golden file test,
-- or a whole test tree. This allows the developer freedom to use as is
-- or design the rest of the test harness to their liking.
------------------------------------------------------------------------
-- Test Structure
--
-- This harness works from the assumption that each individual golden
-- test comprises of a directory with the following structure:
--
-- + `run` a *shell* script that runs the test. We expect it to:
-- * Use `$1` as the variable standing for the Agda executable to be tested
-- * Clean up after itself (e.g. by running `rm -rf build/`)
--
-- + `expected` a file containing the expected output of `run`
--
-- During testing, the test harness will generate an `output` file.
-- It will be compared to the `expected` golden file provided by the user.
-- In case there is a mismatch, the framework will:
-- + either display output & expected if the session is not interactive
-- + or use the following command line to produce a diff and ask the user
-- whether they want to overwrite the currently `expected` value:
--
-- git diff --no-index --exit-code --word-diff=color expected output
--
-- If `git` fails then the runner will simply present the expected and
-- 'given' files side-by-side.
--
-- Of note, it is helpful to add `output` to a local `.gitignore` instance
-- to ensure that it is not mistakenly versioned.
------------------------------------------------------------------------
-- Options
--
-- The test harness has several options that may be set:
--
-- + `exeUnderTest` The path of the executable we are testing (typically `agda`)
-- + `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.
-- + `failureFile` The file in which to write the list of failing tests.
-- + `colour` The output should use ANSI escape codes
--
-- We provide an options parser (`options`) that takes the list of command line
-- arguments and constructs this for you.
--
------------------------------------------------------------------------
-- Usage
--
-- When compiled to an executable the expected usage is:
--
--```sh
--runtests <path to executable under test>
-- [--timing]
-- [--interactive]
-- [--only-file PATH]
-- [--failure-file PATH]
-- [--no-colour]
-- [--only [NAMES]]
--```
--
-- assuming that the test runner is compiled to an executable named `runtests`.
{-# OPTIONS --cubical-compatible --guardedness #-}
module Test.Golden where
open import Data.Bool.Base using (Bool; true; false; if_then_else_)
import Data.Char as Char
open import Data.Fin using (#_)
import Data.Integer.Base as ℤ
open import Data.List.Base as List using (List; []; _∷_; _++_; filter; partitionSums)
open import Data.List.Relation.Binary.Infix.Heterogeneous.Properties using (infix?)
open import Data.List.Relation.Unary.Any using (any?)
open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe)
open import Data.Nat.Base using (ℕ; _≡ᵇ_; _<ᵇ_; _+_; _∸_)
open import Data.Nat.ListAction using (sum)
import Data.Nat.Show as ℕ using (show)
open import Data.Product.Base using (_×_; _,_)
open import Data.String.Base as String using (String; lines; unlines; unwords; concat)
open import Data.String.Properties as String using (_≟_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Data.Unit.Base using (⊤)
open import Function.Base using (id; _$_; case_of_)
open import Relation.Nullary.Decidable.Core using (does)
open import Codata.Musical.Notation using (♯_)
open import IO
open import System.Clock as Clock using (time′; Time; seconds)
open import System.Console.ANSI
open import System.Directory using (doesFileExist; doesDirectoryExist)
open import System.Environment using (getArgs; lookupEnv)
open import System.Exit
open import System.FilePath.Posix using (mkFilePath)
open import System.Process using (callCommand; system)
record Options : Set where
field
-- What is the name of the Agda executable?
exeUnderTest : String
-- Should we only run some specific cases?
onlyNames : List String
-- Should we run the test suite interactively?
interactive : Bool
-- Should we time and display the tests?
timing : Bool
-- Should we write the list of failing cases to a file?
failureFile : Maybe String
-- Should we use ANSI escape codes to colour the output?
colour : Bool
open Options
initOptions : String → Options
initOptions exe = record
{ exeUnderTest = exe
; onlyNames = []
; interactive = false
; timing = false
; failureFile = nothing
; colour = true
}
usage : String
usage = unwords
$ "Usage:"
∷ "runtests <path>"
∷ "[--timing]"
∷ "[--interactive]"
∷ "[--failure-file PATH]"
∷ "[--only-file PATH]"
∷ "[--no-colour]"
∷ "[--only [NAMES]]"
∷ []
data Error : Set where
MissingExecutable : Error
InvalidArgument : String → Error
show : Error → String
show MissingExecutable = "Expected a path to Agda, got nothing"
show (InvalidArgument arg) = "Invalid argument: " String.++ arg
-- Process the command line options
options : List String → IO (Error ⊎ Options)
options(exe ∷ rest) = mkOptions exe rest where
go : List String → Maybe String → Options → String ⊎ (Maybe String × Options)
go [] mfp opts = inj₂ (mfp , opts)
go ("--timing" ∷ args) mfp opts =
go args mfp (record opts { timing = true })
go ("--interactive" ∷ args) mfp opts =
go args mfp (record opts { interactive = true })
go ("--failure-file" ∷ fp ∷ args) mfp opts =
go args mfp (record opts { failureFile = just fp })
go ("--only" ∷ args) mfp opts =
inj₂ (mfp , (record opts { onlyNames = args }))
go ("--only-file" ∷ fp ∷ args) mfp opts =
go args (just fp) (record opts { onlyNames = args })
go ("--no-colour" ∷ args) mfp opts =
go args mfp (record opts { colour = false })
go (arg ∷ _) _ _ = inj₁ arg
mkOptions : String → List String → IO (Error ⊎ Options)
mkOptions exe rest = do
inj₂ (mfp , opts) ← pure $ go rest nothing (initOptions exe)
where inj₁ arg → pure (inj₁ (InvalidArgument arg))
term ← fromMaybe "" <$> lookupEnv "TERM"
let opts = if does (term ≟ "DUMB")
then record opts { colour = false }
else opts
just fp ← pure mfp
where _ → pure (inj₂ opts)
only ← readFiniteFile fp
pure $ inj₂ $ record opts { onlyNames = lines only ++ onlyNames opts }
options [] = pure (inj₁ MissingExecutable)
-- The result of a test run
-- `Left` corresponds to a failure and `Right` to a success
Result : Set
Result = String ⊎ String
-- Run the specified golden test with the supplied options.
runTest : Options → String → IO Result
runTest opts testPath = do
true ← doesDirectoryExist (mkFilePath testPath)
where false → fail directoryNotFound
time ← time′ $ callCommand $ unwords
$ "cd" ∷ testPath
∷ "&&" ∷ "sh ./run" ∷ opts .exeUnderTest
∷ "| tr -d '\\r' > output"
∷ []
just out ← readLocalFile "output"
where nothing → fail (fileNotFound "output")
just exp ← readLocalFile "expected"
where nothing → do if opts .interactive
then mayOverwrite nothing out
else putStrLn (fileNotFound "expected")
pure (inj₁ testPath)
let result = does (out String.≟ exp)
if result
then printTiming (opts .timing) time
$ if opts .colour
then withCommand (setColour foreground classic green)
else id
$ "success"
else do printTiming (opts .timing) time
$ if opts .colour
then withCommand (setColour foreground bright red)
else id
$ "FAILURE"
if opts .interactive
then mayOverwrite (just exp) out
else putStrLn (unlines (expVsOut exp out))
pure $ if result then inj₂ testPath else inj₁ testPath
where
directoryNotFound : String
directoryNotFound = unwords
$ "Directory"
∷ testPath
∷ "does not exist" ∷ []
fileNotFound : String → String
fileNotFound name = unwords
$ "File"
∷ (testPath String.++ "/output")
∷ "does not exist" ∷ []
fail : String → IO Result
fail msg = do putStrLn msg
pure (inj₁ testPath)
readLocalFile : String → IO (Maybe String)
readLocalFile name = do
let fp = concat (testPath ∷ "/" ∷ name ∷ [])
true ← doesFileExist (mkFilePath fp)
where false → pure nothing
just <$> readFiniteFile fp
getAnswer : IO Bool
getAnswer = untilJust $ do
str ← getLine
case str of λ where
"y" → pure $ just true
"n" → pure $ just false
"" → pure $ just false -- default answer is no
_ → do putStrLn "Invalid answer."
pure nothing
expVsOut : String → String → List String
expVsOut exp out = "Expected:" ∷ exp ∷ "Given:" ∷ out ∷ []
hasFailed : ExitCode → Bool
hasFailed ExitSuccess = false
hasFailed (ExitFailure code) = code ℤ.≤ᵇ ℤ.+ 0
mayOverwrite : Maybe String → String → IO _
mayOverwrite mexp out = do
case mexp of λ where
nothing → putStrLn $ unlines
$ "Golden value missing. I computed the following result:"
∷ out
∷ "Accept new golden value? [y/N]"
∷ []
(just exp) → do
code ← system $ concat
$ "git diff --no-index --exit-code --word-diff=color "
∷ testPath ∷ "/expected "
∷ testPath ∷ "/output"
∷ []
putStrLn $ unlines
$ "Golden value differs from actual value."
∷ (if hasFailed code then expVsOut exp out else [])
++ "Accept actual value as new golden value? [y/N]"
∷ []
b ← getAnswer
when b $ writeFile (testPath String.++ "/expected") out
printTiming : Bool → Time → String → IO _
printTiming false _ msg = putStrLn $ concat (testPath ∷ ": " ∷ msg ∷ [])
printTiming true time msg =
let time = ℕ.show (time .seconds) String.++ "s"
spent = 9 + sum (List.map String.length (testPath ∷ time ∷ []))
-- ^ hack: both "success" and "FAILURE" have the same length
-- can't use `String.length msg` because the msg contains escape codes
pad = String.replicate (72 ∸ spent) ' '
in putStrLn (concat (testPath ∷ ": " ∷ msg ∷ pad ∷ time ∷ []))
-- A test pool is characterised by
-- + a name
-- + and a list of directory paths
record TestPool : Set where
constructor mkTestPool
field
poolName : String
testCases : List String
open TestPool
module Summary where
-- The summary of a test pool run
record Summary : Set where
constructor mkSummary
field
success : List String
failure : List String
open Summary public
init : Summary
init = mkSummary [] []
merge : Summary → Summary → Summary
merge (mkSummary ws1 ls1) (mkSummary ws2 ls2) =
mkSummary (ws2 ++ ws1) (ls2 ++ ls1)
update : List Result → Summary → Summary
update res sum =
let (ls2 , ws2) = partitionSums res in
merge sum (mkSummary ws2 ls2)
open Summary using (Summary) hiding (module Summary)
-- Only keep the tests that have been asked for
filterTests : Options → List String → List String
filterTests opts = case onlyNames opts of λ where
[] → id
xs → let names = List.map String.toList xs in
filter (λ n → any? (λ m → infix? Char._≟_ m (String.toList n)) names)
poolRunner : Options → TestPool → IO Summary
poolRunner opts pool = do
-- check there is a non-empty list of tests we want to run
let tests = filterTests opts (pool .testCases)
(_ ∷ _) ← pure tests
where [] → pure Summary.init
-- announce the test pool and run them
putStrLn banner
loop Summary.init tests
where
separator : String
separator = String.replicate 72 '-'
banner : String
banner = unlines
$ "" ∷ separator
∷ pool .poolName
∷ separator ∷ ""
∷ []
loop : Summary → List String → IO Summary
loop acc [] = pure acc
loop acc (test ∷ tests) = do
res <- runTest opts test
loop (Summary.update (res ∷ []) acc) tests
runner : List TestPool → IO ⊤
runner tests = do
-- figure out the options
args ← getArgs
inj₂ opts ← options args
where inj₁ err → die (unlines (show err ∷ usage ∷ []))
-- run the tests
ress ← List.mapM (poolRunner opts) tests
let open Summary
let res = List.foldl merge init ress
-- report the result
let nsucc = List.length (res .success)
let nfail = List.length (res .failure)
let ntotal = nsucc + nfail
putStrLn $ concat $ ℕ.show nsucc ∷ "/" ∷ ℕ.show ntotal ∷ " tests successful" ∷ []
-- deal with failures
let list = unlines (res .failure)
when (0 <ᵇ nfail) $ do
putStrLn "Failing tests:"
putStrLn list
whenJust (opts .failureFile) $ λ fp → writeFile fp list
-- exit
if 0 ≡ᵇ nfail
then exitSuccess
else exitFailure
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4