a02bfec · Idris-dev · git.iko.soy

.travis.yml+2

compare with master

unifiedsplit

@@ -66,6 +66,8 @@ before_install:

66 fi

67

68install:

69+ - which cabal

70+ - which ghc

69 - cabal --version

71 - cabal --version

70 - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]"

72 - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]"

71 - if [ -f $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz ];

73 - if [ -f $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz ];

CHANGELOG.md+4

@@ -10,7 +10,11 @@

10 + `FirstClassReflection`, which must be enabled to define a `%reflection`

11 function

12

13+## Library Updates

13

14

15++ Terminating programs has been improved with more appropriate

16+ functions (`exitWith`, `exitFailure`, and `exitSuccess`) and a data

17+ structure (`ExitCode`) to capture a program's return code.

14

18

15# New in 0.99:

19# New in 0.99:

16

20

docs/reference/packages.rst+5

@@ -111,6 +111,11 @@ The following option is available:

111

112.. IMPORTANT::

113 The modules containing the test functions must also be added to the list of modules.

114+

115+Comments

116+---------

117+

118+Package files support comments using the standard Idris singleline ``--`` and multiline ``{- -}`` format.

114

119

115Using Package files

120Using Package files

116===================

121===================

docs/tutorial/testing.rst+4

@@ -27,6 +27,8 @@ For example, lets take the following list of functions that are defined in a mod

27.. code-block:: idris

28

29 module Maths.NumOps

30+

31+ %access export -- to make functions under test visible

30

32

31 double : Num a => a -> a

33 double : Num a => a -> a

32 double a = a + a

34 double a = a + a

@@ -42,6 +44,8 @@ A simple test module, with a qualified name of ``Test.NumOps`` can be declared a

42 module Test.NumOps

44 module Test.NumOps

43

45

44 import Maths.NumOps

46 import Maths.NumOps

47+

48+ %access export -- to make the test functions visible

45

49

46 assertEq : Eq a => (given : a) -> (expected : a) -> IO ()

50 assertEq : Eq a => (given : a) -> (expected : a) -> IO ()

47 assertEq g e = if g == e

51 assertEq g e = if g == e

idris.cabal+8−1

@@ -289,7 +289,6 @@ Library

289 , vector < 0.12

290 , vector-binary-instances < 0.3

291 , zip-archive > 0.2.3.5 && < 0.4

292− , safe == 0.3.9

293 , fsnotify >= 0.2 && < 2.2

292 , fsnotify >= 0.2 && < 2.2

294 , async < 2.2

293 , async < 2.2

295

294

@@ -302,6 +301,14 @@ Library

302 else

301 else

303 build-depends: process < 1.5

302 build-depends: process < 1.5

304

303

304+ -- safe 0.3.10 is having issues with cabal 1.20 and ghc 7.6.3, the

305+ -- hvr ghc ppa doesn't provide a new enough cabal library. Temporary

306+ -- fix until hvr ghc ppa is fixed or we deprecate support for 7.6.3.

307+ if impl(ghc < 7.8.4)

308+ build-depends: safe == 0.3.9

309+ else

310+ build-depends: safe >= 0.3.9

311+

305 Extensions: MultiParamTypeClasses

312 Extensions: MultiParamTypeClasses

306 , DeriveFoldable

313 , DeriveFoldable

307 , DeriveTraversable

314 , DeriveTraversable

libs/base/Debug/Error.idr+1−2

@@ -12,9 +12,8 @@ error : {default (%runElab sourceLocation) loc : SourceLocation} ->

12 (message : String) ->

13 a

14error {loc = FileLoc filename (line, col) _} message =

15− believe_me . unsafePerformIO $

15+ unsafePerformIO $

16 do let place = filename ++ " line " ++ show line ++ " column " ++ show col

17 let message' = place ++ ": " ++ message

18 putStrLn message'

19 exit 1

20−

libs/base/System.idr+35−4

@@ -1,5 +1,7 @@

1module System

2

3+import Data.So

4+

3%include C "unistd.h"

5%include C "unistd.h"

4%default partial

6%default partial

5%access public export

7%access public export

@@ -52,11 +54,41 @@ getEnvironment = getAllPairs 0 []

52 then pure $ reverse $ map splitEq acc

54 then pure $ reverse $ map splitEq acc

53 else getAllPairs (n + 1) (envPair :: acc)

55 else getAllPairs (n + 1) (envPair :: acc)

54

56

57+||| Programs can either terminate successfully, or end in a caught

58+||| failure.

59+data ExitCode : Type where

60+ ||| Terminate successfully.

61+ ExitSuccess : ExitCode

62+ ||| Program terminated for some prescribed reason.

63+ |||

