git.iko.soy/Idris-dev
on 54e4e41 help sign in
Idris-dev/src/Pkg/Package.hs
298 lines 12 kB history raw
1{-# LANGUAGE CPP #-}
2module Pkg.Package where
4import System.Process
5import System.Directory
6import System.Exit
7import System.IO
8import System.FilePath ((</>), addTrailingPathSeparator, takeFileName, takeDirectory, normalise)
9import System.Directory (createDirectoryIfMissing, copyFile)
11import Util.System
13import Control.Monad
14import Control.Monad.Trans.State.Strict (execStateT)
15import Control.Monad.Trans.Except (runExceptT)
17import Data.List
18import Data.List.Split(splitOn)
20import Idris.Core.TT
21import Idris.REPL
22import Idris.Parser (loadModule)
23import Idris.Output (pshow)
24import Idris.AbsSyntax
25import Idris.IdrisDoc
26import Idris.IBC
27import Idris.Output
28import Idris.Imports
30import Pkg.PParser
32import IRTS.System
34-- To build a package:
35-- * read the package description
36-- * check all the library dependencies exist
37-- * invoke the makefile if there is one
38-- * invoke idris on each module, with idris_opts
39-- * install everything into datadir/pname, if install flag is set
41-- | Run the package through the idris compiler.
42buildPkg :: Bool -> (Bool, FilePath) -> IO ()
43buildPkg warnonly (install, fp)
44 = do pkgdesc <- parseDesc fp
45 dir <- getCurrentDirectory
46 let idx = PkgIndex (pkgIndex (pkgname pkgdesc))
47 ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
48 when (and ok) $
49 do m_ist <- inPkgDir pkgdesc $
50 do make (makefile pkgdesc)
51 case (execout pkgdesc) of
52 Nothing -> buildMods (idx : NoREPL : Verbose : idris_opts pkgdesc)
53 (modules pkgdesc)
54 Just o -> do let exec = dir </> o
55 buildMods
56 (idx : NoREPL : Verbose : Output exec : idris_opts pkgdesc)
57 [idris_main pkgdesc]
58 case m_ist of
59 Nothing -> exitWith (ExitFailure 1)
60 Just ist -> do
61 -- Quit with error code if there was a problem
62 case errSpan ist of
63 Just _ -> exitWith (ExitFailure 1)
64 _ -> return ()
65 when install $ installPkg pkgdesc
67-- | Type check packages only
68--
69-- This differs from build in that executables are not built, if the
70-- package contains an executable.
71checkPkg :: Bool -- ^ Show Warnings
72 -> Bool -- ^ quit on failure
73 -> FilePath -- ^ Path to ipkg file.
74 -> IO ()
75checkPkg warnonly quit fpath
76 = do pkgdesc <- parseDesc fpath
77 ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
78 when (and ok) $
79 do res <- inPkgDir pkgdesc $
80 do make (makefile pkgdesc)
81 buildMods (NoREPL : Verbose : idris_opts pkgdesc)
82 (modules pkgdesc)
83 when quit $ case res of
84 Nothing -> exitWith (ExitFailure 1)
85 Just res' -> do
86 case errSpan res' of
87 Just _ -> exitWith (ExitFailure 1)
88 _ -> return ()
90-- | Check a package and start a REPL
91replPkg :: FilePath -> Idris ()
92replPkg fp = do orig <- getIState
93 runIO $ checkPkg False False fp
94 pkgdesc <- runIO $ parseDesc fp -- bzzt, repetition!
95 let opts = idris_opts pkgdesc
96 let mod = idris_main pkgdesc
97 let f = toPath (showCG mod)
98 putIState orig
99 dir <- runIO $ getCurrentDirectory
100 runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc
102 if (f /= "")
103 then idrisMain ((Filename f) : opts)
104 else iputStrLn "Can't start REPL: no main module given"
105 runIO $ setCurrentDirectory dir
107 where toPath n = foldl1' (</>) $ splitOn "." n
109-- | Clean Package build files
110cleanPkg :: FilePath -- ^ Path to ipkg file.
111 -> IO ()
112cleanPkg fp
113 = do pkgdesc <- parseDesc fp
114 dir <- getCurrentDirectory
115 inPkgDir pkgdesc $
116 do clean (makefile pkgdesc)
117 mapM_ rmIBC (modules pkgdesc)
118 rmIdx (pkgname pkgdesc)
119 case execout pkgdesc of
120 Nothing -> return ()
121 Just s -> rmFile $ dir </> s
123-- | Generate IdrisDoc for package
124-- TODO: Handle case where module does not contain a matching namespace
125-- E.g. from prelude.ipkg: IO, Prelude.Chars, Builtins
126--
127-- Issue number #1572 on the issue tracker
128-- https://github.com/idris-lang/Idris-dev/issues/1572
129documentPkg :: FilePath -- ^ Path to .ipkg file.
130 -> IO ()
131documentPkg fp =
132 do pkgdesc <- parseDesc fp
133 cd <- getCurrentDirectory
134 let pkgDir = cd </> takeDirectory fp
135 outputDir = cd </> (pkgname pkgdesc) ++ "_doc"
136 opts = NoREPL : Verbose : idris_opts pkgdesc
137 mods = modules pkgdesc
138 fs = map (foldl1' (</>) . splitOn "." . showCG) mods
139 setCurrentDirectory $ pkgDir </> sourcedir pkgdesc
140 make (makefile pkgdesc)
141 setCurrentDirectory $ pkgDir
142 let run l = runExceptT . execStateT l
143 load [] = return ()
144 load (f:fs) = do loadModule f; load fs
145 loader = do idrisMain opts; load fs
146 idrisInstance <- run loader idrisInit
147 setCurrentDirectory cd
148 case idrisInstance of
149 Left err -> do putStrLn $ pshow idrisInit err; exitWith (ExitFailure 1)
150 Right ist ->
151 do docRes <- generateDocs ist mods outputDir
152 case docRes of
153 Right _ -> return ()
154 Left msg -> do putStrLn msg
155 exitWith (ExitFailure 1)
157-- | Build a package with a sythesized main function that runs the tests
158testPkg :: FilePath -> IO ()
159testPkg fp
160 = do pkgdesc <- parseDesc fp
161 ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc)
162 when (and ok) $
163 do m_ist <- inPkgDir pkgdesc $
164 do make (makefile pkgdesc)
165 -- Get a temporary file to save the tests' source in
166 (tmpn, tmph) <- tempIdr
167 hPutStrLn tmph $
168 "module Test_______\n" ++
169 concat ["import " ++ show m ++ "\n"
170 | m <- modules pkgdesc] ++
171 "namespace Main\n" ++
172 " main : IO ()\n" ++
173 " main = do " ++
174 concat [show t ++ "\n "
175 | t <- idris_tests pkgdesc]
176 hClose tmph
177 (tmpn', tmph') <- tempfile
178 hClose tmph'
179 m_ist <- idris (Filename tmpn : NoREPL : Verbose : Output tmpn' : idris_opts pkgdesc)
180 rawSystem tmpn' []
181 return m_ist
182 case m_ist of
183 Nothing -> exitWith (ExitFailure 1)
184 Just ist -> do
185 -- Quit with error code if problem building
186 case errSpan ist of
187 Just _ -> exitWith (ExitFailure 1)
188 _ -> return ()
189 where tempIdr :: IO (FilePath, Handle)
190 tempIdr = do dir <- getTemporaryDirectory
191 openTempFile (normalise dir) "idristests.idr"
193-- | Install package
194installPkg :: PkgDesc -> IO ()
195installPkg pkgdesc
196 = inPkgDir pkgdesc $
197 do case (execout pkgdesc) of
198 Nothing -> do mapM_ (installIBC (pkgname pkgdesc)) (modules pkgdesc)
199 installIdx (pkgname pkgdesc)
200 Just o -> return () -- do nothing, keep executable locally, for noe
201 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)
203-- ---------------------------------------------------------- [ Helper Methods ]
204-- Methods for building, testing, installing, and removal of idris
205-- packages.
207buildMods :: [Opt] -> [Name] -> IO (Maybe IState)
208buildMods opts ns = do let f = map (toPath . showCG) ns
209 idris (map Filename f ++ opts)
210 where toPath n = foldl1' (</>) $ splitOn "." n
212testLib :: Bool -> String -> String -> IO Bool
213testLib warn p f
214 = do d <- getDataDir
215 gcc <- getCC
216 (tmpf, tmph) <- tempfile
217 hClose tmph
218 let libtest = d </> "rts" </> "libtest.c"
219 e <- rawSystem gcc [libtest, "-l" ++ f, "-o", tmpf]
220 case e of
221 ExitSuccess -> return True
222 _ -> do if warn
223 then do putStrLn $ "Not building " ++ p ++
224 " due to missing library " ++ f
225 return False
226 else fail $ "Missing library " ++ f
228rmIBC :: Name -> IO ()
229rmIBC m = rmFile $ toIBCFile m
231rmIdx :: String -> IO ()
232rmIdx p = do let f = pkgIndex p
233 ex <- doesFileExist f
234 when ex $ rmFile f
236toIBCFile (UN n) = str n ++ ".ibc"
237toIBCFile (NS n ns) = foldl1' (</>) (reverse (toIBCFile n : map str ns))
239installIBC :: String -> Name -> IO ()
240installIBC p m = do let f = toIBCFile m
241 d <- getTargetDir
242 let destdir = d </> p </> getDest m
243 putStrLn $ "Installing " ++ f ++ " to " ++ destdir
244 createDirectoryIfMissing True destdir
245 copyFile f (destdir </> takeFileName f)
246 return ()
247 where getDest (UN n) = ""
248 getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : map str ns))
250installIdx :: String -> IO ()
251installIdx p = do d <- getTargetDir
252 let f = pkgIndex p
253 let destdir = d </> p
254 putStrLn $ "Installing " ++ f ++ " to " ++ destdir
255 createDirectoryIfMissing True destdir
256 copyFile f (destdir </> takeFileName f)
257 return ()
259installObj :: String -> String -> IO ()
260installObj p o = do d <- getTargetDir
261 let destdir = addTrailingPathSeparator (d </> p)
262 putStrLn $ "Installing " ++ o ++ " to " ++ destdir
263 createDirectoryIfMissing True destdir
264 copyFile o (destdir </> takeFileName o)
265 return ()
267#ifdef mingw32_HOST_OS
268mkDirCmd = "mkdir "
269#else
270mkDirCmd = "mkdir -p "
271#endif
273inPkgDir :: PkgDesc -> IO a -> IO a
274inPkgDir pkgdesc action =
275 do dir <- getCurrentDirectory
276 when (sourcedir pkgdesc /= "") $
277 do putStrLn $ "Entering directory `" ++ ("." </> sourcedir pkgdesc) ++ "'"
278 setCurrentDirectory $ dir </> sourcedir pkgdesc
279 res <- action
280 when (sourcedir pkgdesc /= "") $
281 do putStrLn $ "Leaving directory `" ++ ("." </> sourcedir pkgdesc) ++ "'"
282 setCurrentDirectory dir
283 return res
285-- ------------------------------------------------------- [ Makefile Commands ]
286-- | Invoke a Makefile's default target.
287make :: Maybe String -> IO ()
288make Nothing = return ()
289make (Just s) = do rawSystem "make" ["-f", s]
290 return ()
292-- | Invoke a Makefile's clean target.
293clean :: Maybe String -> IO ()
294clean Nothing = return ()
295clean (Just s) = do rawSystem "make" ["-f", s, "clean"]
296 return ()
298-- --------------------------------------------------------------------- [ EOF ]