git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/src/Idris/Package.hs
512 lines 18 kB history raw
1{-|
2Module : Idris.Package
3Description : Functionality for working with Idris packages.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE CPP #-}
9module Idris.Package where
11import System.Directory
12import System.Directory (copyFile, createDirectoryIfMissing)
13import System.Exit
14import System.FilePath (addExtension, addTrailingPathSeparator, dropExtension,
15 hasExtension, takeDirectory, takeExtension,
16 takeFileName, (</>))
17import System.IO
18import System.Process
20import Util.System
22import Control.Monad
23import Control.Monad.Trans.Except (runExceptT)
24import Control.Monad.Trans.State.Strict (execStateT)
25import Data.Either (partitionEithers)
26import Data.List
27import Data.List.Split (splitOn)
29import Idris.AbsSyntax
30import Idris.Core.TT
31import Idris.Error (ifail)
32import Idris.IBC
33import Idris.IdrisDoc
34import Idris.Imports
35import Idris.Main (idris, idrisMain)
36import Idris.Options
37import Idris.Output
38import Idris.Parser (loadModule)
40import Idris.Package.Common
41import Idris.Package.Parser
43import IRTS.System
45-- To build a package:
46-- * read the package description
47-- * check all the library dependencies exist
48-- * invoke the makefile if there is one
49-- * invoke idris on each module, with idris_opts
50-- * install everything into datadir/pname, if install flag is set
52getPkgDesc :: FilePath -> IO PkgDesc
53getPkgDesc = parseDesc
55-- --------------------------------------------------------- [ Build Packages ]
57-- | Run the package through the idris compiler.
58buildPkg :: [Opt] -- ^ Command line options
59 -> Bool -- ^ Provide Warnings
60 -> (Bool, FilePath) -- ^ (Should we install, Location of iPKG file)
61 -> IO ()
62buildPkg copts warnonly (install, fp) = do
63 pkgdesc <- parseDesc fp
64 dir <- getCurrentDirectory
65 let idx' = pkgIndex $ pkgname pkgdesc
66 idx = PkgIndex $ case opt getIBCSubDir copts of
67 (ibcsubdir:_) -> ibcsubdir </> idx'
68 [] -> idx'
69 oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
70 when (and oks) $ do
71 m_ist <- inPkgDir pkgdesc $ do
73 make (makefile pkgdesc)
74 case (execout pkgdesc) of
75 Nothing -> do
76 case mergeOptions copts (idx : NoREPL : Verbose 1 : idris_opts pkgdesc) of
77 Left emsg -> do
78 putStrLn emsg
79 exitWith (ExitFailure 1)
80 Right opts -> do
81 auditPackage (AuditIPkg `elem` opts) pkgdesc
82 buildMods opts (modules pkgdesc)
83 Just o -> do
84 let exec = dir </> o
85 case mergeOptions copts (idx : NoREPL : Verbose 1 : Output exec : idris_opts pkgdesc) of
86 Left emsg -> do
87 putStrLn emsg
88 exitWith (ExitFailure 1)
89 Right opts -> do
90 auditPackage (AuditIPkg `elem` opts) pkgdesc
91 buildMain opts (idris_main pkgdesc)
92 case m_ist of
93 Nothing -> exitWith (ExitFailure 1)
94 Just ist -> do
95 -- Quit with error code if there was a problem
96 case errSpan ist of
97 Just _ -> exitWith (ExitFailure 1)
98 _ -> return ()
99 when install $ installPkg (opt getIBCSubDir copts) pkgdesc
100 where
101 buildMain opts (Just mod) = buildMods opts [mod]
102 buildMain _ Nothing = do
103 putStrLn "Can't build an executable: No main module given"
104 exitWith (ExitFailure 1)
106-- --------------------------------------------------------- [ Check Packages ]
108-- | Type check packages only
109--
110-- This differs from build in that executables are not built, if the
111-- package contains an executable.
112checkPkg :: [Opt] -- ^ Command line Options
113 -> Bool -- ^ Show Warnings
114 -> Bool -- ^ quit on failure
115 -> FilePath -- ^ Path to ipkg file.
116 -> IO ()
117checkPkg copts warnonly quit fpath = do
118 pkgdesc <- parseDesc fpath
119 oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
120 when (and oks) $ do
121 res <- inPkgDir pkgdesc $ do
122 make (makefile pkgdesc)
124 case mergeOptions copts (NoREPL : Verbose 1 : idris_opts pkgdesc) of
125 Left emsg -> do
126 putStrLn emsg
127 exitWith (ExitFailure 1)
128 Right opts -> do
129 auditPackage (AuditIPkg `elem` opts) pkgdesc
130 buildMods opts (modules pkgdesc)
131 when quit $ case res of
132 Nothing -> exitWith (ExitFailure 1)
133 Just res' -> do
134 case errSpan res' of
135 Just _ -> exitWith (ExitFailure 1)
136 _ -> return ()
138-- ------------------------------------------------------------------- [ REPL ]
140-- | Check a package and start a REPL.
141--
142-- This function only works with packages that have a main module.
143--
144replPkg :: [Opt] -- ^ Command line Options
145 -> FilePath -- ^ Path to ipkg file.
146 -> Idris ()
147replPkg copts fp = do
148 orig <- getIState
149 runIO $ checkPkg copts False False fp
150 pkgdesc <- runIO $ parseDesc fp -- bzzt, repetition!
152 case mergeOptions copts (idris_opts pkgdesc) of
153 Left emsg -> ifail emsg
154 Right opts -> do
156 putIState orig
157 dir <- runIO getCurrentDirectory
158 runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc
159 runMain opts (idris_main pkgdesc)
160 runIO $ setCurrentDirectory dir
162 where
163 toPath n = foldl1' (</>) $ splitOn "." n
165 runMain opts (Just mod) = do
166 let f = toPath (showCG mod)
167 idrisMain ((Filename f) : opts)
168 runMain _ Nothing =
169 iputStrLn "Can't start REPL: no main module given"
171-- --------------------------------------------------------------- [ Cleaning ]
173-- | Clean Package build files
174cleanPkg :: [Opt] -- ^ Command line options.
175 -> FilePath -- ^ Path to ipkg file.
176 -> IO ()
177cleanPkg copts fp = do
178 pkgdesc <- parseDesc fp
179 dir <- getCurrentDirectory
180 inPkgDir pkgdesc $ do
181 clean (makefile pkgdesc)
182 mapM_ rmIBC (modules pkgdesc)
183 rmIdx (pkgname pkgdesc)
184 case execout pkgdesc of
185 Nothing -> return ()
186 Just s -> rmExe $ dir </> s
188-- ------------------------------------------------------ [ Generate IdrisDoc ]
191-- | Generate IdrisDoc for package
192-- TODO: Handle case where module does not contain a matching namespace
193-- E.g. from prelude.ipkg: IO, Prelude.Chars, Builtins
194--
195-- Issue number #1572 on the issue tracker
196-- https://github.com/idris-lang/Idris-dev/issues/1572
197documentPkg :: [Opt] -- ^ Command line options.
198 -> (Bool,FilePath) -- ^ (Should we install?, Path to ipkg file).
199 -> IO ()
200documentPkg copts (install,fp) = do
201 pkgdesc <- parseDesc fp
202 cd <- getCurrentDirectory
203 let pkgDir = cd </> takeDirectory fp
204 outputDir = cd </> unPkgName (pkgname pkgdesc) ++ "_doc"
205 popts = NoREPL : Verbose 1 : idris_opts pkgdesc
206 mods = modules pkgdesc
207 fs = map (foldl1' (</>) . splitOn "." . showCG) mods
208 setCurrentDirectory $ pkgDir </> sourcedir pkgdesc
209 make (makefile pkgdesc)
210 setCurrentDirectory pkgDir
211 case mergeOptions copts popts of
212 Left emsg -> do
213 putStrLn emsg
214 exitWith (ExitFailure 1)
215 Right opts -> do
216 let run l = runExceptT . execStateT l
217 load [] = return ()
218 load (f:fs) = do loadModule f IBC_Building; load fs
219 loader = do
220 idrisMain opts
221 addImportDir (sourcedir pkgdesc)
222 load fs
223 idrisImplementation <- run loader idrisInit
224 setCurrentDirectory cd
225 case idrisImplementation of
226 Left err -> do
227 putStrLn $ pshow idrisInit err
228 exitWith (ExitFailure 1)
229 Right ist -> do
230 iDocDir <- getIdrisDocDir
231 pkgDocDir <- makeAbsolute (iDocDir </> unPkgName (pkgname pkgdesc))
232 let out_dir = if install then pkgDocDir else outputDir
233 when install $ do
234 putStrLn $ unwords ["Attempting to install IdrisDocs for", show $ pkgname pkgdesc, "in:", out_dir]
236 docRes <- generateDocs ist mods out_dir
237 case docRes of
238 Right _ -> return ()
239 Left msg -> do
240 putStrLn msg
241 exitWith (ExitFailure 1)
243-- ------------------------------------------------------------------- [ Test ]
245-- | Build a package with a sythesized main function that runs the tests
246testPkg :: [Opt] -- ^ Command line options.
247 -> FilePath -- ^ Path to ipkg file.
248 -> IO ExitCode
249testPkg copts fp = do
250 pkgdesc <- parseDesc fp
251 ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc)
252 if and ok
253 then do
254 (m_ist, exitCode) <- inPkgDir pkgdesc $ do
255 make (makefile pkgdesc)
256 -- Get a temporary file to save the tests' source in
257 (tmpn, tmph) <- tempfile ".idr"
258 hPutStrLn tmph $
259 "module Test_______\n" ++
260 concat ["import " ++ show m ++ "\n" | m <- modules pkgdesc]
261 ++ "namespace Main\n"
262 ++ " main : IO ()\n"
263 ++ " main = do "
264 ++ concat [ show t ++ "\n "
265 | t <- idris_tests pkgdesc]
266 hClose tmph
267 (tmpn', tmph') <- tempfile ""
268 hClose tmph'
269 let popts = (Filename tmpn : NoREPL : Verbose 1 : Output tmpn' : idris_opts pkgdesc)
270 case mergeOptions copts popts of
271 Left emsg -> do
272 putStrLn emsg
273 exitWith (ExitFailure 1)
274 Right opts -> do
275 m_ist <- idris opts
276 let texe = if isWindows then addExtension tmpn' ".exe" else tmpn'
277 exitCode <- rawSystem texe []
278 return (m_ist, exitCode)
279 case m_ist of
280 Nothing -> exitWith (ExitFailure 1)
281 Just ist -> do
282 -- Quit with error code if problem building
283 case errSpan ist of
284 Just _ -> exitWith (ExitFailure 1)
285 _ -> return exitCode
286 else return (ExitFailure 1)
288-- ----------------------------------------------------------- [ Installation ]
290-- | Install package
291installPkg :: [String] -- ^ Alternate install location
292 -> PkgDesc -- ^ iPKG file.
293 -> IO ()
294installPkg altdests pkgdesc = inPkgDir pkgdesc $ do
295 d <- getIdrisLibDir
296 let destdir = case altdests of
297 [] -> d
298 (d':_) -> d'
299 case (execout pkgdesc) of
300 Nothing -> do
301 mapM_ (installIBC destdir (pkgname pkgdesc)) (modules pkgdesc)
302 installIdx destdir (pkgname pkgdesc)
303 Just o -> return () -- do nothing, keep executable locally, for noe
305 mapM_ (installObj destdir (pkgname pkgdesc)) (objs pkgdesc)
307-- ---------------------------------------------------------- [ Helper Methods ]
308-- Methods for building, testing, installing, and removal of idris
309-- packages.
311auditPackage :: Bool -> PkgDesc -> IO ()
312auditPackage False _ = return ()
313auditPackage True ipkg = do
314 cwd <- getCurrentDirectory
316 let ms = map (sourcedir ipkg </>) $ map (toPath . showCG) (modules ipkg)
317 ms' <- mapM makeAbsolute ms
319 ifiles <- getIdrisFiles cwd
321 let ifiles' = map dropExtension ifiles
323 not_listed <- mapM makeRelativeToCurrentDirectory (ifiles' \\ ms')
325 putStrLn $ unlines $
326 ["Warning: The following modules are not listed in your iPkg file:\n"]
327 ++ map (\m -> unwords ["-", m]) not_listed
328 ++ ["\nModules that are not listed, are not installed."]
330 where
331 toPath n = foldl1' (</>) $ splitOn "." n
333 getIdrisFiles :: FilePath -> IO [FilePath]
334 getIdrisFiles dir = do
335 contents <- getDirectoryContents dir
337 -- [ NOTE ] Directory >= 1.2.5.0 introduced `listDirectory` but later versions of directory appear to be causing problems with ghc 7.10.3 and cabal 1.22 in travis. Let's reintroduce the old ranges for directory to be sure.
339 files <- forM contents (findRest dir)
340 return $ filter (isIdrisFile) (concat files)
342 isIdrisFile :: FilePath -> Bool
343 isIdrisFile fp = takeExtension fp == ".idr" || takeExtension fp == ".lidr"
345 findRest :: FilePath -> FilePath -> IO [FilePath]
346 findRest dir fn = do
347 path <- makeAbsolute (dir </> fn)
348 isDir <- doesDirectoryExist path
349 if isDir
350 then getIdrisFiles path
351 else return [path]
353buildMods :: [Opt] -> [Name] -> IO (Maybe IState)
354buildMods opts ns = do let f = map (toPath . showCG) ns
355 idris (map Filename f ++ opts)
356 where
357 toPath n = foldl1' (</>) $ splitOn "." n
359testLib :: Bool -> PkgName -> String -> IO Bool
360testLib warn p f
361 = do d <- getIdrisCRTSDir
362 gcc <- getCC
363 (tmpf, tmph) <- tempfile ""
364 hClose tmph
365 let libtest = d </> "libtest.c"
366 e <- rawSystem gcc [libtest, "-l" ++ f, "-o", tmpf]
367 case e of
368 ExitSuccess -> return True
369 _ -> do if warn
370 then do putStrLn $ "Not building " ++ show p ++
371 " due to missing library " ++ f
372 return False
373 else fail $ "Missing library " ++ f
375rmIBC :: Name -> IO ()
376rmIBC m = rmFile $ toIBCFile m
378rmIdx :: PkgName -> IO ()
379rmIdx p = do let f = pkgIndex p
380 ex <- doesFileExist f
381 when ex $ rmFile f
383rmExe :: String -> IO ()
384rmExe p = do
385 fn <- return $ if isWindows && not (hasExtension p)
386 then addExtension p ".exe" else p
387 rmFile fn
389toIBCFile (UN n) = str n ++ ".ibc"
390toIBCFile (NS n ns) = foldl1' (</>) (reverse (toIBCFile n : map str ns))
392installIBC :: String -> PkgName -> Name -> IO ()
393installIBC dest p m = do
394 let f = toIBCFile m
395 let destdir = dest </> unPkgName p </> getDest m
396 putStrLn $ "Installing " ++ f ++ " to " ++ destdir
397 createDirectoryIfMissing True destdir
398 copyFile f (destdir </> takeFileName f)
399 return ()
400 where
401 getDest (UN n) = ""
402 getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : map str ns))
404installIdx :: String -> PkgName -> IO ()
405installIdx dest p = do
406 let f = pkgIndex p
407 let destdir = dest </> unPkgName p
408 putStrLn $ "Installing " ++ f ++ " to " ++ destdir
409 createDirectoryIfMissing True destdir
410 copyFile f (destdir </> takeFileName f)
411 return ()
413installObj :: String -> PkgName -> String -> IO ()
414installObj dest p o = do
415 let destdir = addTrailingPathSeparator (dest </> unPkgName p)
416 putStrLn $ "Installing " ++ o ++ " to " ++ destdir
417 createDirectoryIfMissing True destdir
418 copyFile o (destdir </> takeFileName o)
419 return ()
421#ifdef mingw32_HOST_OS
422mkDirCmd = "mkdir "
423#else
424mkDirCmd = "mkdir -p "
425#endif
427inPkgDir :: PkgDesc -> IO a -> IO a
428inPkgDir pkgdesc action =
429 do dir <- getCurrentDirectory
430 when (sourcedir pkgdesc /= "") $
431 do putStrLn $ "Entering directory `" ++ ("." </> sourcedir pkgdesc) ++ "'"
432 setCurrentDirectory $ dir </> sourcedir pkgdesc
433 res <- action
434 when (sourcedir pkgdesc /= "") $
435 do putStrLn $ "Leaving directory `" ++ ("." </> sourcedir pkgdesc) ++ "'"
436 setCurrentDirectory dir
437 return res
439-- ------------------------------------------------------- [ Makefile Commands ]
440-- | Invoke a Makefile's default target.
441make :: Maybe String -> IO ()
442make Nothing = return ()
443make (Just s) = do rawSystem "make" ["-f", s]
444 return ()
446-- | Invoke a Makefile's clean target.
447clean :: Maybe String -> IO ()
448clean Nothing = return ()
449clean (Just s) = do rawSystem "make" ["-f", s, "clean"]
450 return ()
452-- | Merge an option list representing the command line options into
453-- those specified for a package description.
454--
455-- This is not a complete union between the two options sets. First,
456-- to prevent important package specified options from being
457-- overwritten. Second, the semantics for this merge are not fully
458-- defined.
459--
460-- A discussion for this is on the issue tracker:
461-- https://github.com/idris-lang/Idris-dev/issues/1448
462--
463mergeOptions :: [Opt] -- ^ The command line options
464 -> [Opt] -- ^ The package options
465 -> Either String [Opt]
466mergeOptions copts popts =
467 case partitionEithers (map chkOpt (normaliseOpts copts)) of
468 ([], copts') -> Right $ copts' ++ popts
469 (es, _) -> Left $ genErrMsg es
470 where
471 normaliseOpts :: [Opt] -> [Opt]
472 normaliseOpts = filter filtOpt
474 filtOpt :: Opt -> Bool
475 filtOpt (PkgBuild _) = False
476 filtOpt (PkgInstall _) = False
477 filtOpt (PkgClean _) = False
478 filtOpt (PkgCheck _) = False
479 filtOpt (PkgREPL _) = False
480 filtOpt (PkgDocBuild _) = False
481 filtOpt (PkgDocInstall _) = False
482 filtOpt (PkgTest _) = False
483 filtOpt _ = True
485 chkOpt :: Opt -> Either String Opt
486 chkOpt o@(OLogging _) = Right o
487 chkOpt o@(OLogCats _) = Right o
488 chkOpt o@(DefaultTotal) = Right o
489 chkOpt o@(DefaultPartial) = Right o
490 chkOpt o@(WarnPartial) = Right o
491 chkOpt o@(WarnReach) = Right o
492 chkOpt o@(IBCSubDir _) = Right o
493 chkOpt o@(ImportDir _ ) = Right o
494 chkOpt o@(UseCodegen _) = Right o
495 chkOpt o@(Verbose _) = Right o
496 chkOpt o@(AuditIPkg) = Right o
497 chkOpt o@(DumpHighlights) = Right o
498 chkOpt o = Left (unwords ["\t", show o, "\n"])
500 genErrMsg :: [String] -> String
501 genErrMsg es = unlines
502 [ "Not all command line options can be used to override package options."
503 , "\nThe only changeable options are:"
504 , "\t--log <lvl>, --total, --warnpartial, --warnreach, --warnipkg"
505 , "\t--ibcsubdir <path>, -i --idrispath <path>"
506 , "\t--logging-categories <cats>"
507 , "\t--highlight"
508 , "\nThe options need removing are:"
509 , unlines es
510 ]
512-- --------------------------------------------------------------------- [ EOF ]