64+ ||| @errNo A non-zero numerical value indicating failure.

65+ ||| @prf Proof that the int value is non-zero.

66+ ExitFailure : (errNo : Int)

67+ -> {auto prf : So (not $ errNo == 0)}

68+ -> ExitCode

69+

55||| Quit with a particular exit code

70||| Quit with a particular exit code

56−exit : Int -> IO ()

71+exit : Int -> IO a

57−exit code = foreign FFI_C "exit" (Int -> IO ()) code

72+exit code = believe_me $ foreign FFI_C "exit" (Int -> IO ()) code

73+

74+||| Terminate the program with an `ExitCode`. This code indicates the

75+||| success of the program's execution, and returns the success code

76+||| to the program's caller.

77+|||

78+||| @code The `ExitCode` for program.

79+exitWith : (code : ExitCode) -> IO a

80+exitWith ExitSuccess = exit 0

81+exitWith (ExitFailure errNo) = exit errNo

58

82

83+||| Exit the program indicating failure.

84+exitFailure : IO a

85+exitFailure = exitWith (ExitFailure 1)

86+

87+||| Exit the program after a successful run.

88+exitSuccess : IO a

89+exitSuccess = exitWith ExitSuccess

90+

59−||| Get the numbers of seconds since 1st January 1970, 00:00 UTC

91+||| Get the numbers of seconds since 1st January 1970, 00:00 UTC

60time : IO Integer

92time : IO Integer

61time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))

93time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))

62 pure t

94 pure t

@@ -66,4 +98,3 @@ usleep i = foreign FFI_C "usleep" (Int -> IO ()) i

66

98

67system : String -> IO Int

99system : String -> IO Int

68system cmd = foreign FFI_C "system" (String -> IO Int) cmd

100system cmd = foreign FFI_C "system" (String -> IO Int) cmd

69−

libs/effects/Effect/Exception.idr+1−2

@@ -17,7 +17,7 @@ implementation Handler (Exception a) List where

17

18implementation Show a => Handler (Exception a) IO where

19 handle _ (Raise e) k = do printLn e

20− believe_me (exit 1)

20+ (exit 1)

21

22implementation Handler (Exception a) (IOExcept a) where

23 handle _ (Raise e) k = ioe_fail e

@@ -30,4 +30,3 @@ EXCEPTION t = MkEff () (Exception t)

30

31raise : a -> Eff b [EXCEPTION a]

32raise err = call $ Raise err

33−

src/IRTS/System.hs+6−1

@@ -6,7 +6,7 @@ License : BSD3

6Maintainer : The Idris Community.

7-}

