git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3201 from jfdm/testing-adjustments

Testing adjustments

commitb1a42b3891de21ad288b060e9e4f8d0abd161353 authorEdwin Brady <edwin.brady@gmail.com> dateFri 3 Jun 2016, 16:55 (10 years ago) parentc2446faf43e36e
67 files changed+59−146
compare with master
unifiedsplit
idris.cabal+7−62 test/README−19 test/README.md+39 test/reg001/run−4 test/reg036/expected test/reg036/run−3 test/reg037/expected test/reg037/run−3 test/reg038/expected test/reg038/run−3 test/reg046/expected test/reg046/run−3 test/reg047/expected test/reg047/run−4 test/reg053/expected test/reg053/run−3 test/reg057/expected test/reg057/run−3 test/reg058/expected test/reg058/run−5 test/reg059/expected test/reg059/run−3 test/reg060/expected test/reg060/run−3 test/reg061/expected test/reg061/run−3 test/reg062/expected test/reg062/run−4 test/reg063/expected test/reg063/run−3 test/reg064/expected test/reg064/run−3 test/reg065/expected test/reg065/run−3 test/reg066/expected test/reg066/run−3 test/reg071/expected test/reg071/run−3 test/reg073/expected test/reg073/run−3 test/reg074/expected test/reg074/run−3 test/reg001/expected → test/regression001/expected test/reg001/reg001.idr → test/regression001/reg001.idr test/reg036/reg036.idr → test/regression001/reg036.idr test/reg037/reg037.idr → test/regression001/reg037.idr test/reg038/reg038.idr → test/regression001/reg038.idr test/reg046/reg046.idr → test/regression001/reg046.idr test/reg047/reg047.idr → test/regression001/reg047.idr test/reg047/reg047a.idr → test/regression001/reg047a.idr test/reg053/four.idr → test/regression001/reg053.idr test/reg057/reg057.idr → test/regression001/reg057.idr test/reg058/implicits.idr → test/regression001/reg058.idr test/reg058/implicits2.idr → test/regression001/reg058a.idr test/reg059/reg059.idr → test/regression001/reg059.idr test/reg060/reg060.idr → test/regression001/reg060.idr test/reg061/Capture.idr → test/regression001/reg061.idr test/reg062/reg062.idr → test/regression001/reg062.idr test/reg062/reg062.lidr → test/regression001/reg062.lidr test/reg063/Cmp.idr → test/regression001/reg063.idr test/reg064/reg064.idr → test/regression001/reg064.idr test/reg065/reg065.idr → test/regression001/reg065.idr test/reg066/reg066.idr → test/regression001/reg066.idr test/reg071/reg071.idr → test/regression001/reg071.idr test/reg073/reg073.lidr → test/regression001/reg073.lidr test/reg074/reg074.idr → test/regression001/reg074.idr test/regression001/run+13
idris.cabal+7−62
@@ -157,9 +157,12 @@ Extra-source-files:
157157
158158 test/Makefile
159159 test/runtest.hs
160− test/reg001/run
161− test/reg001/*.idr
162− test/reg001/expected
160+
161+ test/regression001/run
162+ test/regression001/expected
163+ test/regression001/*.idr
164+ test/regression001/*.lidr
165+
163166 test/reg002/run
164167 test/reg002/*.idr
165168 test/reg002/expected
@@ -227,15 +230,6 @@ Extra-source-files:
227230 test/reg035/*.idr
228231 test/reg035/*.lidr
229232 test/reg035/expected
230− test/reg036/run
231− test/reg036/*.idr
232− test/reg036/expected
233− test/reg037/run
234− test/reg037/*.idr
235− test/reg037/expected
236− test/reg038/run
237− test/reg038/*.idr
238− test/reg038/expected
239233 test/reg039/run
240234 test/reg039/*.idr
241235 test/reg039/expected
@@ -254,12 +248,6 @@ Extra-source-files:
254248 test/reg045/run
255249 test/reg045/*.idr
256250 test/reg045/expected
257− test/reg046/run
258− test/reg046/*.idr
259− test/reg046/expected
260− test/reg047/run
261− test/reg047/*.idr
262− test/reg047/expected
263251 test/reg048/run
264252 test/reg048/*.idr
265253 test/reg048/expected
@@ -275,9 +263,6 @@ Extra-source-files:
275263 test/reg052/run
276264 test/reg052/*.idr
277265 test/reg052/expected
278− test/reg053/run
279− test/reg053/*.idr
280− test/reg053/expected
281266 test/reg054/run
282267 test/reg054/*.idr
283268 test/reg054/expected
@@ -287,36 +272,6 @@ Extra-source-files:
287272 test/reg056/run
288273 test/reg056/*.idr
289274 test/reg056/expected
290− test/reg057/run
291− test/reg057/*.idr
292− test/reg057/expected
293− test/reg058/run
294− test/reg058/*.idr
295− test/reg058/expected
296− test/reg059/run
297− test/reg059/*.idr
298− test/reg059/expected
299− test/reg060/run
300− test/reg060/*.idr
301− test/reg060/expected
302− test/reg061/run
303− test/reg061/*.idr
304− test/reg061/expected
305− test/reg062/run
306− test/reg062/*.idr
307− test/reg062/expected
308− test/reg063/run
309− test/reg063/*.idr
310− test/reg063/expected
311− test/reg064/run
312− test/reg064/*.idr
313− test/reg064/expected
314− test/reg065/run
315− test/reg065/*.idr
316− test/reg065/expected
317− test/reg066/run
318− test/reg066/*.idr
319− test/reg066/expected
320275 test/reg067/run
321276 test/reg067/*.idr
322277 test/reg067/expected
@@ -329,24 +284,14 @@ Extra-source-files:
329284 test/reg070/run
330285 test/reg070/*.idr
331286 test/reg070/expected
332− test/reg071/run
333− test/reg071/*.idr
334− test/reg071/expected
335287 test/reg072/run
336288 test/reg072/*.idr
337289 test/reg072/expected
338− test/reg073/run
339− test/reg073/*.lidr
340− test/reg073/expected
341− test/reg074/run
342− test/reg074/*.idr
343− test/reg074/expected
344290 test/reg075/run
345291 test/reg075/input
346292 test/reg075/*.idr
347293 test/reg075/expected
348294
349−
350295 test/basic001/run
351296 test/basic001/*.idr
352297 test/basic001/expected
@@ -880,7 +825,7 @@ Extra-source-files:
880825 test/views003/run
881826 test/views003/*.idr
882827 test/views003/expected
883−
828+
884829 test/universes001/run
885830 test/universes001/*.idr
886831 test/universes001/expected
test/READMEdeleted−19
@@ -1,19 +0,0 @@
1−Tests are categorised as follows:
2−
3−basic: Basic language features, some complete programs
4−bignum: Bignums and GMP
5−dsl: Embedded DSLs and features to support DSL development
6−effects: Effects package
7−error: Error messages and error reflection
8−ffi: FFI calls, including type providers
9−idrisdoc: Documentation tool functionality
10−interactive: Interactive editing, proof search
11−io: IO monad
12−literate: .lidr files; literate programming
13−primitives: Primitive types
14−proof: Theorem proving, tactics
15−sugar: Syntactic sugar, syntax extensions
16−totality: Totality checking
17−tutorial: Examples from the tutorial
18−
19−reg: Regression tests, covering previous bug fixes
test/README.mdnew file+39
@@ -0,0 +1,39 @@
1+# Idris' Testing Suite
2+
3+Tests are categorised as follows:
4+
5++ *basic*: Basic language features, some complete programs
6++ *bignum*: Bignums and GMP
7++ *bounded*: Bounds testing for bits
8++ *corecords*: Tests for corecord
9++ *delab*: De-elaboration tests
10++ *directives*: Tests for directives
11++ *docs*: Testing documentation functionality
12++ *dsl*: Embedded DSLs and features to support DSL development
13++ *effects*: Effects package
14++ *error*: Error messages and error reflection
15++ *ffi*: FFI calls, including type providers
16++ *folding* Testing some folds
17++ *idrisdoc*: Documentation tool functionality
18++ *interactive*: Interactive editing, proof search
19++ *interfaces*: Testing interfaces.
20++ *io*: IO monad
21++ *literate*: `.lidr` files; literate programming
22++ *meta*: Meta-programming
23++ *pkg*: Packages
24++ *primitives*: Primitive types
25++ *proof*: Theorem proving, tactics
26++ *proofsearch*: Proof search
27++ *pruviloj*: Elaborator reflection
28++ *quasiquote*: Quasiquotations
29++ *records*: Records
30++ *reg*: Regression tests, covering previous bug fixes
31++ *regression*: Regression tests, covering previous bug fixes
32++ *sourceLocation*: Interaction with files from Idris
33++ *sugar*: Syntactic sugar, syntax extensions
34++ *tactics*: Testing for tactics
35++ *totality*: Totality checking
36++ *tutorial*: Examples from the tutorial
37++ *unique*: Uniqueness types
38++ *universes*: Universes
39++ *views*: Views and covering functions
test/reg001/rundeleted−4
@@ -1,4 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} reg001.idr --check
3−rm -rf reg001.ibc
4−
test/reg036/expecteddeleted

No changes to the content.

test/reg036/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} --check reg036.idr
3−rm -f reg036 *.ibc
test/reg037/expecteddeleted

No changes to the content.

test/reg037/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} --check reg037.idr
3−rm -f reg037 *.ibc
test/reg038/expecteddeleted

No changes to the content.

test/reg038/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} --check reg038.idr
3−rm -f *.ibc
test/reg046/expecteddeleted

No changes to the content.

test/reg046/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg046.idr --check
3−rm -f reg046 *.ibc
test/reg047/expecteddeleted

No changes to the content.

test/reg047/rundeleted−4
@@ -1,4 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg047.idr --check --nobuiltins
3−${IDRIS:-idris} $@ reg047a.idr --check
4−rm -f *.ibc
test/reg053/expecteddeleted

No changes to the content.

test/reg053/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ --check four.idr
3−rm -f *.ibc
test/reg057/expecteddeleted

No changes to the content.

test/reg057/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg057.idr --check
3−rm -f *.ibc
test/reg058/expecteddeleted

No changes to the content.

test/reg058/rundeleted−5
@@ -1,5 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ implicits.idr --check
3−${IDRIS:-idris} $@ implicits2.idr --check
4−
5−rm -f *.ibc
test/reg059/expecteddeleted

No changes to the content.

test/reg059/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg059.idr --check
3−rm -f *.ibc
test/reg060/expecteddeleted

No changes to the content.

test/reg060/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg060.idr --check
3−rm -f *.ibc
test/reg061/expecteddeleted

No changes to the content.

test/reg061/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ Capture.idr --check
3−rm -f *.ibc
test/reg062/expecteddeleted

No changes to the content.

test/reg062/rundeleted−4
@@ -1,4 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg062.idr --check --nocolour
3−${IDRIS:-idris} $@ reg062.lidr --check --nocolour
4−rm -f *.ibc
test/reg063/expecteddeleted

No changes to the content.

test/reg063/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ Cmp.idr --check --nocolour --quiet
3−rm *.ibc
test/reg064/expecteddeleted

No changes to the content.

test/reg064/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg064.idr --check
3−rm -f *.ibc
test/reg065/expecteddeleted

No changes to the content.

test/reg065/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg065.idr --check
3−rm -f *.ibc
test/reg066/expecteddeleted

No changes to the content.

test/reg066/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg066.idr --check --nocolor
3−rm -f *.ibc
test/reg071/expecteddeleted

No changes to the content.

test/reg071/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg071.idr --check
3−rm -f *.ibc
test/reg073/expecteddeleted

No changes to the content.

test/reg073/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg073.lidr --check
3−rm -f *.ibc
test/reg074/expecteddeleted

No changes to the content.

test/reg074/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg074.idr --check
3−rm -f *.ibc
test/reg001/expected → test/regression001/expectedrenamed

The content is the same.

test/reg001/reg001.idr → test/regression001/reg001.idrrenamed

The content is the same.

test/reg036/reg036.idr → test/regression001/reg036.idrrenamed

The content is the same.

test/reg037/reg037.idr → test/regression001/reg037.idrrenamed

The content is the same.

test/reg038/reg038.idr → test/regression001/reg038.idrrenamed

The content is the same.

test/reg046/reg046.idr → test/regression001/reg046.idrrenamed

The content is the same.

test/reg047/reg047.idr → test/regression001/reg047.idrrenamed

The content is the same.

test/reg047/reg047a.idr → test/regression001/reg047a.idrrenamed

The content is the same.

test/reg053/four.idr → test/regression001/reg053.idrrenamed

The content is the same.

test/reg057/reg057.idr → test/regression001/reg057.idrrenamed

The content is the same.

test/reg058/implicits.idr → test/regression001/reg058.idrrenamed

The content is the same.

test/reg058/implicits2.idr → test/regression001/reg058a.idrrenamed

The content is the same.

test/reg059/reg059.idr → test/regression001/reg059.idrrenamed

The content is the same.

test/reg060/reg060.idr → test/regression001/reg060.idrrenamed

The content is the same.

test/reg061/Capture.idr → test/regression001/reg061.idrrenamed

The content is the same.

test/reg062/reg062.idr → test/regression001/reg062.idrrenamed

The content is the same.

test/reg062/reg062.lidr → test/regression001/reg062.lidrrenamed

The content is the same.

test/reg063/Cmp.idr → test/regression001/reg063.idrrenamed

The content is the same.

test/reg064/reg064.idr → test/regression001/reg064.idrrenamed

The content is the same.

test/reg065/reg065.idr → test/regression001/reg065.idrrenamed

The content is the same.

test/reg066/reg066.idr → test/regression001/reg066.idrrenamed

The content is the same.

test/reg071/reg071.idr → test/regression001/reg071.idrrenamed

The content is the same.

test/reg073/reg073.lidr → test/regression001/reg073.lidrrenamed

The content is the same.

test/reg074/reg074.idr → test/regression001/reg074.idrrenamed

The content is the same.

test/regression001/runnew file+13
@@ -0,0 +1,13 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ --check \
3+ reg001.idr reg036.idr reg037.idr reg038.idr reg046.idr \
4+ reg047a.idr reg053.idr reg057.idr reg058.idr reg058a.idr \
5+ reg059.idr reg060.idr reg061.idr reg062.idr reg063.idr \
6+ reg064.idr reg065.idr reg066.idr reg071.idr reg074.idr
7+
8+${IDRIS:-idris} $@ --check --nobuiltins reg047.idr
9+
10+${IDRIS:-idris} $@ --check --nocolour \
11+ reg062.lidr reg073.lidr
12+
13+rm -f *.ibc