62b4876 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow certain CLI options to work when using iPKG files.

62b4876Jan de Muijnck-Hughes11 years ago

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

5 module that has changed accessibility.

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============

src/Pkg/Package.hs+204−113

@@ -18,6 +18,8 @@ import Control.Monad.Trans.Except (runExceptT)

18import Data.List

19import Data.List.Split(splitOn)

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)

31import Pkg.PParser

34import Pkg.PParser

@@ -46,29 +49,37 @@ buildPkg :: [Opt] -- ^ Command line options

46 -> Bool -- ^ Provide Warnings

49 -> Bool -- ^ Provide Warnings

47 -> (Bool, FilePath) -- ^ (Should we install, Location of iPKG file)

50 -> (Bool, FilePath) -- ^ (Should we install, Location of iPKG file)

48 -> IO ()

51 -> IO ()

49−buildPkg copts warnonly (install, fp)

52+buildPkg copts warnonly (install, fp) = do

50− = do pkgdesc <- parseDesc fp

53+ pkgdesc <- parseDesc fp

51− dir <- getCurrentDirectory

54+ dir <- getCurrentDirectory

52− let idx = PkgIndex (pkgIndex (pkgname pkgdesc))

55+ let idx = PkgIndex (pkgIndex (pkgname pkgdesc))

53− ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)

56+ oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)

54− when (and ok) $

57+ when (and oks) $ do

55− do m_ist <- inPkgDir pkgdesc $

58+ m_ist <- inPkgDir pkgdesc $ do

59+

56− do make (makefile pkgdesc)

60+ make (makefile pkgdesc)

57− case (execout pkgdesc) of

61+ case (execout pkgdesc) of

62+ Nothing -> do

58− 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)

59− (modules pkgdesc)

67+ Right opts -> buildMods opts (modules pkgdesc)

68+ Just o -> do

60− Just o -> do let exec = dir </> o

69+ let exec = dir </> o

61− buildMods

62− (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)

63− [idris_main pkgdesc]

74+ Right opts -> buildMods opts [idris_main pkgdesc]

64− case m_ist of

75+ case m_ist of

65− Nothing -> exitWith (ExitFailure 1)

76+ Nothing -> exitWith (ExitFailure 1)

66− Just ist -> do

77+ Just ist -> do

67− -- Quit with error code if there was a problem

78+ -- Quit with error code if there was a problem

68− case errSpan ist of

79+ case errSpan ist of

69− Just _ -> exitWith (ExitFailure 1)

80+ Just _ -> exitWith (ExitFailure 1)

70− _ -> return ()

81+ _ -> return ()

71− when install $ installPkg pkgdesc

82+ when install $ installPkg pkgdesc

73-- --------------------------------------------------------- [ Check Packages ]

84-- --------------------------------------------------------- [ Check Packages ]

@@ -81,20 +92,25 @@ checkPkg :: [Opt] -- ^ Command line Options

81 -> Bool -- ^ quit on failure

92 -> Bool -- ^ quit on failure

82 -> FilePath -- ^ Path to ipkg file.

93 -> FilePath -- ^ Path to ipkg file.

83 -> IO ()

94 -> IO ()

84−checkPkg copts warnonly quit fpath

95+checkPkg copts warnonly quit fpath = do

85− = do pkgdesc <- parseDesc fpath

96+ pkgdesc <- parseDesc fpath

86− ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)

97+ oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)

87− when (and ok) $

98+ when (and oks) $ do

88− do res <- inPkgDir pkgdesc $

99+ res <- inPkgDir pkgdesc $ do

89− do make (makefile pkgdesc)

100+ make (makefile pkgdesc)

101+

90− 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

91− (modules pkgdesc)

107+ buildMods opts (modules pkgdesc)

92− when quit $ case res of

108+ when quit $ case res of

93− Nothing -> exitWith (ExitFailure 1)

109+ Nothing -> exitWith (ExitFailure 1)

94− Just res' -> do

110+ Just res' -> do

95− case errSpan res' of

111+ case errSpan res' of

96− Just _ -> exitWith (ExitFailure 1)

112+ Just _ -> exitWith (ExitFailure 1)

97− _ -> return ()

113+ _ -> return ()

114

99-- ------------------------------------------------------------------- [ REPL ]

115-- ------------------------------------------------------------------- [ REPL ]

100

116

@@ -109,19 +125,23 @@ replPkg copts fp = do

109 orig <- getIState

125 orig <- getIState

