idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-08-16 08:40:37 +03:00
Code Issues Projects Releases Wiki Activity

Add a test package to the Idris 2 project (#1162)

Browse Source
This commit is contained in:
Mathew Polzin 2021-03-09 10:27:05 -08:00 committed by GitHub
parent 50c60185a7
commit 06586d401a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
15 changed files with 110 additions and 338 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
.gitignore vendored
View File

@ -41,3 +41,6 @@ idris2docs_venv
/bootstrap/idris2-boot.rkt
/custom.mk
#Mac OS
.DS_Store

7
CHANGELOG.md
View File

@ -1,6 +1,13 @@
Changes since Idris 2 v0.3.0
============================
Library changes:
* Introduced `test` package.
- Moved `tests/Lib.idr` into new `test` package as `Test/Golden.idr`.
- Removed `contrib/Test/Golden.idr` which duplicated the test framework now in the `test` package.
REPL/IDE mode changes:
* Added `:search` command, which searches for functions by type

17
Makefile
View File

@ -42,14 +42,14 @@ IDRIS2_BOOT_TEST_LIBS := ${IDRIS2_CURDIR}/bootstrap/${NAME}-${IDRIS2_VERSION}/li
IDRIS2_BOOT_TEST_DATA := ${IDRIS2_CURDIR}/bootstrap/${NAME}-${IDRIS2_VERSION}/support
# These are the library path in the build dir to be used during build
export IDRIS2_BOOT_PATH := "${IDRIS2_CURDIR}/libs/prelude/build/ttc${SEP}${IDRIS2_CURDIR}/libs/base/build/ttc${SEP}${IDRIS2_CURDIR}/libs/contrib/build/ttc${SEP}${IDRIS2_CURDIR}/libs/network/build/ttc"
export IDRIS2_BOOT_PATH := "${IDRIS2_CURDIR}/libs/prelude/build/ttc${SEP}${IDRIS2_CURDIR}/libs/base/build/ttc${SEP}${IDRIS2_CURDIR}/libs/contrib/build/ttc${SEP}${IDRIS2_CURDIR}/libs/network/build/ttc${SEP}${IDRIS2_CURDIR}/libs/test/build/ttc"
export SCHEME
.PHONY: all idris2-exec ${TARGET} testbin support support-clean clean distclean FORCE
all: support ${TARGET} testbin libs
all: support ${TARGET} libs
idris2-exec: ${TARGET}
@ -74,13 +74,16 @@ base: prelude
network: prelude
${MAKE} -C libs/network IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
contrib: prelude
contrib: base
${MAKE} -C libs/contrib IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
libs : prelude base contrib network
test-lib: contrib
${MAKE} -C libs/test IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
testbin:
@${MAKE} -C tests testbin
libs : prelude base contrib network test-lib
testbin: test-lib install
@${MAKE} -C tests testbin IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
test: testbin
@echo
@ -102,6 +105,7 @@ clean-libs:
${MAKE} -C libs/base clean
${MAKE} -C libs/contrib clean
${MAKE} -C libs/network clean
${MAKE} -C libs/test clean
clean: clean-libs support-clean
-${IDRIS2_BOOT} --clean ${IDRIS2_APP_IPKG}
@ -142,6 +146,7 @@ install-libs:
${MAKE} -C libs/base install IDRIS2?=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/contrib install IDRIS2?=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/network install IDRIS2?=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/test install IDRIS2?=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
.PHONY: bootstrap bootstrap-build bootstrap-racket bootstrap-racket-build bootstrap-test bootstrap-clean

2
Release/CHECKLIST
View File

@ -1,6 +1,6 @@
[ ] Change version number (MAJOR, MINOR, PATCH) in Makefile
[ ] Change version numbers in doc listings
[ ] Change version numbers in prelude, base, contrib, network ipkgs
[ ] Change version numbers in prelude, base, contrib, network, and test ipkgs
[ ] Update bootstrap chez and racket
[ ] Tag on github with version number (in the form vX.Y.Z)
[ ] Run release script

2
bootstrap-stage2.sh
View File

@ -16,7 +16,7 @@ fi
IDRIS2_CG="${IDRIS2_CG-"chez"}"
BOOT_PATH_BASE=$IDRIS_PREFIX/idris2-$IDRIS2_VERSION
IDRIS2_BOOT_PATH="$BOOT_PATH_BASE/prelude$SEP $BOOT_PATH_BASE/base$SEP $BOOT_PATH_BASE/contrib$SEP $BOOT_PATH_BASE/network"
IDRIS2_BOOT_PATH="$BOOT_PATH_BASE/prelude$SEP $BOOT_PATH_BASE/base$SEP $BOOT_PATH_BASE/contrib$SEP $BOOT_PATH_BASE/network $BOOT_PATH_BASE/test"
# PREFIX must be the "clean" build root, without cygpath -m
# Otherwise, we get 'git: Bad address'

2
libs/contrib/Test/REDIRECT.md Normal file
View File

@ -0,0 +1,2 @@
# Where did contrib's `Test.Golden` go?
You can find the same module as part of the new `test` package. Just add `test` to your package file's `depends` section or launch Idris2 with `-p test` and `import Test.Golden` to get the same module.

2
libs/contrib/contrib.ipkg
View File

@ -134,8 +134,6 @@ modules = Control.ANSI,
System.Random,
System.Path,
Test.Golden,
Text.Token,
Text.Quantity,
Text.Parser,

8
libs/test/Makefile Normal file
View File

@ -0,0 +1,8 @@
all:
${IDRIS2} --build test.ipkg
install:
${IDRIS2} --install test.ipkg
clean:
$(RM) -r build

59
libs/test/README.md Normal file
View File

@ -0,0 +1,59 @@
# Test
The test package exposes the same test framework(s) the Idris 2 compiler uses for its test suite.
In a language like Idris 2, there are a number of strategies one can take for testing their code and the eventual goal of this testing package is to facilitate a blend of these strategies in any project. Currently the package contains one module facilitating one style of testing: `Golden`. Contributions containing other modules that enable additional testing styles are encouraged.
To use the test package, either pass `-p test` to the idris2 executable or add `depends = test` to your test suite's package file.
## Golden
Golden facilitates testing by way of comparing test output with a predetermined expecation. The module is well documented in its own source code but the following is a primer.
You first import the `Test.Golden` module and write an `IO` function to serve as the entrypoint for your test suite. This function must at some point call into Golden's `runner`.
```idris
-- your_project/tests/Main.idr
module Main
import Test.Golden
tests : TestPool
main : IO ()
main = do
runner [tests]
```
You populate the `TestPool` list that the `runner` expects with one entry per pool of tests you want to run. Within each pool, tests are run concurrently.
```idris
tests : TestPool
tests = MkTestPool [] [
"my_great_test"
]
```
The first argument to `MkTestPool` (empty in the above example) is a list of codegen backends required to run the tests in the given pool. Any empty list means no requirements. If your tests required the Racket backend, you could instead specify `[Racket]`. See the [`Requirement` type](./Test/Golden.idr#L228) for more.
The second argument to `MkTestPool` is a list of directory names that can be found relative to your `Main.idr` file. This directory will have some combination of the following files.
```Shell
my_great_test/
Test.idr
test.ipkg
expected
input
run
```
These files define:
1. Any Idris 2 source code needed for the test (Test.idr, which can be named anything you'd like and is not limited to 1 file).
2. Any package information needed to build those source files (test.ipkg).
3. The command run at the shell to execute your test (run).
4. Optional input passed to your test case (input).
5. The expected output of running your test (expected).
See the [documentation](./Test/Golden.idr#L12) in `Test/Golden.idr` and the [template directories](../../tests/templates) provided with the Idris 2 project for a great primer on these files.
When you run your tests (the executable produced by building your `tests/Main.idr` file), you need to specify the Idris executable to use and optionally use interactive mode (`--interactive`) or limit the test cases that are run (`--only [names]`).
Interactive mode is useful when you know the expected output for a test case is going to change -- you will be prompted to updated the expectation so you can choose whether the output produced by a new test run should become the new "golden" standard.
You can even skip the step of creating an `expected` file altogether when you write a new test case and use interactive mode to accept the output of your test case as the expectation.

12
libs/contrib/Test/Golden.idr → libs/test/Test/Golden.idr
View File

@ -136,7 +136,7 @@ normalize str =
|||
||| See the module documentation for more information.
|||
||| @testpath the directory that contains the test.
||| @testPath the directory that contains the test.
export
runTest : Options -> String -> IO (Future Bool)
runTest opts testPath = forkIO $ do
@ -225,14 +225,15 @@ pathLookup names = do
||| Some test may involve Idris' backends and have requirements.
||| We define here the ones supported by Idris
public export
data Requirement = Chez | Node | Racket | C
data Requirement = C | Chez | Node | Racket | Gambit
export
Show Requirement where
show C = "C"
show Chez = "Chez"
show Node = "node"
show Racket = "racket"
show C = "C"
show Gambit = "gambit"
export
checkRequirement : Requirement -> IO (Maybe String)
@ -243,10 +244,11 @@ checkRequirement req
where
requirement : Requirement -> (String, List String)
requirement C = ("CC", ["cc"])
requirement Chez = ("CHEZ", ["chez", "chezscheme9.5", "scheme", "scheme.exe"])
requirement Node = ("NODE", ["node"])
requirement Racket = ("RACKET", ["racket"])
requirement C = ("CC", ["cc"])
requirement Gambit = ("GAMBIT", ["gsc"])
export
findCG : IO (Maybe String)
@ -255,6 +257,7 @@ findCG
Nothing <- checkRequirement Chez | p => pure (Just "chez")
Nothing <- checkRequirement Node | p => pure (Just "node")
Nothing <- checkRequirement Racket | p => pure (Just "racket")
Nothing <- checkRequirement Gambit | p => pure (Just "gsc")
Nothing <- checkRequirement C | p => pure (Just "refc")
pure Nothing
@ -294,6 +297,7 @@ poolRunner opts pool
-- if so run them all!
map await <$> traverse (runTest opts) tests
||| A runner for a whole test suite
export
runner : List TestPool -> IO ()

7
libs/test/test.ipkg Normal file
View File

@ -0,0 +1,7 @@
package test
version = 0.3.0
opts = "--ignore-missing-ipkg -p contrib"
modules = Test.Golden

2
package.nix
View File

@ -31,7 +31,7 @@ stdenv.mkDerivation rec {
# TODO: Move this into its own derivation, such that this can be changed
# without having to recompile idris2 every time.
postInstall = let
includedLibs = [ "base" "contrib" "network" "prelude" ];
includedLibs = [ "base" "contrib" "network" "prelude" "test" ];
name = "${pname}-${version}";
packagePaths = builtins.map (l: "$out/${name}/${l}-${version}") includedLibs;
additionalIdris2Paths = builtins.concatStringsSep ":" packagePaths;

321
tests/Lib.idr
View File

@ -1,321 +0,0 @@
||| 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.
|||
||| This was originally used as part of Idris2's own test suite and
||| the core functionality is useful for the many and not the few.
||| Please see Idris2 test harness for example usage.
|||
||| # 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 idris executable to be tested
||| * May use `${IDRIS2_TESTS_CG}` to pick a codegen that ought to work
||| * Clean up after itself (e.g. by running `rm -rf build/`)
|||
||| + `expected` a file containting the expected output of `run`
|||
||| During testing, the test harness will generate an artefact named `output` and
||| display both outputs if there is a failure.
||| During an interactive session the following command is used to compare them as
||| they are:
|||
||| ```sh
||| 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 if `output` was added to a local `.gitignore` instance
||| to ensure that it is not mistakenly versioned.
|||
||| # Options
|||
||| The test harness has several options that may be set:
|||
||| + `idris2` The path of the executable we are testing.
||| + `onlyNames` The list of 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.
|||
||| We provide an options parser (`options`) that will take the 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 [NAMES]]
|||```
|||
||| assuming that the test runner is compiled to an executable named `runtests`.
module Lib
import Data.Maybe
import Data.List
import Data.List1
import Data.Strings
import System
import System.Clock
import System.Directory
import System.File
import System.Future
import System.Info
import System.Path
-- [ Options ]
||| Options for the test driver.
public export
record Options where
constructor MkOptions
||| Name of the idris2 executable
exeUnderTest : String
||| Which codegen should we use?
codegen : Maybe 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
export
usage : String -> String
usage exe = unwords ["Usage:", exe, "runtests <path> [--timing] [--interactive] [--cg CODEGEN] [--only [NAMES]]"]
||| Process the command line options.
export
options : List String -> Maybe Options
options args = case args of
(_ :: exeUnderTest :: rest) => go rest (MkOptions exeUnderTest Nothing [] False False)
_ => 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)
("--only" :: xs) => pure $ record { onlyNames = xs } opts
_ => Nothing
-- [ Core ]
export
fail : String -> IO ()
fail err
= do putStrLn err
exitWith (ExitFailure 1)
||| Normalise strings between different OS.
|||
||| on Windows, we just ignore backslashes and slashes when comparing,
||| similarity up to that is good enough. Leave errors that depend
||| on the confusion of slashes and backslashes to unix machines.
normalize : String -> String
normalize str =
if isWindows
then pack $ filter (\ch => ch /= '/' && ch /= '\\') (unpack str)
else str
||| 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 opts testPath = forkIO $ do
start <- clockTime Thread
let cg = case codegen opts of
Nothing => ""
Just cg => "env IDRIS2_TESTS_CG=" ++ cg ++ " "
ignore $ system $ "cd " ++ testPath ++ " && " ++
cg ++ "sh ./run " ++ exeUnderTest opts ++ " | tr -d '\\r' > output"
end <- clockTime Thread
Right out <- readFile $ testPath ++ "/output"
| Left err => do print err
pure False
Right exp <- readFile $ testPath ++ "/expected"
| Left FileNotFound => do
if interactive opts
then mayOverwrite Nothing out
else print FileNotFound
pure False
| Left err => do print err
pure False
let result = normalize out == normalize exp
let time = timeDifference end start
if result
then printTiming (timing opts) time $ testPath ++ ": success"
else do
printTiming (timing opts) time $ testPath ++ ": FAILURE"
if interactive opts
then mayOverwrite (Just exp) out
else putStrLn . unlines $ expVsOut exp out
pure result
where
getAnswer : IO Bool
getAnswer = do
str <- getLine
case str of
"y" => pure True
"n" => pure False
_ => do putStrLn "Invalid Answer."
getAnswer
expVsOut : String -> String -> List String
expVsOut exp out = ["Expected:", exp, "Given:", out]
mayOverwrite : Maybe String -> String -> IO ()
mayOverwrite mexp out = do
case mexp of
Nothing => putStr $ unlines
[ "Golden value missing. I computed the following result:"
, out
, "Accept new golden value? [yn]"
]
Just exp => do
code <- system $ "git diff --no-index --exit-code --word-diff=color " ++
testPath ++ "/expected " ++ testPath ++ "/output"
putStrLn . unlines $
["Golden value differs from actual value."] ++
(if (code < 0) then expVsOut exp out else []) ++
["Accept actual value as new golden value? [yn]"]
b <- getAnswer
when b $ do Right _ <- writeFile (testPath ++ "/expected") out
| Left err => print err
pure ()
printTiming : Bool -> Clock type -> String -> IO ()
printTiming True clock msg = putStrLn (unwords [msg, show clock])
printTiming False _ msg = putStrLn msg
||| Find the first occurrence of an executable on `PATH`.
export
pathLookup : List String -> IO (Maybe String)
pathLookup names = do
path <- getEnv "PATH"
let pathList = forget $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
let candidates = [p ++ "/" ++ x | p <- pathList,
x <- names]
firstExists candidates
||| Some test may involve Idris' backends and have requirements.
||| We define here the ones supported by Idris
public export
data Requirement = C | Chez | Node | Racket | Gambit
export
Show Requirement where
show C = "C"
show Chez = "Chez"
show Node = "node"
show Racket = "racket"
show Gambit = "gambit"
export
checkRequirement : Requirement -> IO (Maybe String)
checkRequirement req
= do let (envvar, paths) = requirement req
Just exec <- getEnv envvar | Nothing => pathLookup paths
pure (Just exec)
where
requirement : Requirement -> (String, List String)
requirement C = ("CC", ["cc"])
requirement Chez = ("CHEZ", ["chez", "chezscheme9.5", "scheme", "scheme.exe"])
requirement Node = ("NODE", ["node"])
requirement Racket = ("RACKET", ["racket"])
requirement Gambit = ("GAMBIT", ["gsc"])
export
findCG : IO (Maybe String)
findCG
= do Nothing <- getEnv "IDRIS2_TESTS_CG" | p => pure p
Nothing <- checkRequirement Chez | p => pure (Just "chez")
Nothing <- checkRequirement Node | p => pure (Just "node")
Nothing <- checkRequirement Racket | p => pure (Just "racket")
Nothing <- checkRequirement Gambit | p => pure (Just "gsc")
Nothing <- checkRequirement C | p => pure (Just "refc")
pure Nothing
||| A test pool is characterised by
||| + a list of requirement
||| + and a list of directory paths
public export
record TestPool where
constructor MkTestPool
constraints : List Requirement
testCases : List String
||| Only keep the tests that have been asked for
export
filterTests : Options -> List String -> List String
filterTests opts = case onlyNames opts of
[] => id
xs => filter (\ name => any (`isInfixOf` name) xs)
||| A runner for a test pool
export
poolRunner : Options -> TestPool -> IO (List Bool)
poolRunner opts pool
= do -- check that we indeed want to run some of these tests
let tests = filterTests opts (testCases pool)
let (_ :: _) = tests
| [] => pure []
-- if so make sure the constraints are satisfied
cs <- for (constraints pool) $ \ req => do
mfp <- checkRequirement req
putStrLn $ case mfp of
Nothing => show req ++ " not found"
Just fp => "Found " ++ show req ++ " at " ++ fp
pure mfp
let Just _ = the (Maybe (List String)) (sequence cs)
| Nothing => pure []
-- if so run them all!
map await <$> traverse (runTest opts) tests
||| 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")
-- 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
-- [ EOF ]

2
tests/Main.idr
View File

@ -11,7 +11,7 @@ import System.File
import System.Info
import System.Path
import Lib
import Test.Golden
%default covering

2
tests/tests.ipkg
View File

@ -1,5 +1,5 @@
package runtests
depends = contrib
depends = test
main = Main
executable = runtests