8{-# LANGUAGE CPP #-}

9−module IRTS.System( getDataFileName

9+module IRTS.System( getIdrisDataFileByName

10 , getCC

11 , getLibFlags

12 , getIdrisDataDir

@@ -42,6 +42,11 @@ getIdrisDataDir = do

42 return ddir

43 Just ddir -> return ddir

44

45+getIdrisDataFileByName :: String -> IO FilePath

46+getIdrisDataFileByName fn = do

47+ dir <- getIdrisDataDir

48+ return $ dir </> fn

49+

45overrideIdrisSubDirWith :: String -- ^ Sub directory in `getDataDir` location.

50overrideIdrisSubDirWith :: String -- ^ Sub directory in `getDataDir` location.

46 -> String -- ^ Environment variable to get new location from.

51 -> String -- ^ Environment variable to get new location from.

47 -> IO FilePath

52 -> IO FilePath

src/Idris/IdrisDoc.hs+2−2

@@ -19,7 +19,7 @@ import Idris.Docs

19import Idris.Docstrings (nullDocstring)

20import qualified Idris.Docstrings as Docstrings

21import Idris.Parser.Helpers (opChars)

22−import IRTS.System (getDataFileName)

22+import IRTS.System (getIdrisDataFileByName)

23

24import Control.Applicative ((<|>))

25import Control.Monad (forM_)

@@ -708,5 +708,5 @@ copyDependencies :: FilePath -- ^ The base directory to which

708 -- dependencies should be written

709 -> IO ()

710copyDependencies dir =

711− do styles <- getDataFileName $ "idrisdoc" </> "styles.css"

711+ do styles <- getIdrisDataFileByName $ "idrisdoc" </> "styles.css"

712 copyFile styles (dir </> "styles.css")

src/Idris/Info.hs+5

@@ -22,6 +22,7 @@ module Idris.Info

22 , getIdrisHistoryFile

23 , getIdrisInstalledPackages

24 , getIdrisLoggingCategories

25+ , getIdrisDataFileByName

25 ) where

26 ) where

26

27

27import Idris.AbsSyntax (loggingCatsStr)

28import Idris.AbsSyntax (loggingCatsStr)

@@ -34,6 +35,7 @@ import Version_idris (gitHash)

34import Data.Version

35import Data.Version

35import System.Directory

36import System.Directory

36import System.FilePath

37import System.FilePath

38+

37getIdrisDataDir :: IO String

39getIdrisDataDir :: IO String

38getIdrisDataDir = S.getIdrisDataDir

40getIdrisDataDir = S.getIdrisDataDir

39

41

@@ -88,3 +90,6 @@ getIdrisInstalledPackages = installedPackages

88

90

89getIdrisLoggingCategories :: IO [String]

91getIdrisLoggingCategories :: IO [String]

90getIdrisLoggingCategories = return $ words loggingCatsStr

92getIdrisLoggingCategories = return $ words loggingCatsStr

93+

94+getIdrisDataFileByName :: String -> IO FilePath

95+getIdrisDataFileByName = S.getIdrisDataFileByName

src/Idris/Package.hs+3−2

@@ -145,7 +145,7 @@ replPkg copts fp = do

145 case mergeOptions copts (idris_opts pkgdesc) of

146 Left emsg -> ifail emsg

147 Right opts -> do

148−

148+

149 putIState orig

150 dir <- runIO getCurrentDirectory

151 runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc

@@ -266,7 +266,8 @@ testPkg copts fp = do

266 exitWith (ExitFailure 1)

267 Right opts -> do

268 m_ist <- idris opts

269+ let texe = if isWindows then addExtension tmpn' ".exe" else tmpn'

269− exitCode <- rawSystem tmpn' []

270+ exitCode <- rawSystem texe []

270 return (m_ist, exitCode)

271 return (m_ist, exitCode)

271 case m_ist of

272 case m_ist of

272 Nothing -> exitWith (ExitFailure 1)

273 Nothing -> exitWith (ExitFailure 1)

test/TestData.hs+2−1

@@ -178,7 +178,8 @@ testFamiliesData = [

178 ( 4, ANY ),

179 ( 5, ANY ),

180 ( 6, ANY ),

181− ( 7, ANY )]),

181+ ( 7, ANY ),

182+ ( 8, ANY )]),

182 ("prelude", "Prelude",

183 ("prelude", "Prelude",

183 [ ( 1, ANY )]),

184 [ ( 1, ANY )]),

184 ("primitives", "Primitive types",

185 ("primitives", "Primitive types",

test/pkg008/expectednew file+13

@@ -0,0 +1,13 @@

1+Entering directory `./src'

2+Type checking ./NumOps.idr

3+Type checking ./Test.idr

4+Leaving directory `./src'

5+Test Passed

6+Test Passed

7+Entering directory `./src'

8+Leaving directory `./src'

9+Entering directory `./src'

10+Removed: NumOps.ibc

11+Removed: Test.ibc

12+Removed: 00maths-idx.ibc

13+Leaving directory `./src'

test/pkg008/maths.ipkgnew file+9

@@ -0,0 +1,9 @@

1+package maths

2+

3+sourcedir = src

4+

5+modules = NumOps

6+ , Test

7+

8+tests = Test.testDouble

9+ , Test.testTriple

test/pkg008/runnew file+9

@@ -0,0 +1,9 @@

1+#!/usr/bin/env bash

2+

3+${IDRIS:-idris} $@ --build maths.ipkg

4+${IDRIS:-idris} $@ --testpkg maths.ipkg | grep -v -e "idris"

5+

6+# Idris only appears in the randomly generated name of test so we grep

7+# to remove it to make output consistent.

8+

9+${IDRIS:-idris} $@ --clean maths.ipkg

test/pkg008/src/NumOps.idrnew file+9

@@ -0,0 +1,9 @@

1+module NumOps

2+

3+%access export -- to make functions under test visible

4+

5+double : Num a => a -> a

6+double a = a + a

7+

8+triple : Num a => a -> a

9+triple a = a + double a

test/pkg008/src/Test.idrnew file+21

@@ -0,0 +1,21 @@

1+module Test

2+

3+import NumOps

4+

5+%access export -- to make the test functions visible

6+

7+assertEq : Eq a => (given : a) -> (expected : a) -> IO ()

8+assertEq g e = if g == e

9+ then putStrLn "Test Passed"

10+ else putStrLn "Test Failed"

11+

12+assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()

13+assertNotEq g e = if not (g == e)

14+ then putStrLn "Test Passed"

15+ else putStrLn "Test Failed"

16+

17+testDouble : IO ()

18+testDouble = assertEq (double 2) 4

19+

20+testTriple : IO ()

21+testTriple = assertNotEq (triple 2) 5