1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
|
{ stdenv, lib, pname, idris2, zsh }:
let
testCompileAndRun = {testName, code, want, packages ? []}: let
packageString = builtins.concatStringsSep " " (map (p: "--package " + p) packages);
in stdenv.mkDerivation {
name = "${pname}-${testName}";
meta.timeout = 60;
# with idris2 compiled binaries assume zsh is available on darwin, but that
# is not the case with pure nix environments. Thus, we need to include zsh
# when we build for darwin in tests. While this is impure, this is also what
# we find in real darwin hosts.
nativeBuildInputs = lib.optional stdenv.isDarwin [ zsh ];
buildCommand = ''
set -eo pipefail
cat > packageTest.idr <<HERE
${code}
HERE
${idris2}/bin/idris2 ${packageString} -o packageTest packageTest.idr
GOT=$(./build/exec/packageTest)
if [ "$GOT" = "${want}" ]; then
echo "${testName} SUCCESS: '$GOT' = '${want}'"
else
>&2 echo "Got '$GOT', want: '${want}'"
exit 1
fi
touch $out
'';
};
in {
# Simple hello world compiles, runs and outputs as expected
hello-world = testCompileAndRun {
testName = "hello-world";
code = ''
module Main
main : IO ()
main = putStrLn "Hello World!"
'';
want = "Hello World!";
};
# Data.Vect.Sort is available via --package contrib
use-contrib = testCompileAndRun {
testName = "use-contrib";
code = ''
module Main
import Data.Vect
import Data.Vect.Sort -- from contrib
vect : Vect 3 Int
vect = 3 :: 1 :: 5 :: Nil
main : IO ()
main = putStrLn $ show (sort vect)
'';
want = "[1, 3, 5]";
};
}
|