110 runIO $ checkPkg copts False False fp

126 runIO $ checkPkg copts False False fp

111 pkgdesc <- runIO $ parseDesc fp -- bzzt, repetition!

127 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

118

128

119− if (f /= "")

129+ case mergeOptions copts (idris_opts pkgdesc) of

120− then idrisMain ((Filename f) : opts)

130+ Left emsg -> ifail emsg

121− else iputStrLn "Can't start REPL: no main module given"

131+ Right opts -> do

132+ let mod = idris_main pkgdesc

133+ let f = toPath (showCG mod)

134+ putIState orig

135+ dir <- runIO $ getCurrentDirectory

122− runIO $ setCurrentDirectory dir

136+ runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc

123

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

124− where toPath n = foldl1' (</>) $ splitOn "." n

144+ toPath n = foldl1' (</>) $ splitOn "." n

125

145

126-- --------------------------------------------------------------- [ Cleaning ]

146-- --------------------------------------------------------------- [ Cleaning ]

127

147

@@ -129,16 +149,16 @@ replPkg copts fp = do

129cleanPkg :: [Opt] -- ^ Command line options.

149cleanPkg :: [Opt] -- ^ Command line options.

130 -> FilePath -- ^ Path to ipkg file.

150 -> FilePath -- ^ Path to ipkg file.

131 -> IO ()

151 -> IO ()

132−cleanPkg copts fp

152+cleanPkg copts fp = do

133− = do pkgdesc <- parseDesc fp

153+ pkgdesc <- parseDesc fp

134− dir <- getCurrentDirectory

154+ dir <- getCurrentDirectory

135− inPkgDir pkgdesc $

155+ inPkgDir pkgdesc $ do

136− do clean (makefile pkgdesc)

156+ clean (makefile pkgdesc)

137− mapM_ rmIBC (modules pkgdesc)

157+ mapM_ rmIBC (modules pkgdesc)

138− rmIdx (pkgname pkgdesc)

158+ rmIdx (pkgname pkgdesc)

139− case execout pkgdesc of

159+ case execout pkgdesc of

140− Nothing -> return ()

160+ Nothing -> return ()

141− Just s -> rmExe $ dir </> s

161+ Just s -> rmExe $ dir </> s

142

162

143-- ------------------------------------------------------ [ Generate IdrisDoc ]

163-- ------------------------------------------------------ [ Generate IdrisDoc ]

144

164

@@ -152,31 +172,42 @@ cleanPkg copts fp

152documentPkg :: [Opt] -- ^ Command line options.

172documentPkg :: [Opt] -- ^ Command line options.

153 -> FilePath -- ^ Path to ipkg file.

173 -> FilePath -- ^ Path to ipkg file.

154 -> IO ()

174 -> IO ()

155−documentPkg copts fp =

175+documentPkg copts fp = do

156− do pkgdesc <- parseDesc fp

176+ pkgdesc <- parseDesc fp

157− cd <- getCurrentDirectory

177+ cd <- getCurrentDirectory

158− let pkgDir = cd </> takeDirectory fp

178+ let pkgDir = cd </> takeDirectory fp

159− outputDir = cd </> pkgname pkgdesc ++ "_doc"

179+ outputDir = cd </> pkgname pkgdesc ++ "_doc"

160− opts = NoREPL : Verbose : idris_opts pkgdesc

180+ popts = NoREPL : Verbose : idris_opts pkgdesc

161− mods = modules pkgdesc

181+ mods = modules pkgdesc

