git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3071 from jfdm/fix-cli-and-pkg-options
ba53b91Jan de Muijnck-Hughes
CHANGELOG+6
compare with master
unifiedsplit
@@ -4,6 +4,12 @@ New in 0.12:
4* Improved startup performance by reducing the processing of an already imported
4* Improved startup performance by reducing the processing of an already imported
5 module that has changed accessibility.
5 module that has changed accessibility.
6
6
7+* A limited set of command line options can be used to override
8+ package declared options. Overridable options are currently,
9+ logging level and categories, default totality check, warn reach,
10+ IBC output folder, and idris path.
11+
12+
7New in 0.11:
13New in 0.11:
8============
14============
9
15
main/Main.hs+6−6
@@ -56,26 +56,26 @@ runIdris opts = do
56 runIO exitSuccess
56 runIO exitSuccess
57 case opt getPkgCheck opts of
57 case opt getPkgCheck opts of
58 [] -> return ()
58 [] -> return ()
59− fs -> do runIO $ mapM_ (checkPkg (WarnOnly `elem` opts) True) fs
59+ fs -> do runIO $ mapM_ (checkPkg opts (WarnOnly `elem` opts) True) fs
60 runIO exitSuccess
60 runIO exitSuccess
61 case opt getPkgClean opts of
61 case opt getPkgClean opts of
62 [] -> return ()
62 [] -> return ()
63− fs -> do runIO $ mapM_ cleanPkg fs
63+ fs -> do runIO $ mapM_ (cleanPkg opts) fs
64 runIO exitSuccess
64 runIO exitSuccess
65 case opt getPkgMkDoc opts of -- IdrisDoc
65 case opt getPkgMkDoc opts of -- IdrisDoc
66 [] -> return ()
66 [] -> return ()
67− fs -> do runIO $ mapM_ documentPkg fs
67+ fs -> do runIO $ mapM_ (documentPkg opts) fs
68 runIO exitSuccess
68 runIO exitSuccess
69 case opt getPkgTest opts of
69 case opt getPkgTest opts of
70 [] -> return ()
70 [] -> return ()
71− fs -> do runIO $ mapM_ testPkg fs
71+ fs -> do runIO $ mapM_ (testPkg opts) fs
72 runIO exitSuccess
72 runIO exitSuccess
73 case opt getPkg opts of
73 case opt getPkg opts of
74 [] -> case opt getPkgREPL opts of
74 [] -> case opt getPkgREPL opts of
75 [] -> idrisMain opts
75 [] -> idrisMain opts
76− [f] -> replPkg f
76+ [f] -> replPkg opts f
77 _ -> ifail "Too many packages"
77 _ -> ifail "Too many packages"
78− fs -> runIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs
78+ fs -> runIO $ mapM_ (buildPkg opts (WarnOnly `elem` opts)) fs
79
79
80showver :: IO b
80showver :: IO b
81showver = do putStrLn $ "Idris version " ++ ver
81showver = do putStrLn $ "Idris version " ++ ver
src/Pkg/Package.hs+249−129
@@ -18,6 +18,8 @@ import Control.Monad.Trans.Except (runExceptT)
18import Data.List
18import Data.List
19import Data.List.Split(splitOn)
19import Data.List.Split(splitOn)
20
20
21+import Data.Either
22+
21import Idris.Core.TT
23import Idris.Core.TT
22import Idris.REPL
24import Idris.REPL
23import Idris.Parser (loadModule)
25import Idris.Parser (loadModule)
@@ -27,6 +29,7 @@ import Idris.IdrisDoc
27import Idris.IBC
29import Idris.IBC
28import Idris.Output
30import Idris.Output
29import Idris.Imports
31import Idris.Imports
32+import Idris.Error (ifail)
30
33
31import Pkg.PParser
34import Pkg.PParser
32
35
@@ -39,87 +42,126 @@ import IRTS.System
39-- * invoke idris on each module, with idris_opts
42-- * invoke idris on each module, with idris_opts
40-- * install everything into datadir/pname, if install flag is set
43-- * install everything into datadir/pname, if install flag is set
41
44
45+-- --------------------------------------------------------- [ Build Packages ]
46+
42-- | Run the package through the idris compiler.
47-- | Run the package through the idris compiler.
43−buildPkg :: Bool -> (Bool, FilePath) -> IO ()
48+buildPkg :: [Opt] -- ^ Command line options
49+ -> Bool -- ^ Provide Warnings
50+ -> (Bool, FilePath) -- ^ (Should we install, Location of iPKG file)
51+ -> IO ()
44−buildPkg warnonly (install, fp)
52+buildPkg copts warnonly (install, fp) = do
45− = do pkgdesc <- parseDesc fp
53+ pkgdesc <- parseDesc fp
46− dir <- getCurrentDirectory
54+ dir <- getCurrentDirectory
47− let idx = PkgIndex (pkgIndex (pkgname pkgdesc))
55+ let idx = PkgIndex (pkgIndex (pkgname pkgdesc))
48− ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
56+ oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
49− when (and ok) $
57+ when (and oks) $ do
50− do m_ist <- inPkgDir pkgdesc $
58+ m_ist <- inPkgDir pkgdesc $ do
59+
51− do make (makefile pkgdesc)
60+ make (makefile pkgdesc)
52− case (execout pkgdesc) of
61+ case (execout pkgdesc) of
62+ Nothing -> do
53− Nothing -> buildMods (idx : NoREPL : Verbose : idris_opts pkgdesc)
63+ case mergeOptions copts (idx : NoREPL : Verbose : idris_opts pkgdesc) of
64+ Left emsg -> do
65+ putStrLn emsg
66+ exitWith (ExitFailure 1)
54− (modules pkgdesc)
67+ Right opts -> buildMods opts (modules pkgdesc)
68+ Just o -> do
55− Just o -> do let exec = dir </> o
69+ let exec = dir </> o
56− buildMods
57− (idx : NoREPL : Verbose : Output exec : idris_opts pkgdesc)
70+ case mergeOptions copts (idx : NoREPL : Verbose : Output exec : idris_opts pkgdesc) of
71+ Left emsg -> do
72+ putStrLn emsg
73+ exitWith (ExitFailure 1)
58− [idris_main pkgdesc]
74+ Right opts -> buildMods opts [idris_main pkgdesc]
59− case m_ist of
75+ case m_ist of
60− Nothing -> exitWith (ExitFailure 1)
76+ Nothing -> exitWith (ExitFailure 1)
61− Just ist -> do
77+ Just ist -> do
62− -- Quit with error code if there was a problem
78+ -- Quit with error code if there was a problem
63− case errSpan ist of
79+ case errSpan ist of
64− Just _ -> exitWith (ExitFailure 1)
80+ Just _ -> exitWith (ExitFailure 1)
65− _ -> return ()
81+ _ -> return ()
66− when install $ installPkg pkgdesc
82+ when install $ installPkg pkgdesc
83+
84+-- --------------------------------------------------------- [ Check Packages ]
67
85
68-- | Type check packages only
86-- | Type check packages only
69--
87--
70-- This differs from build in that executables are not built, if the
88-- This differs from build in that executables are not built, if the
71-- package contains an executable.
89-- package contains an executable.
90+checkPkg :: [Opt] -- ^ Command line Options
72−checkPkg :: Bool -- ^ Show Warnings
91+ -> Bool -- ^ Show Warnings
73− -> Bool -- ^ quit on failure
92+ -> Bool -- ^ quit on failure
74− -> FilePath -- ^ Path to ipkg file.
93+ -> FilePath -- ^ Path to ipkg file.
75− -> IO ()
94+ -> IO ()
76−checkPkg warnonly quit fpath
95+checkPkg copts warnonly quit fpath = do
77− = do pkgdesc <- parseDesc fpath
96+ pkgdesc <- parseDesc fpath
78− ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
97+ oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
79− when (and ok) $
98+ when (and oks) $ do
80− do res <- inPkgDir pkgdesc $
99+ res <- inPkgDir pkgdesc $ do
81− do make (makefile pkgdesc)
100+ make (makefile pkgdesc)
101+
82− buildMods (NoREPL : Verbose : idris_opts pkgdesc)
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
83− (modules pkgdesc)
107+ buildMods opts (modules pkgdesc)
84− when quit $ case res of
108+ when quit $ case res of
85− Nothing -> exitWith (ExitFailure 1)
109+ Nothing -> exitWith (ExitFailure 1)
86− Just res' -> do
110+ Just res' -> do
87− case errSpan res' of
111+ case errSpan res' of
88− Just _ -> exitWith (ExitFailure 1)
112+ Just _ -> exitWith (ExitFailure 1)
89− _ -> return ()
113+ _ -> 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
107
114
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
108− where toPath n = foldl1' (</>) $ splitOn "." n
144+ toPath n = foldl1' (</>) $ splitOn "." n
145+
146+-- --------------------------------------------------------------- [ Cleaning ]
109
147
110-- | Clean Package build files
148-- | Clean Package build files
149+cleanPkg :: [Opt] -- ^ Command line options.
111−cleanPkg :: FilePath -- ^ Path to ipkg file.
150+ -> FilePath -- ^ Path to ipkg file.
112 -> IO ()
151 -> IO ()
113−cleanPkg fp
152+cleanPkg copts fp = do
114− = do pkgdesc <- parseDesc fp
153+ pkgdesc <- parseDesc fp
115− dir <- getCurrentDirectory
154+ dir <- getCurrentDirectory
116− inPkgDir pkgdesc $
155+ inPkgDir pkgdesc $ do
117− do clean (makefile pkgdesc)
156+ clean (makefile pkgdesc)
118− mapM_ rmIBC (modules pkgdesc)
157+ mapM_ rmIBC (modules pkgdesc)
119− rmIdx (pkgname pkgdesc)
158+ rmIdx (pkgname pkgdesc)
120− case execout pkgdesc of
159+ case execout pkgdesc of
121− Nothing -> return ()
160+ Nothing -> return ()
122− Just s -> rmExe $ dir </> s
161+ Just s -> rmExe $ dir </> s
162+
163+-- ------------------------------------------------------ [ Generate IdrisDoc ]
164+
123
165
124-- | Generate IdrisDoc for package
166-- | Generate IdrisDoc for package
125-- TODO: Handle case where module does not contain a matching namespace
167-- TODO: Handle case where module does not contain a matching namespace
@@ -127,66 +169,89 @@ cleanPkg fp
127--
169--
128-- Issue number #1572 on the issue tracker
170-- Issue number #1572 on the issue tracker
129-- https://github.com/idris-lang/Idris-dev/issues/1572
171-- https://github.com/idris-lang/Idris-dev/issues/1572
172+documentPkg :: [Opt] -- ^ Command line options.
130−documentPkg :: FilePath -- ^ Path to .ipkg file.
173+ -> FilePath -- ^ Path to ipkg file.
131 -> IO ()
174 -> IO ()
132−documentPkg fp =
175+documentPkg copts fp = do
133− do pkgdesc <- parseDesc fp
176+ pkgdesc <- parseDesc fp
134− cd <- getCurrentDirectory
177+ cd <- getCurrentDirectory
135− let pkgDir = cd </> takeDirectory fp
178+ let pkgDir = cd </> takeDirectory fp
136− outputDir = cd </> pkgname pkgdesc ++ "_doc"
179+ outputDir = cd </> pkgname pkgdesc ++ "_doc"
137− opts = NoREPL : Verbose : idris_opts pkgdesc
180+ popts = NoREPL : Verbose : idris_opts pkgdesc
138− mods = modules pkgdesc
181+ mods = modules pkgdesc
139− fs = map (foldl1' (</>) . splitOn "." . showCG) mods
182+ fs = map (foldl1' (</>) . splitOn "." . showCG) mods
140− setCurrentDirectory $ pkgDir </> sourcedir pkgdesc
183+ setCurrentDirectory $ pkgDir </> sourcedir pkgdesc
141− make (makefile pkgdesc)
184+ make (makefile pkgdesc)
142− setCurrentDirectory pkgDir
185+ setCurrentDirectory pkgDir
186+ case mergeOptions copts popts of
187+ Left emsg -> do
188+ putStrLn emsg
189+ exitWith (ExitFailure 1)
190+ Right opts -> do
143− let run l = runExceptT . execStateT l
191+ let run l = runExceptT . execStateT l
144− load [] = return ()
192+ load [] = return ()
145− load (f:fs) = do loadModule f IBC_Building; load fs
193+ load (f:fs) = do loadModule f IBC_Building; load fs
194+ loader = do
195+ idrisMain opts
146− loader = do idrisMain opts; addImportDir (sourcedir pkgdesc); load fs
196+ addImportDir (sourcedir pkgdesc)
197+ load fs
147− idrisInstance <- run loader idrisInit
198+ idrisInstance <- run loader idrisInit
148− setCurrentDirectory cd
199+ setCurrentDirectory cd
149− case idrisInstance of
200+ case idrisInstance of
201+ Left err -> do
150− Left err -> do putStrLn $ pshow idrisInit err; exitWith (ExitFailure 1)
202+ putStrLn $ pshow idrisInit err
203+ exitWith (ExitFailure 1)
151− Right ist ->
204+ Right ist -> do
152− do docRes <- generateDocs ist mods outputDir
205+ docRes <- generateDocs ist mods outputDir
153− case docRes of
206+ case docRes of
154− Right _ -> return ()
207+ Right _ -> return ()
208+ Left msg -> do
155− Left msg -> do putStrLn msg
209+ putStrLn msg
156− exitWith (ExitFailure 1)
210+ exitWith (ExitFailure 1)
211+
212+-- ------------------------------------------------------------------- [ Test ]
157
213
158-- | Build a package with a sythesized main function that runs the tests
214-- | Build a package with a sythesized main function that runs the tests
159−testPkg :: FilePath -> IO ()
215+testPkg :: [Opt] -- ^ Command line options.
160−testPkg fp
216+ -> FilePath -- ^ Path to ipkg file.
217+ -> IO ()
218+testPkg copts fp = do
161− = do pkgdesc <- parseDesc fp
219+ pkgdesc <- parseDesc fp
162− ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc)
220+ ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc)
163− when (and ok) $
221+ when (and ok) $ do
164− do m_ist <- inPkgDir pkgdesc $
222+ m_ist <- inPkgDir pkgdesc $ do
165− do make (makefile pkgdesc)
223+ make (makefile pkgdesc)
166− -- Get a temporary file to save the tests' source in
224+ -- Get a temporary file to save the tests' source in
167− (tmpn, tmph) <- tempfile ".idr"
225+ (tmpn, tmph) <- tempfile ".idr"
168− hPutStrLn tmph $
226+ hPutStrLn tmph $
169− "module Test_______\n" ++
227+ "module Test_______\n" ++
170− concat ["import " ++ show m ++ "\n"
228+ concat ["import " ++ show m ++ "\n" | m <- modules pkgdesc]
171− | m <- modules pkgdesc] ++
172− "namespace Main\n" ++
229+ ++ "namespace Main\n"
173− " main : IO ()\n" ++
230+ ++ " main : IO ()\n"
174− " main = do " ++
231+ ++ " main = do "
175− concat [show t ++ "\n "
232+ ++ concat [ show t ++ "\n "
176− | t <- idris_tests pkgdesc]
233+ | t <- idris_tests pkgdesc]
177− hClose tmph
234+ hClose tmph
178− (tmpn', tmph') <- tempfile ""
235+ (tmpn', tmph') <- tempfile ""
179− hClose tmph'
236+ hClose tmph'
180− m_ist <- idris (Filename tmpn : NoREPL : Verbose : Output tmpn' : idris_opts pkgdesc)
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
181− rawSystem tmpn' []
244+ rawSystem tmpn' []
182− return m_ist
245+ return m_ist
183− case m_ist of
246+ case m_ist of
184− Nothing -> exitWith (ExitFailure 1)
247+ Nothing -> exitWith (ExitFailure 1)
185− Just ist -> do
248+ Just ist -> do
186− -- Quit with error code if problem building
249+ -- Quit with error code if problem building
187− case errSpan ist of
250+ case errSpan ist of
188− Just _ -> exitWith (ExitFailure 1)
251+ Just _ -> exitWith (ExitFailure 1)
189− _ -> return ()
252+ _ -> return ()
253+
254+-- ----------------------------------------------------------- [ Installation ]
190
255
191-- | Install package
256-- | Install package
192installPkg :: PkgDesc -> IO ()
257installPkg :: PkgDesc -> IO ()
@@ -254,7 +319,7 @@ installIBC p m = do let f = toIBCFile m
254installIdx :: String -> IO ()
319installIdx :: String -> IO ()
255installIdx p = do d <- getTargetDir
320installIdx p = do d <- getTargetDir
256 let f = pkgIndex p
321 let f = pkgIndex p
257− let destdir = d </> p
322+ let destdir = d </> p
258 putStrLn $ "Installing " ++ f ++ " to " ++ destdir
323 putStrLn $ "Installing " ++ f ++ " to " ++ destdir
259 createDirectoryIfMissing True destdir
324 createDirectoryIfMissing True destdir
260 copyFile f (destdir </> takeFileName f)
325 copyFile f (destdir </> takeFileName f)
@@ -299,4 +364,59 @@ clean Nothing = return ()
299clean (Just s) = do rawSystem "make" ["-f", s, "clean"]
364clean (Just s) = do rawSystem "make" ["-f", s, "clean"]
300 return ()
365 return ()
301
366
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+
302-- --------------------------------------------------------------------- [ EOF ]
422-- --------------------------------------------------------------------- [ EOF ]
test/pkg001/expected+19
@@ -0,0 +1,19 @@
1+Not all command line options can be used to override package options.
2+
3+The only changeable options are:
4+ --log <lvl>, --total, --warnpartial, --warnreach
5+ --ibcsubdir <path>, -i --idrispath <path>
6+ --logging-categories <cats>
7+
8+The options need removing are:
9+ Quiet
10+
11+
12+
13+Elaborating {__Infer0}
14+builtin
15+Elaborating =
16+builtin
17+Elaborating type decl Main.main[]
18+Elaborating clause Main.main
19+Rechecking for positivity []
test/pkg001/run+2
@@ -1,3 +1,5 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
2${IDRIS:-idris} $@ --build test.ipkg
2${IDRIS:-idris} $@ --build test.ipkg
3rm -f *.ibc
3rm -f *.ibc
4+${IDRIS:-idris} $@ --build test.ipkg --quiet
5+${IDRIS:-idris} $@ --build test.ipkg --logging-categories "elab" --log 1