Make --quiet imply non-verbosity
This causes Idris to not emit messages about "Type checking ...." while
in quiet mode, which improves the portability of tests to Windows (due
to the slash facing the other way there). It also makes tests a bit more
robust with regards to their source files changing names.
commit6c4553c31f0ead6f881b00ba65c042d677f4973e
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateWed 1 Apr 2015, 17:48 (12 years ago)
parentce3b60b
src/Idris/AbsSyntax.hs+3−1
@@ -816,7 +816,9 @@ targetCPU = do i <- getIState
816816
817817verbose :: Idris Bool
818818verbose = do i <- getIState
819− return (opt_verbose (idris_options i))
819+ -- Quietness overrides verbosity
820+ return (not (opt_quiet (idris_options i)) &&
821+ opt_verbose (idris_options i))
820822
821823setVerbose :: Bool -> Idris ()
822824setVerbose t = do i <- getIState
test/delab001/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./delab001.idr
21foo : Nat -> String
32foo n = case n of
43 0 => "z"
test/docs001/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./docs001.idr
21Type class C
32 class
43
test/docs002/expected+3−5
@@ -1,11 +1,9 @@
1−Type checking ./docs002.idr
2−*docs002> T1 : Type
1+T1 : Type
32 Some documentation
43
5−*docs002> T2 : Type
4+T2 : Type
65 Some other documentation
76
8−*docs002> T3 : Int
7+T3 : Int
98 Some provided postulate
109
11−*docs002> Bye bye
test/docs002/run+1−1
@@ -1,3 +1,3 @@
11#!/usr/bin/env bash
2−idris --consolewidth 80 --nobanner --nocolor docs002.idr < input
2+idris --consolewidth 80 --nobanner --nocolor --quiet docs002.idr < input
33rm *.ibc
test/docs003/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./docs003.idr
21Type class Functor
32 Functors
43
test/ffi001/expected−1
@@ -1,2 +1 @@
1−Type checking ./test022.idr
210.9995736030415051
test/ffi003/expected−1
@@ -1,2 +1 @@
1−Type checking ./test024.idr
21testtest
test/idrisdoc001/expected−2
@@ -1,5 +1,3 @@
1−Type checking ./TestEmpty.idr
2−Type checking ./TestPrivate.idr
31Warning: Ignoring empty or non-existing namespace 'TestEmpty'
42Warning: Ignoring empty or non-existing namespace 'TestPrivate'
53No namespaces to generate documentation for
test/idrisdoc001/run+1−1
@@ -1,4 +1,4 @@
11#!/usr/bin/env bash
22# Tests that no documentation is built for empty and/or private-only namespaces
33idris --mkdoc test_empty.ipkg
4−rm -rf *.ibc *_doc
4+rm -rf *.ibc *_doc
test/idrisdoc001/test_empty.ipkg+2
@@ -1,4 +1,6 @@
11package test_empty
22
3+opts = "--quiet"
4+
35modules = TestEmpty, TestPrivate
46
test/idrisdoc002/expected−1
@@ -1,2 +1 @@
1−Type checking ./TestFunctions.idr
21Functions are documented
test/idrisdoc002/test_functions.ipkg+2
@@ -1,4 +1,6 @@
11package test_functions
22
3+opts = "--quiet"
4+
35modules = TestFunctions
46
test/idrisdoc003/expected−1
@@ -1,2 +1 @@
1−Type checking ./TestDatatypes.idr
21Data types are documented
test/idrisdoc003/test_datatypes.ipkg+2
@@ -1,4 +1,6 @@
11package test_datatypes
22
3+opts = "--quiet"
4+
35modules = TestDatatypes
46
test/idrisdoc004/expected−1
@@ -1,2 +1 @@
1−Type checking ./TestTypeclasses.idr
21Typeclasses are documented
test/idrisdoc004/test_typeclasses.ipkg+2
@@ -1,4 +1,6 @@
11package test_typeclasses
22
3+opts = "--quiet"
4+
35modules = TestTypeclasses
46
test/idrisdoc005/expected−1
@@ -1,3 +1,2 @@
1−Type checking ./TestTracing.idr
21TestTracing: Check
32Prelude.Bool: Check
test/idrisdoc005/test_tracing.ipkg+2
@@ -1,4 +1,6 @@
11package test_tracing
22
3+opts = "--quiet"
4+
35modules = TestTracing
46
test/idrisdoc006/expected−2
@@ -1,6 +1,4 @@
1−Type checking ./A/fully/Qualified/NAME.idr
21IdrisDoc file written
3−Type checking ./B.idr
42A.fully.Qualified.NAME.html
53B.html
64A.fully.Qualified.NAME is in the index
test/idrisdoc006/package_a.ipkg+2
@@ -1,4 +1,6 @@
11package test_merge
22
3+opts = "--quiet"
4+
35modules = A.fully.Qualified.NAME
46
test/idrisdoc006/package_b.ipkg+2
@@ -1,4 +1,6 @@
11package test_merge
22
3+opts = "--quiet"
4+
35modules = B
46
test/idrisdoc007/package.ipkg+2
@@ -1,4 +1,6 @@
11package do_not_delete
22
3+opts = "--quiet"
4+
35modules = A
46
test/idrisdoc008/expected−2
@@ -1,4 +1,2 @@
1−Type checking ./Abstract.idr
2−Type checking ./Visible.idr
31Abstract members are documented
42Public members are documented
test/idrisdoc008/visibility.ipkg+2
@@ -1,4 +1,6 @@
11package visibility
22
3+opts = "--quiet"
4+
35modules = Abstract, Visible
46
test/idrisdoc009/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./Test.idr
21Data type Test : Type
32 Docs for datatype Test.
43
test/interactive001/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./test032.idr
21isElem x [] = ?isElem_rhs_1
32isElem x (y :: xs) = ?isElem_rhs_3
43
test/interactive002/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./interactive002.idr
21Nat
32Nat
43Nat
test/interactive003/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./interactive003.idr
21ys
32x :: app xs ys
43[]
test/interactive004/expected−1
@@ -1,3 +1,2 @@
1−Type checking ./interactive004.idr
21plus ?foo_rhs2 ?foo_rhs3
32append k m ?append_rhs2 ?append_rhs3
test/interactive005/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./interactive005.idr
213 : Nat
32Hello, World
43main : IO ()
test/interactive006/expected−1
@@ -1,2 +1 @@
1−Type checking ./interactive006.idr
21plus ?foo_rhs2 ?foo_rhs3
test/proof009/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./proof009.idr
21
32
43---------- Goal: ----------
test/reg039/expected−1
@@ -1,2 +1 @@
1−Type checking ./reg039.idr
21[3, 2, 1]
test/reg041/expected−1
@@ -1,3 +1,2 @@
1−Type checking ./ott.idr
21?prf : (x : Bool) -> (x1 : Bool) -> El (EQ two x two x1) -> El (EQ two x two x1)
32Z
test/totality007/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./Totality.idr
21Totality.idr:4:1:
32Totality.foo is not total as there are missing cases
43Totality.idr:4:1:Could not build: Totality.foo is not total as there are missing cases
test/totality007/totality.ipkg+1−1
@@ -2,6 +2,6 @@ package totality
22
33-- totality007
44-- Test that the package builder doesn't allow totality errors in a build
5−opts = "--consolewidth 80"
5+opts = "--quiet --consolewidth 80"
66sourcedir = src
77modules = Totality