041b80b · Idris-dev · git.iko.soy

CHANGELOG.md+7

compare with master

unifiedsplit

@@ -1,3 +1,10 @@

1+# New in 0.99.2

2+

3+## Tool Updates

4+

5++ Idris now checks the list of packages specified at the command line

6+ against those installed. If there is a mismatch Idris will complain.

7+

1# New in 0.99.1:

8# New in 0.99.1:

2

9

3## Language updates

10## Language updates

src/Idris/Main.hs+13

@@ -37,6 +37,7 @@ import Control.Monad

37import Control.Monad.Trans (lift)

38import Control.Monad.Trans.Except (runExceptT)

39import Control.Monad.Trans.State.Strict (execStateT)

40+import Data.List

40import Data.Maybe

41import Data.Maybe

41import Prelude hiding (id, (.), (<$>))

42import Prelude hiding (id, (.), (<$>))

42import System.Console.Haskeline as H

43import System.Console.Haskeline as H

@@ -138,9 +139,21 @@ idrisMain opts =

138

139

139 setNoBanner nobanner

140 setNoBanner nobanner

140

141

142+ -- Check if listed packages are actually installed

143+

144+ idrisCatch (do ipkgs <- runIO $ getIdrisInstalledPackages

145+ let diff_pkgs = (\\) pkgdirs ipkgs

146+

147+ when (not $ null diff_pkgs) $ do

148+ iputStrLn "The following packages were specified but cannot be found:"

149+ iputStr $ unlines $ map (\x -> unwords ["-", x]) diff_pkgs

150+ runIO $ exitWith (ExitFailure 1))

151+ (\e -> return ())

152+

141 when (not (NoBasePkgs `elem` opts)) $ do

153 when (not (NoBasePkgs `elem` opts)) $ do

142 addPkgDir "prelude"

154 addPkgDir "prelude"

143 addPkgDir "base"

155 addPkgDir "base"

156+

144 mapM_ addPkgDir pkgdirs

157 mapM_ addPkgDir pkgdirs

145 elabPrims

158 elabPrims

146 when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins" (IBC_REPL True)

159 when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins" (IBC_REPL True)

src/Idris/Output.hs+5

@@ -174,6 +174,11 @@ iputStrLn s = do i <- getIState

174 RawOutput h -> runIO $ hPutStrLn h s

175 IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" s n

176

177+iputStr :: String -> Idris ()

178+iputStr s = do i <- getIState

179+ case idris_outputmode i of

180+ RawOutput h -> runIO $ hPutStr h s

181+ IdeMode n h -> runIO . hPutStr h $ convSExp "write-string" s n

177

182

178idemodePutSExp :: SExpable a => String -> a -> Idris ()

183idemodePutSExp :: SExpable a => String -> a -> Idris ()

179idemodePutSExp cmd info = do i <- getIState

184idemodePutSExp cmd info = do i <- getIState

test/pkg008/expected+2

@@ -11,3 +11,5 @@ Removed: NumOps.ibc

11Removed: Test.ibc

12Removed: 00maths-idx.ibc

13Leaving directory `./src'

14+The following packages were specified but cannot be found:

15+- maths

test/pkg008/run+2

@@ -7,3 +7,5 @@ ${IDRIS:-idris} $@ --testpkg maths.ipkg | grep -v -e "idris"

7# to remove it to make output consistent.

8

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

10+

11+${IDRIS:-idris} $@ -p maths