@@ -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
@@ -39,87 +42,126 @@ import IRTS.System
3942-- * invoke idris on each module, with idris_opts
4043-- * install everything into datadir/pname, if install flag is set
4144
45+-- --------------------------------------------------------- [ Build Packages ]
46+
4247-- | Run the package through the idris compiler.
43−buildPkg :: Bool -> (Bool, FilePath) -> IO ()
44−buildPkg warnonly (install, fp)
45− = do pkgdesc <- parseDesc fp
46− dir <- getCurrentDirectory
47− let idx = PkgIndex (pkgIndex (pkgname pkgdesc))
48− ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
49− when (and ok) $
50− do m_ist <- inPkgDir pkgdesc $
51− do make (makefile pkgdesc)
52− case (execout pkgdesc) of
53− Nothing -> buildMods (idx : NoREPL : Verbose : idris_opts pkgdesc)
54− (modules pkgdesc)
55− Just o -> do let exec = dir </> o
56− buildMods
57− (idx : NoREPL : Verbose : Output exec : idris_opts pkgdesc)
58− [idris_main pkgdesc]
59− case m_ist of
60− Nothing -> exitWith (ExitFailure 1)
61− Just ist -> do
62− -- Quit with error code if there was a problem
63− case errSpan ist of
64− Just _ -> exitWith (ExitFailure 1)
65− _ -> return ()
66− when install $ installPkg pkgdesc
48+buildPkg :: [Opt] -- ^ Command line options
49+ -> Bool -- ^ Provide Warnings
50+ -> (Bool, FilePath) -- ^ (Should we install, Location of iPKG file)
51+ -> IO ()
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
83+
84+-- --------------------------------------------------------- [ Check Packages ]
6785
6886-- | Type check packages only
6987--
7088-- This differs from build in that executables are not built, if the
7189-- package contains an executable.
72−checkPkg :: Bool -- ^ Show Warnings
73− -> Bool -- ^ quit on failure
74− -> FilePath -- ^ Path to ipkg file.
75− -> IO ()
76−checkPkg warnonly quit fpath
77− = do pkgdesc <- parseDesc fpath
78− ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
79− when (and ok) $
80− do res <- inPkgDir pkgdesc $
81− do make (makefile pkgdesc)
82− buildMods (NoREPL : Verbose : idris_opts pkgdesc)
83− (modules pkgdesc)
84− when quit $ case res of
85− Nothing -> exitWith (ExitFailure 1)
86− Just res' -> do
87− case errSpan res' of
88− Just _ -> exitWith (ExitFailure 1)
89− _ -> return ()
90−
91−-- | Check a package and start a REPL
92−replPkg :: FilePath -> Idris ()
93−replPkg fp = do orig <- getIState
94− runIO $ checkPkg False False fp
95− pkgdesc <- runIO $ parseDesc fp -- bzzt, repetition!
96− let opts = idris_opts pkgdesc
97− let mod = idris_main pkgdesc
98− let f = toPath (showCG mod)
99− putIState orig
100− dir <- runIO $ getCurrentDirectory
101− runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc
102−
103− if (f /= "")
104− then idrisMain ((Filename f) : opts)
105− else iputStrLn "Can't start REPL: no main module given"
106− runIO $ setCurrentDirectory dir
90+checkPkg :: [Opt] -- ^ Command line Options
91+ -> Bool -- ^ Show Warnings
92+ -> Bool -- ^ quit on failure
93+ -> FilePath -- ^ Path to ipkg file.
94+ -> IO ()
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 ()
107114
108− where toPath n = foldl1' (</>) $ splitOn "." n
115+-- ------------------------------------------------------------------- [ REPL ]
116+
117+-- | Check a package and start a REPL.
118+--
119+-- This function only works with packages that have a main module.
120+--
121+replPkg :: [Opt] -- ^ Command line Options
122+ -> FilePath -- ^ Path to ipkg file.
123+ -> Idris ()
124+replPkg copts fp = do
125+ orig <- getIState
126+ runIO $ checkPkg copts False False fp
127+ pkgdesc <- runIO $ parseDesc fp -- bzzt, repetition!
128+
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
137+
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
145+
146+-- --------------------------------------------------------------- [ Cleaning ]
109147
110148-- | Clean Package build files
111−cleanPkg :: FilePath -- ^ Path to ipkg file.
149+cleanPkg :: [Opt] -- ^ Command line options.
150+ -> FilePath -- ^ Path to ipkg file.
112151 -> IO ()
113−cleanPkg fp
114− = do pkgdesc <- parseDesc fp
115− dir <- getCurrentDirectory
116− inPkgDir pkgdesc $
117− do clean (makefile pkgdesc)
118− mapM_ rmIBC (modules pkgdesc)
119− rmIdx (pkgname pkgdesc)
120− case execout pkgdesc of
121− Nothing -> return ()
122− 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
162+
163+-- ------------------------------------------------------ [ Generate IdrisDoc ]
164+
123165
124166-- | Generate IdrisDoc for package
125167-- TODO: Handle case where module does not contain a matching namespace
@@ -127,66 +169,89 @@ cleanPkg fp
127169--
128170-- Issue number #1572 on the issue tracker
129171-- https://github.com/idris-lang/Idris-dev/issues/1572
130−documentPkg :: FilePath -- ^ Path to .ipkg file.
172+documentPkg :: [Opt] -- ^ Command line options.
173+ -> FilePath -- ^ Path to ipkg file.
131174 -> IO ()
132−documentPkg fp =
133− do pkgdesc <- parseDesc fp
134− cd <- getCurrentDirectory
135− let pkgDir = cd </> takeDirectory fp
136− outputDir = cd </> pkgname pkgdesc ++ "_doc"
137− opts = NoREPL : Verbose : idris_opts pkgdesc
138− mods = modules pkgdesc
139− fs = map (foldl1' (</>) . splitOn "." . showCG) mods
140− setCurrentDirectory $ pkgDir </> sourcedir pkgdesc
141− make (makefile pkgdesc)
142− setCurrentDirectory pkgDir
143− let run l = runExceptT . execStateT l
144− load [] = return ()
145− load (f:fs) = do loadModule f IBC_Building; load fs
146− loader = do idrisMain opts; addImportDir (sourcedir pkgdesc); load fs
147− idrisInstance <- run loader idrisInit
148− setCurrentDirectory cd
149− case idrisInstance of
150− Left err -> do putStrLn $ pshow idrisInit err; exitWith (ExitFailure 1)
151− Right ist ->
152− do docRes <- generateDocs ist mods outputDir
153− case docRes of
154− Right _ -> return ()
155− Left msg -> do putStrLn msg
156− 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)
211+
212+-- ------------------------------------------------------------------- [ Test ]
157213
158214-- | Build a package with a sythesized main function that runs the tests
159−testPkg :: FilePath -> IO ()
160−testPkg fp
161− = do pkgdesc <- parseDesc fp
162− ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc)
163− when (and ok) $
164− do m_ist <- inPkgDir pkgdesc $
165− do make (makefile pkgdesc)
166− -- Get a temporary file to save the tests' source in
167− (tmpn, tmph) <- tempfile ".idr"
168− hPutStrLn tmph $
169− "module Test_______\n" ++
170− concat ["import " ++ show m ++ "\n"
171− | m <- modules pkgdesc] ++
172− "namespace Main\n" ++
173− " main : IO ()\n" ++
174− " main = do " ++
175− concat [show t ++ "\n "
176− | t <- idris_tests pkgdesc]
177− hClose tmph
178− (tmpn', tmph') <- tempfile ""
179− hClose tmph'
180− m_ist <- idris (Filename tmpn : NoREPL : Verbose : Output tmpn' : idris_opts pkgdesc)
181− rawSystem tmpn' []
182− return m_ist
183− case m_ist of
184− Nothing -> exitWith (ExitFailure 1)
185− Just ist -> do
186− -- Quit with error code if problem building
187− case errSpan ist of
188− Just _ -> exitWith (ExitFailure 1)
189− _ -> return ()
215+testPkg :: [Opt] -- ^ Command line options.
216+ -> FilePath -- ^ Path to ipkg file.
217+ -> IO ()
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 ()
253+
254+-- ----------------------------------------------------------- [ Installation ]
190255
191256-- | Install package
192257installPkg :: PkgDesc -> IO ()
@@ -254,7 +319,7 @@ installIBC p m = do let f = toIBCFile m
254319installIdx :: String -> IO ()
255320installIdx p = do d <- getTargetDir
256321 let f = pkgIndex p
257− let destdir = d </> p
322+ let destdir = d </> p
258323 putStrLn $ "Installing " ++ f ++ " to " ++ destdir
259324 createDirectoryIfMissing True destdir
260325 copyFile f (destdir </> takeFileName f)
@@ -299,4 +364,59 @@ clean Nothing = return ()
299364clean (Just s) = do rawSystem "make" ["-f", s, "clean"]
300365 return ()
301366
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+
302422-- --------------------------------------------------------------------- [ EOF ]