tjh.dev
1{
2 stdenv,
3 runCommand,
4 lib,
5 pname,
6 idris2,
7 idris2Packages,
8 zsh,
9 tree,
10}:
11
12let
13 testCompileAndRun =
14 {
15 testName,
16 code,
17 want,
18 packages ? [ ],
19 }:
20 let
21 packageString = builtins.concatStringsSep " " (map (p: "--package " + p) packages);
22 in
23 runCommand "${pname}-${testName}"
24 {
25 meta.timeout = 60;
26
27 # with idris2 compiled binaries assume zsh is available on darwin, but that
28 # is not the case with pure nix environments. Thus, we need to include zsh
29 # when we build for darwin in tests. While this is impure, this is also what
30 # we find in real darwin hosts.
31 nativeBuildInputs = lib.optionals stdenv.hostPlatform.isDarwin [ zsh ];
32 }
33 ''
34 set -eo pipefail
35
36 cat > packageTest.idr <<HERE
37 ${code}
38 HERE
39
40 ${idris2}/bin/idris2 ${packageString} -o packageTest packageTest.idr
41
42 GOT=$(./build/exec/packageTest)
43
44 if [ "$GOT" = "${want}" ]; then
45 echo "${testName} SUCCESS: '$GOT' = '${want}'"
46 else
47 >&2 echo "Got '$GOT', want: '${want}'"
48 exit 1
49 fi
50
51 touch $out
52 '';
53
54 testBuildIdris =
55 {
56 testName,
57 buildIdrisArgs,
58 # function that takes result of `buildIdris` and transforms it (commonly
59 # by calling `.executable` or `.library {}` upon it):
60 transformBuildIdrisOutput,
61 expectedTree,
62 }:
63 let
64 idrisPkg = transformBuildIdrisOutput (idris2Packages.buildIdris buildIdrisArgs);
65 in
66 runCommand "${pname}-${testName}"
67 {
68 meta.timeout = 60;
69
70 nativeBuildInputs = [ tree ];
71 }
72 ''
73 GOT="$(tree ${idrisPkg} | tail -n +2)"
74
75 if [ "$GOT" = '${expectedTree}' ]; then
76 echo "${testName} SUCCESS"
77 else
78 >&2 echo "Got:
79 $GOT"
80 >&2 echo 'want:
81 ${expectedTree}'
82 exit 1
83 fi
84
85 touch $out
86 '';
87in
88{
89 # Simple hello world compiles, runs and outputs as expected
90 helloWorld = testCompileAndRun {
91 testName = "hello-world";
92 code = ''
93 module Main
94
95 main : IO ()
96 main = putStrLn "Hello World!"
97 '';
98 want = "Hello World!";
99 };
100
101 # Data.Vect.Sort is available via --package contrib
102 useContrib = testCompileAndRun {
103 testName = "use-contrib";
104 packages = [ "contrib" ];
105 code = ''
106 module Main
107
108 import Data.Vect
109 import Data.Vect.Sort -- from contrib
110
111 vect : Vect 3 Int
112 vect = 3 :: 1 :: 5 :: Nil
113
114 main : IO ()
115 main = putStrLn $ show (sort vect)
116 '';
117 want = "[1, 3, 5]";
118 };
119
120 buildLibrary = testBuildIdris {
121 testName = "library-package";
122 buildIdrisArgs = {
123 ipkgName = "pkg";
124 idrisLibraries = [ idris2Packages.idris2Api ];
125 src = runCommand "library-package-src" { } ''
126 mkdir $out
127
128 cat > $out/Main.idr <<EOF
129 module Main
130
131 import Compiler.ANF -- from Idris2Api
132
133 hello : String
134 hello = "world"
135 EOF
136
137 cat > $out/pkg.ipkg <<EOF
138 package pkg
139 modules = Main
140 depends = idris2
141 EOF
142 '';
143 };
144 transformBuildIdrisOutput = pkg: pkg.library { withSource = false; };
145 expectedTree = ''
146 `-- lib
147 `-- idris2-0.7.0
148 `-- pkg-0
149 |-- 2023090800
150 | |-- Main.ttc
151 | `-- Main.ttm
152 `-- pkg.ipkg
153
154 5 directories, 3 files'';
155 };
156
157 buildLibraryWithSource = testBuildIdris {
158 testName = "library-with-source-package";
159 buildIdrisArgs = {
160 ipkgName = "pkg";
161 idrisLibraries = [ idris2Packages.idris2Api ];
162 src = runCommand "library-package-src" { } ''
163 mkdir $out
164
165 cat > $out/Main.idr <<EOF
166 module Main
167
168 import Compiler.ANF -- from Idris2Api
169
170 hello : String
171 hello = "world"
172 EOF
173
174 cat > $out/pkg.ipkg <<EOF
175 package pkg
176 modules = Main
177 depends = idris2
178 EOF
179 '';
180 };
181 transformBuildIdrisOutput = pkg: pkg.library { withSource = true; };
182 expectedTree = ''
183 `-- lib
184 `-- idris2-0.7.0
185 `-- pkg-0
186 |-- 2023090800
187 | |-- Main.ttc
188 | `-- Main.ttm
189 |-- Main.idr
190 `-- pkg.ipkg
191
192 5 directories, 4 files'';
193 };
194
195 buildLibraryWithSourceRetroactively = testBuildIdris {
196 testName = "library-with-source-retro-package";
197 buildIdrisArgs = {
198 ipkgName = "pkg";
199 idrisLibraries = [ idris2Packages.idris2Api ];
200 src = runCommand "library-package-src" { } ''
201 mkdir $out
202
203 cat > $out/Main.idr <<EOF
204 module Main
205
206 import Compiler.ANF -- from Idris2Api
207
208 hello : String
209 hello = "world"
210 EOF
211
212 cat > $out/pkg.ipkg <<EOF
213 package pkg
214 modules = Main
215 depends = idris2
216 EOF
217 '';
218 };
219 transformBuildIdrisOutput = pkg: pkg.library'.withSource;
220 expectedTree = ''
221 `-- lib
222 `-- idris2-0.7.0
223 `-- pkg-0
224 |-- 2023090800
225 | |-- Main.ttc
226 | `-- Main.ttm
227 |-- Main.idr
228 `-- pkg.ipkg
229
230 5 directories, 4 files'';
231 };
232
233 buildExecutable = testBuildIdris {
234 testName = "executable-package";
235 buildIdrisArgs = {
236 ipkgName = "pkg";
237 idrisLibraries = [ ];
238 src = runCommand "executable-package-src" { } ''
239 mkdir $out
240
241 cat > $out/Main.idr <<EOF
242 module Main
243
244 main : IO ()
245 main = putStrLn "hi"
246 EOF
247
248 cat > $out/pkg.ipkg <<EOF
249 package pkg
250 modules = Main
251 main = Main
252 executable = mypkg
253 EOF
254 '';
255 };
256 transformBuildIdrisOutput = pkg: pkg.executable;
257 expectedTree = ''
258 `-- bin
259 `-- mypkg
260
261 2 directories, 1 file'';
262 };
263}