@@ -18,6 +18,8 @@ import Control.Monad.Trans.Except (runExceptT)
1818import Data.List
1919import Data.List.Split(splitOn)
2020
21+import Data.Either
22+
2123import Idris.Core.TT
2224import Idris.REPL
2325import Idris.Parser (loadModule)
@@ -27,6 +29,7 @@ import Idris.IdrisDoc
2729import Idris.IBC
2830import Idris.Output
2931import Idris.Imports
32+import Idris.Error (ifail)
3033
3134import Pkg.PParser
3235
@@ -46,29 +49,37 @@ buildPkg :: [Opt] -- ^ Command line options
4649 -> Bool -- ^ Provide Warnings
4750 -> (Bool, FilePath) -- ^ (Should we install, Location of iPKG file)
4851 -> IO ()
49−buildPkg copts warnonly (install, fp)
50− = do pkgdesc <- parseDesc fp
51− dir <- getCurrentDirectory
52− let idx = PkgIndex (pkgIndex (pkgname pkgdesc))
53− ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
54− when (and ok) $
55− do m_ist <- inPkgDir pkgdesc $
56− do make (makefile pkgdesc)
57− case (execout pkgdesc) of
58− Nothing -> buildMods (idx : NoREPL : Verbose : idris_opts pkgdesc)
59− (modules pkgdesc)
60− Just o -> do let exec = dir </> o
61− buildMods
62− (idx : NoREPL : Verbose : Output exec : idris_opts pkgdesc)
63− [idris_main pkgdesc]
64− case m_ist of
65− Nothing -> exitWith (ExitFailure 1)
66− Just ist -> do
67− -- Quit with error code if there was a problem
68− case errSpan ist of
69− Just _ -> exitWith (ExitFailure 1)
70− _ -> return ()
71− when install $ installPkg pkgdesc
52+buildPkg copts warnonly (install, fp) = do
53+ pkgdesc <- parseDesc fp
54+ dir <- getCurrentDirectory
55+ let idx = PkgIndex (pkgIndex (pkgname pkgdesc))
56+ oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
57+ when (and oks) $ do
58+ m_ist <- inPkgDir pkgdesc $ do
59+
60+ make (makefile pkgdesc)
61+ case (execout pkgdesc) of
62+ Nothing -> do
63+ case mergeOptions copts (idx : NoREPL : Verbose : idris_opts pkgdesc) of
64+ Left emsg -> do
65+ putStrLn emsg
66+ exitWith (ExitFailure 1)
67+ Right opts -> buildMods opts (modules pkgdesc)
68+ Just o -> do
69+ let exec = dir </> o
70+ case mergeOptions copts (idx : NoREPL : Verbose : Output exec : idris_opts pkgdesc) of
71+ Left emsg -> do
72+ putStrLn emsg
73+ exitWith (ExitFailure 1)
74+ Right opts -> buildMods opts [idris_main pkgdesc]
75+ case m_ist of
76+ Nothing -> exitWith (ExitFailure 1)
77+ Just ist -> do
78+ -- Quit with error code if there was a problem
79+ case errSpan ist of
80+ Just _ -> exitWith (ExitFailure 1)
81+ _ -> return ()
82+ when install $ installPkg pkgdesc
7283
7384-- --------------------------------------------------------- [ Check Packages ]
7485
@@ -81,20 +92,25 @@ checkPkg :: [Opt] -- ^ Command line Options
8192 -> Bool -- ^ quit on failure
8293 -> FilePath -- ^ Path to ipkg file.
8394 -> IO ()
84−checkPkg copts warnonly quit fpath
85− = do pkgdesc <- parseDesc fpath
86− ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
87− when (and ok) $
88− do res <- inPkgDir pkgdesc $
89− do make (makefile pkgdesc)
90− buildMods (NoREPL : Verbose : idris_opts pkgdesc)
91− (modules pkgdesc)
92− when quit $ case res of
93− Nothing -> exitWith (ExitFailure 1)
94− Just res' -> do
95− case errSpan res' of
96− Just _ -> exitWith (ExitFailure 1)
97− _ -> return ()
95+checkPkg copts warnonly quit fpath = do
96+ pkgdesc <- parseDesc fpath
97+ oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
98+ when (and oks) $ do
99+ res <- inPkgDir pkgdesc $ do
100+ make (makefile pkgdesc)
101+
102+ case mergeOptions copts (NoREPL : Verbose : idris_opts pkgdesc) of
103+ Left emsg -> do
104+ putStrLn emsg
105+ exitWith (ExitFailure 1)
106+ Right opts -> do
107+ buildMods opts (modules pkgdesc)
108+ when quit $ case res of
109+ Nothing -> exitWith (ExitFailure 1)
110+ Just res' -> do
111+ case errSpan res' of
112+ Just _ -> exitWith (ExitFailure 1)
113+ _ -> return ()
98114
99115-- ------------------------------------------------------------------- [ REPL ]
100116
@@ -109,19 +125,23 @@ replPkg copts fp = do
109125 orig <- getIState
110126 runIO $ checkPkg copts False False fp
111127 pkgdesc <- runIO $ parseDesc fp -- bzzt, repetition!
112− let opts = idris_opts pkgdesc
113− let mod = idris_main pkgdesc
114− let f = toPath (showCG mod)
115− putIState orig
116− dir <- runIO $ getCurrentDirectory
117− runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc
118128
119− if (f /= "")
120− then idrisMain ((Filename f) : opts)
121− else iputStrLn "Can't start REPL: no main module given"
122− runIO $ setCurrentDirectory dir
129+ case mergeOptions copts (idris_opts pkgdesc) of
130+ Left emsg -> ifail emsg
131+ Right opts -> do
132+ let mod = idris_main pkgdesc
133+ let f = toPath (showCG mod)
134+ putIState orig
135+ dir <- runIO $ getCurrentDirectory
136+ runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc
123137
124− where toPath n = foldl1' (</>) $ splitOn "." n
138+ if (f /= "")
139+ then idrisMain ((Filename f) : opts)
140+ else iputStrLn "Can't start REPL: no main module given"
141+ runIO $ setCurrentDirectory dir
142+
143+ where
144+ toPath n = foldl1' (</>) $ splitOn "." n
125145
126146-- --------------------------------------------------------------- [ Cleaning ]
127147
@@ -129,16 +149,16 @@ replPkg copts fp = do
129149cleanPkg :: [Opt] -- ^ Command line options.
130150 -> FilePath -- ^ Path to ipkg file.
131151 -> IO ()
132−cleanPkg copts fp
133− = do pkgdesc <- parseDesc fp
134− dir <- getCurrentDirectory
135− inPkgDir pkgdesc $
136− do clean (makefile pkgdesc)
137− mapM_ rmIBC (modules pkgdesc)
138− rmIdx (pkgname pkgdesc)
139− case execout pkgdesc of
140− Nothing -> return ()
141− Just s -> rmExe $ dir </> s
152+cleanPkg copts fp = do
153+ pkgdesc <- parseDesc fp
154+ dir <- getCurrentDirectory
155+ inPkgDir pkgdesc $ do
156+ clean (makefile pkgdesc)
157+ mapM_ rmIBC (modules pkgdesc)
158+ rmIdx (pkgname pkgdesc)
159+ case execout pkgdesc of
160+ Nothing -> return ()
161+ Just s -> rmExe $ dir </> s
142162
143163-- ------------------------------------------------------ [ Generate IdrisDoc ]
144164
@@ -152,31 +172,42 @@ cleanPkg copts fp
152172documentPkg :: [Opt] -- ^ Command line options.
153173 -> FilePath -- ^ Path to ipkg file.
154174 -> IO ()
155−documentPkg copts fp =
156− do pkgdesc <- parseDesc fp
157− cd <- getCurrentDirectory
158− let pkgDir = cd </> takeDirectory fp
159− outputDir = cd </> pkgname pkgdesc ++ "_doc"
160− opts = NoREPL : Verbose : idris_opts pkgdesc
161− mods = modules pkgdesc
162− fs = map (foldl1' (</>) . splitOn "." . showCG) mods
163− setCurrentDirectory $ pkgDir </> sourcedir pkgdesc
164− make (makefile pkgdesc)
165− setCurrentDirectory pkgDir
166− let run l = runExceptT . execStateT l
167− load [] = return ()
168− load (f:fs) = do loadModule f IBC_Building; load fs
169− loader = do idrisMain opts; addImportDir (sourcedir pkgdesc); load fs
170− idrisInstance <- run loader idrisInit
171− setCurrentDirectory cd
172− case idrisInstance of
173− Left err -> do putStrLn $ pshow idrisInit err; exitWith (ExitFailure 1)
174− Right ist ->
175− do docRes <- generateDocs ist mods outputDir
176− case docRes of
177− Right _ -> return ()
178− Left msg -> do putStrLn msg
179− exitWith (ExitFailure 1)
175+documentPkg copts fp = do
176+ pkgdesc <- parseDesc fp
177+ cd <- getCurrentDirectory
178+ let pkgDir = cd </> takeDirectory fp
179+ outputDir = cd </> pkgname pkgdesc ++ "_doc"
180+ popts = NoREPL : Verbose : idris_opts pkgdesc
181+ mods = modules pkgdesc
182+ fs = map (foldl1' (</>) . splitOn "." . showCG) mods
183+ setCurrentDirectory $ pkgDir </> sourcedir pkgdesc
184+ make (makefile pkgdesc)
185+ setCurrentDirectory pkgDir
186+ case mergeOptions copts popts of
187+ Left emsg -> do
188+ putStrLn emsg
189+ exitWith (ExitFailure 1)
190+ Right opts -> do
191+ let run l = runExceptT . execStateT l
192+ load [] = return ()
193+ load (f:fs) = do loadModule f IBC_Building; load fs
194+ loader = do
195+ idrisMain opts
196+ addImportDir (sourcedir pkgdesc)
197+ load fs
198+ idrisInstance <- run loader idrisInit
199+ setCurrentDirectory cd
200+ case idrisInstance of
201+ Left err -> do
202+ putStrLn $ pshow idrisInit err
203+ exitWith (ExitFailure 1)
204+ Right ist -> do
205+ docRes <- generateDocs ist mods outputDir
206+ case docRes of
207+ Right _ -> return ()
208+ Left msg -> do
209+ putStrLn msg
210+ exitWith (ExitFailure 1)
180211
181212-- ------------------------------------------------------------------- [ Test ]
182213
@@ -184,36 +215,41 @@ documentPkg copts fp =
184215testPkg :: [Opt] -- ^ Command line options.
185216 -> FilePath -- ^ Path to ipkg file.
186217 -> IO ()
187−testPkg copts fp
188− = do pkgdesc <- parseDesc fp
189− ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc)
190− when (and ok) $
191− do m_ist <- inPkgDir pkgdesc $
192− do make (makefile pkgdesc)
193− -- Get a temporary file to save the tests' source in
194− (tmpn, tmph) <- tempfile ".idr"
195− hPutStrLn tmph $
196− "module Test_______\n" ++
197− concat ["import " ++ show m ++ "\n"
198− | m <- modules pkgdesc] ++
199− "namespace Main\n" ++
200− " main : IO ()\n" ++
201− " main = do " ++
202− concat [show t ++ "\n "
203− | t <- idris_tests pkgdesc]
204− hClose tmph
205− (tmpn', tmph') <- tempfile ""
206− hClose tmph'
207− m_ist <- idris (Filename tmpn : NoREPL : Verbose : Output tmpn' : idris_opts pkgdesc)
208− rawSystem tmpn' []
209− return m_ist
210− case m_ist of
211− Nothing -> exitWith (ExitFailure 1)
212− Just ist -> do
213− -- Quit with error code if problem building
214− case errSpan ist of
215− Just _ -> exitWith (ExitFailure 1)
216− _ -> return ()
218+testPkg copts fp = do
219+ pkgdesc <- parseDesc fp
220+ ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc)
221+ when (and ok) $ do
222+ m_ist <- inPkgDir pkgdesc $ do
223+ make (makefile pkgdesc)
224+ -- Get a temporary file to save the tests' source in
225+ (tmpn, tmph) <- tempfile ".idr"
226+ hPutStrLn tmph $
227+ "module Test_______\n" ++
228+ concat ["import " ++ show m ++ "\n" | m <- modules pkgdesc]
229+ ++ "namespace Main\n"
230+ ++ " main : IO ()\n"
231+ ++ " main = do "
232+ ++ concat [ show t ++ "\n "
233+ | t <- idris_tests pkgdesc]
234+ hClose tmph
235+ (tmpn', tmph') <- tempfile ""
236+ hClose tmph'
237+ let popts = (Filename tmpn : NoREPL : Verbose : Output tmpn' : idris_opts pkgdesc)
238+ case mergeOptions copts popts of
239+ Left emsg -> do
240+ putStrLn emsg
241+ exitWith (ExitFailure 1)
242+ Right opts -> do
243+ m_ist <- idris opts
244+ rawSystem tmpn' []
245+ return m_ist
246+ case m_ist of
247+ Nothing -> exitWith (ExitFailure 1)
248+ Just ist -> do
249+ -- Quit with error code if problem building
250+ case errSpan ist of
251+ Just _ -> exitWith (ExitFailure 1)
252+ _ -> return ()
217253
218254-- ----------------------------------------------------------- [ Installation ]
219255
@@ -328,4 +364,59 @@ clean Nothing = return ()
328364clean (Just s) = do rawSystem "make" ["-f", s, "clean"]
329365 return ()
330366
367+-- | Merge an option list representing the command line options into
368+-- those specified for a package description.
369+--
370+-- This is not a complete union between the two options sets. First,
371+-- to prevent important package specified options from being
372+-- overwritten. Second, the semantics for this merge are not fully
373+-- defined.
374+--
375+-- A discussion for this is on the issue tracker:
376+-- https://github.com/idris-lang/Idris-dev/issues/1448
377+--
378+mergeOptions :: [Opt] -- ^ The command line options
379+ -> [Opt] -- ^ The package options
380+ -> Either String [Opt]
381+mergeOptions copts popts =
382+ case partitionEithers (map chkOpt (normaliseOpts copts)) of
383+ ([], copts') -> Right $ copts' ++ popts
384+ (es, _) -> Left $ genErrMsg es
385+ where
386+ normaliseOpts :: [Opt] -> [Opt]
387+ normaliseOpts = filter filtOpt
388+
389+ filtOpt :: Opt -> Bool
390+ filtOpt (PkgBuild _) = False
391+ filtOpt (PkgInstall _) = False
392+ filtOpt (PkgClean _) = False
393+ filtOpt (PkgCheck _) = False
394+ filtOpt (PkgREPL _) = False
395+ filtOpt (PkgMkDoc _) = False
396+ filtOpt (PkgTest _) = False
397+ filtOpt _ = True
398+
399+ chkOpt :: Opt -> Either String Opt
400+ chkOpt o@(OLogging _) = Right o
401+ chkOpt o@(OLogCats _) = Right o
402+ chkOpt o@(DefaultTotal) = Right o
403+ chkOpt o@(DefaultPartial) = Right o
404+ chkOpt o@(WarnPartial) = Right o
405+ chkOpt o@(WarnReach) = Right o
406+ chkOpt o@(IBCSubDir _) = Right o
407+ chkOpt o@(ImportDir _ ) = Right o
408+ chkOpt o@(UseCodegen _) = Right o
409+ chkOpt o = Left (unwords ["\t", show o, "\n"])
410+
411+ genErrMsg :: [String] -> String
412+ genErrMsg es = unlines
413+ [ "Not all command line options can be used to override package options."
414+ , "\nThe only changeable options are:"
415+ , "\t--log <lvl>, --total, --warnpartial, --warnreach"
416+ , "\t--ibcsubdir <path>, -i --idrispath <path>"
417+ , "\t--logging-categories <cats>"
418+ , "\nThe options need removing are:"
419+ , unlines es
420+ ]
421+
331422-- --------------------------------------------------------------------- [ EOF ]