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