git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3706 from jfdm/only-specify-installed-ipkgs

Refuse to work if listed packages are not installed.

commit041b80b306b338d8ade29bc466c99c8ef6a62f38 authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateFri 24 Mar 2017, 10:40 (10 years ago) parent674c214088360f
5 files changed+29
compare with master
unifiedsplit
CHANGELOG.md+7 src/Idris/Main.hs+13 src/Idris/Output.hs+5 test/pkg008/expected+2 test/pkg008/run+2
CHANGELOG.md+7
@@ -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+
18# New in 0.99.1:
29
310## Language updates
src/Idris/Main.hs+13
@@ -37,6 +37,7 @@ import Control.Monad
3737import Control.Monad.Trans (lift)
3838import Control.Monad.Trans.Except (runExceptT)
3939import Control.Monad.Trans.State.Strict (execStateT)
40+import Data.List
4041import Data.Maybe
4142import Prelude hiding (id, (.), (<$>))
4243import System.Console.Haskeline as H
@@ -138,9 +139,21 @@ idrisMain opts =
138139
139140 setNoBanner nobanner
140141
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+
141153 when (not (NoBasePkgs `elem` opts)) $ do
142154 addPkgDir "prelude"
143155 addPkgDir "base"
156+
144157 mapM_ addPkgDir pkgdirs
145158 elabPrims
146159 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
174174 RawOutput h -> runIO $ hPutStrLn h s
175175 IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" s n
176176
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
177182
178183idemodePutSExp :: SExpable a => String -> a -> Idris ()
179184idemodePutSExp cmd info = do i <- getIState
test/pkg008/expected+2
@@ -11,3 +11,5 @@ Removed: NumOps.ibc
1111Removed: Test.ibc
1212Removed: 00maths-idx.ibc
1313Leaving 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"
77# to remove it to make output consistent.
88
99${IDRIS:-idris} $@ --clean maths.ipkg
10+
11+${IDRIS:-idris} $@ -p maths