162− fs = map (foldl1' (</>) . splitOn "." . showCG) mods

182+ fs = map (foldl1' (</>) . splitOn "." . showCG) mods

163− setCurrentDirectory $ pkgDir </> sourcedir pkgdesc

183+ setCurrentDirectory $ pkgDir </> sourcedir pkgdesc

164− make (makefile pkgdesc)

184+ make (makefile pkgdesc)

165− 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

166− let run l = runExceptT . execStateT l

191+ let run l = runExceptT . execStateT l

167− load [] = return ()

192+ load [] = return ()

168− 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

169− loader = do idrisMain opts; addImportDir (sourcedir pkgdesc); load fs

196+ addImportDir (sourcedir pkgdesc)

197+ load fs

170− idrisInstance <- run loader idrisInit

198+ idrisInstance <- run loader idrisInit

171− setCurrentDirectory cd

199+ setCurrentDirectory cd

172− case idrisInstance of

200+ case idrisInstance of

201+ Left err -> do

173− Left err -> do putStrLn $ pshow idrisInit err; exitWith (ExitFailure 1)

202+ putStrLn $ pshow idrisInit err

203+ exitWith (ExitFailure 1)

174− Right ist ->

204+ Right ist -> do

175− do docRes <- generateDocs ist mods outputDir

205+ docRes <- generateDocs ist mods outputDir

176− case docRes of

206+ case docRes of

177− Right _ -> return ()

207+ Right _ -> return ()

208+ Left msg -> do

178− Left msg -> do putStrLn msg

209+ putStrLn msg

179− exitWith (ExitFailure 1)

210+ exitWith (ExitFailure 1)

180

211

181-- ------------------------------------------------------------------- [ Test ]

212-- ------------------------------------------------------------------- [ Test ]

182

213

@@ -184,36 +215,41 @@ documentPkg copts fp =

184testPkg :: [Opt] -- ^ Command line options.

215testPkg :: [Opt] -- ^ Command line options.

185 -> FilePath -- ^ Path to ipkg file.

216 -> FilePath -- ^ Path to ipkg file.

186 -> IO ()

217 -> IO ()

187−testPkg copts fp

218+testPkg copts fp = do

188− = do pkgdesc <- parseDesc fp

219+ pkgdesc <- parseDesc fp

189− ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc)

220+ ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc)

190− when (and ok) $

221+ when (and ok) $ do

191− do m_ist <- inPkgDir pkgdesc $

222+ m_ist <- inPkgDir pkgdesc $ do

192− do make (makefile pkgdesc)

223+ make (makefile pkgdesc)

193− -- Get a temporary file to save the tests' source in

224+ -- Get a temporary file to save the tests' source in

194− (tmpn, tmph) <- tempfile ".idr"

225+ (tmpn, tmph) <- tempfile ".idr"

195− hPutStrLn tmph $

226+ hPutStrLn tmph $

196− "module Test_______\n" ++

227+ "module Test_______\n" ++

197− concat ["import " ++ show m ++ "\n"

228+ concat ["import " ++ show m ++ "\n" | m <- modules pkgdesc]

198− | m <- modules pkgdesc] ++

199− "namespace Main\n" ++

229+ ++ "namespace Main\n"

200− " main : IO ()\n" ++

230+ ++ " main : IO ()\n"

201− " main = do " ++

231+ ++ " main = do "

202− concat [show t ++ "\n "

232+ ++ concat [ show t ++ "\n "

203− | t <- idris_tests pkgdesc]

233+ | t <- idris_tests pkgdesc]

204− hClose tmph

234+ hClose tmph

205− (tmpn', tmph') <- tempfile ""

235+ (tmpn', tmph') <- tempfile ""

206− hClose tmph'

236+ hClose tmph'

207− 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

208− rawSystem tmpn' []

244+ rawSystem tmpn' []

209− return m_ist

245+ return m_ist

210− case m_ist of

246+ case m_ist of

211− Nothing -> exitWith (ExitFailure 1)

247+ Nothing -> exitWith (ExitFailure 1)

212− Just ist -> do

248+ Just ist -> do

213− -- Quit with error code if problem building

249+ -- Quit with error code if problem building

214− case errSpan ist of

250+ case errSpan ist of

215− Just _ -> exitWith (ExitFailure 1)

251+ Just _ -> exitWith (ExitFailure 1)

216− _ -> return ()

252+ _ -> return ()

217

253

218-- ----------------------------------------------------------- [ Installation ]

254-- ----------------------------------------------------------- [ Installation ]

219

255

@@ -328,4 +364,59 @@ clean Nothing = return ()

328clean (Just s) = do rawSystem "make" ["-f", s, "clean"]

364clean (Just s) = do rawSystem "make" ["-f", s, "clean"]

329 return ()

365 return ()

330

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+

331-- --------------------------------------------------------------------- [ EOF ]

422-- --------------------------------------------------------------------- [ EOF ]

test/pkg001/expected+19

@@ -0,0 +1,19 @@

1+Not all command line options can be used to override package options.

3+The only changeable options are:

4+ --log <lvl>, --total, --warnpartial, --warnreach

5+ --ibcsubdir <path>, -i --idrispath <path>

6+ --logging-categories <cats>

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

2${IDRIS:-idris} $@ --build test.ipkg

3rm -f *.ibc

4+${IDRIS:-idris} $@ --build test.ipkg --quiet

5+${IDRIS:-idris} $@ --build test.ipkg --logging-categories "elab" --log 1