6f08060 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added IdrisDoc tests

commit6f0806061ea369950e4d9cd5872eac372ffd8c9d authorPhilip Rasmussen <pjor@itu.dk> dateTue 22 Apr 2014, 23:44 (13 years ago) parentaed1014

46 files changed+276

compare with master

unifiedsplit

idris.cabal+43

@@ -319,6 +319,49 @@ Extra-source-files:

319319 test/ffi005/run

320320 test/ffi005/expected

321321

322+ test/idrisdoc001/*.idr

323+ test/idrisdoc001/*.ipkg

324+ test/idrisdoc001/idrisdoc001.hs

325+ test/idrisdoc001/run

326+ test/idrisdoc001/run_backup

327+ test/idrisdoc001/expected

328+ test/idrisdoc002/*.idr

329+ test/idrisdoc002/*.ipkg

330+ test/idrisdoc002/idrisdoc002.hs

331+ test/idrisdoc002/run

332+ test/idrisdoc002/run_backup

333+ test/idrisdoc002/expected

334+ test/idrisdoc003/*.idr

335+ test/idrisdoc003/*.ipkg

336+ test/idrisdoc003/idrisdoc003.hs

337+ test/idrisdoc003/run

338+ test/idrisdoc003/run_backup

339+ test/idrisdoc003/expected

340+ test/idrisdoc004/*.idr

341+ test/idrisdoc004/*.ipkg

342+ test/idrisdoc004/idrisdoc004.hs

343+ test/idrisdoc004/run

344+ test/idrisdoc004/run_backup

345+ test/idrisdoc004/expected

346+ test/idrisdoc005/*.idr

347+ test/idrisdoc005/*.ipkg

348+ test/idrisdoc005/idrisdoc005.hs

349+ test/idrisdoc005/run

350+ test/idrisdoc005/run_backup

351+ test/idrisdoc005/expected

352+ test/idrisdoc006/*.idr

353+ test/idrisdoc006/*.ipkg

354+ test/idrisdoc006/idrisdoc006.hs

355+ test/idrisdoc006/run

356+ test/idrisdoc006/run_backup

357+ test/idrisdoc006/expected

358+ test/idrisdoc007/*.idr

359+ test/idrisdoc007/*.ipkg

360+ test/idrisdoc007/idrisdoc007.hs

361+ test/idrisdoc007/run

362+ test/idrisdoc007/run_backup

363+ test/idrisdoc007/expected

364+

322365 test/interactive001/run

323366 test/interactive001/input

324367 test/interactive001/*.idr

test/README+1

@@ -5,6 +5,7 @@ dsl: Embedded DSLs and features to support DSL development

55effects: Effects package

66error: Error messages and error reflection

77ffi: FFI calls, including type providers

8+idrisdoc: Documentation tool functionality

89interactive: Interactive editing, proof search

910io: IO monad

1011literate: .lidr files; literate programming

test/idrisdoc001/TestEmpty.idrnew file+1

@@ -0,0 +1 @@

1+module TestEmpty

test/idrisdoc001/expectednew file+3

@@ -0,0 +1,3 @@

1+Type checking ./TestEmpty.idr

2+Warning: Ignoring empty or non-existing namespace 'TestEmpty'

3+No namespaces to generate documentation for

test/idrisdoc001/idrisdoc001.hsnew file+6

@@ -0,0 +1,6 @@

1+-- Tests that documentation for empty namespaces are not created

3+import Pkg.Package

5+main :: IO ()

6+main = documentPkg "test_empty.ipkg"

test/idrisdoc001/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+ghc -v0 idrisdoc001.hs

3+./idrisdoc001

4+rm -rf idrisdoc001 idrisdoc001.hi idrisdoc001.o *.ibc *_doc

test/idrisdoc001/run_backupnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+ghc -v0 idrisdoc001.hs

3+./idrisdoc001

4+rm -rf idrisdoc001 idrisdoc001.hi idrisdoc001.o *.ibc *_doc

test/idrisdoc001/test_empty.ipkgnew file+4

@@ -0,0 +1,4 @@

1+package test_empty

3+modules = TestEmpty

test/idrisdoc002/TestFunctions.idrnew file+5

@@ -0,0 +1,5 @@

1+module TestFunctions

3+||| Test function

4+test : ()

5+test = ()

test/idrisdoc002/expectednew file+2

@@ -0,0 +1,2 @@

1+Type checking ./TestFunctions.idr

2+True

test/idrisdoc002/idrisdoc002.hsnew file+10

@@ -0,0 +1,10 @@

1+-- Tests that documentation is generated for functions

3+import System.Directory

4+import Pkg.Package

6+main :: IO ()

7+main = do

8+ documentPkg "test_functions.ipkg"

9+ (doesDirectoryExist "test_functions_doc") >>= print

10+

test/idrisdoc002/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+ghc -v0 idrisdoc002.hs

3+./idrisdoc002

4+rm -rf idrisdoc002 idrisdoc002.hi idrisdoc002.o *.ibc *_doc

test/idrisdoc002/run_backupnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+ghc -v0 idrisdoc002.hs

3+./idrisdoc002

4+rm -rf idrisdoc002 idrisdoc002.hi idrisdoc002.o *.ibc *_doc

test/idrisdoc002/test_functions.ipkgnew file+4

@@ -0,0 +1,4 @@

1+package test_functions

3+modules = TestFunctions

test/idrisdoc003/TestDatatypes.idrnew file+6

@@ -0,0 +1,6 @@

1+module TestDatatypes

3+||| This is another test

4+data Test : Type where

5+ ||| Test constructor

6+ ATest : Test

test/idrisdoc003/expectednew file+2

@@ -0,0 +1,2 @@

1+Type checking ./TestDatatypes.idr

2+True

test/idrisdoc003/idrisdoc003.hsnew file+10

@@ -0,0 +1,10 @@

1+-- Tests that documentation is generated for data types

3+import System.Directory

4+import Pkg.Package

6+main :: IO ()

7+main = do

8+ documentPkg "test_datatypes.ipkg"

9+ (doesDirectoryExist "test_datatypes_doc") >>= print

10+

test/idrisdoc003/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+ghc -v0 idrisdoc003.hs

3+./idrisdoc003

4+rm -rf idrisdoc003 idrisdoc003.hi idrisdoc003.o *.ibc *_doc

test/idrisdoc003/run_backupnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+ghc -v0 idrisdoc003.hs

3+./idrisdoc003

4+rm -rf idrisdoc003 idrisdoc003.hi idrisdoc003.o *.ibc *_doc

test/idrisdoc003/test_datatypes.ipkgnew file+4

@@ -0,0 +1,4 @@

1+package test_datatypes

3+modules = TestDatatypes

test/idrisdoc004/TestTypeclasses.idrnew file+8

@@ -0,0 +1,8 @@

1+module TestTypeclasses

3+||| This is a test

4+|||

5+||| @ a Test arg

6+class Test a where

7+ ||| Test function

8+ test : a -> Int

test/idrisdoc004/expectednew file+2

@@ -0,0 +1,2 @@

1+Type checking ./TestTypeclasses.idr

2+True

test/idrisdoc004/idrisdoc004.hsnew file+10

@@ -0,0 +1,10 @@

1+-- Tests that documentation is generated for type classes

3+import System.Directory

4+import Pkg.Package

6+main :: IO ()

7+main = do

8+ documentPkg "test_typeclasses.ipkg"

9+ (doesDirectoryExist "test_typeclasses_doc") >>= print

10+

test/idrisdoc004/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+ghc -v0 idrisdoc004.hs

3+./idrisdoc004

4+rm -rf idrisdoc004 idrisdoc004.hi idrisdoc004.o *.ibc *_doc

test/idrisdoc004/run_backupnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+ghc -v0 idrisdoc004.hs

3+./idrisdoc004

4+rm -rf idrisdoc004 idrisdoc004.hi idrisdoc004.o *.ibc *_doc

test/idrisdoc004/test_typeclasses.ipkgnew file+4

@@ -0,0 +1,4 @@

1+package test_typeclasses

3+modules = TestTypeclasses

test/idrisdoc005/TestTracing.idrnew file+4

@@ -0,0 +1,4 @@

1+module TestTracing

3+test : Bool

4+test = True

test/idrisdoc005/expectednew file+2

@@ -0,0 +1,2 @@

1+True

2+True

test/idrisdoc005/idrisdoc005.hsnew file+12

@@ -0,0 +1,12 @@

1+-- Tests that references to other namespaces are traced

3+import System.Directory

4+import System.FilePath

5+import Pkg.Package

7+main :: IO ()

8+main = do

9+ documentPkg "test_tracing.ipkg"

10+ let docs = "test_tracing_doc" </> "docs"

11+ (doesFileExist $ docs </> "TestTracing.html") >>= print

12+ (doesFileExist $ docs </> "Prelude.Bool.html") >>= print

test/idrisdoc005/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+ghc -v0 idrisdoc005.hs

3+./idrisdoc005

4+rm -rf idrisdoc005 idrisdoc005.hi idrisdoc005.o *.ibc *_doc

test/idrisdoc005/run_backupnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+ghc -v0 idrisdoc005.hs

3+./idrisdoc005

4+rm -rf idrisdoc005 idrisdoc005.hi idrisdoc005.o *.ibc *_doc

test/idrisdoc005/test_tracing.ipkgnew file+4

@@ -0,0 +1,4 @@

1+package test_tracing

3+modules = TestTracing

test/idrisdoc006/A.idrnew file+6

@@ -0,0 +1,6 @@

1+module A

3+||| This is another test

4+data Test : Type where

5+ ||| Test constructor

6+ ATest : Test

test/idrisdoc006/B.idrnew file+5

@@ -0,0 +1,5 @@

1+module B

3+||| Test function

4+test : ()

5+test = ()

test/idrisdoc006/expectednew file+6

@@ -0,0 +1,6 @@

1+Type checking ./A.idr

2+Type checking ./B.idr

3+True

4+True

5+A

6+B

test/idrisdoc006/idrisdoc006.hsnew file+14

@@ -0,0 +1,14 @@

1+-- Tests that documentation properly is merged with existing

3+import System.Directory

4+import System.FilePath

5+import Pkg.Package

7+main :: IO ()

8+main = do

9+ documentPkg "package_a.ipkg"

10+ documentPkg "package_b.ipkg"

11+ (doesFileExist $ "test_merge_doc" </> "docs" </> "A.html") >>= print

12+ (doesFileExist $ "test_merge_doc" </> "docs" </> "B.html") >>= print

13+ (readFile $ "test_merge_doc" </> "IdrisDoc") >>= putStr

14+

test/idrisdoc006/package_a.ipkgnew file+4

@@ -0,0 +1,4 @@

1+package test_merge

3+modules = A

test/idrisdoc006/package_b.ipkgnew file+4

@@ -0,0 +1,4 @@

1+package test_merge

3+modules = B

test/idrisdoc006/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+ghc -v0 idrisdoc006.hs

3+./idrisdoc006

4+rm -rf idrisdoc006 idrisdoc006.hi idrisdoc006.o *.ibc *_doc

test/idrisdoc006/run_backupnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+ghc -v0 idrisdoc006.hs

3+./idrisdoc006

4+rm -rf idrisdoc006 idrisdoc006.hi idrisdoc006.o *.ibc *_doc

test/idrisdoc007/A.idrnew file+6

@@ -0,0 +1,6 @@

1+module A

3+||| This is a test

4+data Test : Type where

5+ ||| Test constructor

6+ ATest : Test

test/idrisdoc007/expectednew file+6

@@ -0,0 +1,6 @@

1+Expect 1 for error: 1

2+Expects 2 lines of output:

3+ 2 lines

4+Expects the first line to be type checking:

5+Type checking ./A.idr

6+Cannot check the second line as it contains a host-dependent string.

test/idrisdoc007/idrisdoc007.hsnew file+6

@@ -0,0 +1,6 @@

1+-- Tests that documentation only is written when safe

3+import Pkg.Package

5+main :: IO ()

6+main = documentPkg "package.ipkg"

test/idrisdoc007/package.ipkgnew file+4

@@ -0,0 +1,4 @@

1+package do_not_delete

3+modules = A

test/idrisdoc007/runnew file+10

@@ -0,0 +1,10 @@

1+#!/usr/bin/env bash

2+ghc -v0 idrisdoc007.hs

3+./idrisdoc007 > lines

4+echo Expect 1 for error: $?

5+echo Expects 2 lines of output:

6+wc -l lines

7+echo Expects the first line to be type checking:

8+grep "Type checking \\./A\\.idr" lines

9+echo Cannot check the second line as it contains a host-dependent string.

10+rm -rf idrisdoc007 idrisdoc007.hi idrisdoc007.o *.ibc lines

test/idrisdoc007/run_backupnew file+10

@@ -0,0 +1,10 @@

1+#!/usr/bin/env bash

2+ghc -v0 idrisdoc007.hs

3+./idrisdoc007 > lines

4+echo Expect 1 for error: $?

5+echo Expects 2 lines of output:

6+wc -l lines

7+echo Expects the first line to be type checking:

8+grep "Type checking \\./A\\.idr" lines

9+echo Cannot check the second line as it contains a host-dependent string.

10+rm -rf idrisdoc007 idrisdoc007.hi idrisdoc007.o *.ibc lines