git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Pkg/Package.hs
291 lines 11 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 let idx = PkgIndex (pkgIndex (pkgname pkgdesc))
46 ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
47 when (and ok) $
48 do dir <- getCurrentDirectory
49 setCurrentDirectory $ dir </> sourcedir pkgdesc
50 make (makefile pkgdesc)
51 m_ist <- 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 setCurrentDirectory dir
59 case m_ist of
60 Nothing -> exitWith (ExitFailure 1)
61 Just ist -> do
62 -- Quit with error code if there was a problem
63 case errSpan ist of
64 Just _ -> exitWith (ExitFailure 1)
65 _ -> return ()
66 when install $ installPkg pkgdesc
68-- | Type check packages only
69--
70-- This differs from build in that executables are not built, if the
71-- package contains an executable.
72checkPkg :: Bool -- ^ Show Warnings
73 -> Bool -- ^ quit on failure
74 -> FilePath -- ^ Path to ipkg file.
75 -> IO ()
76checkPkg warnonly quit fpath
77 = do pkgdesc <- parseDesc fpath
78 ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
79 when (and ok) $
80 do dir <- getCurrentDirectory
81 setCurrentDirectory $ dir </> sourcedir pkgdesc
82 make (makefile pkgdesc)
83 res <- buildMods (NoREPL : Verbose : idris_opts pkgdesc)
84 (modules pkgdesc)
85 setCurrentDirectory dir
86 when quit $ case res of
87 Nothing -> exitWith (ExitFailure 1)
88 Just res' -> do
89 case errSpan res' of
90 Just _ -> exitWith (ExitFailure 1)
91 _ -> return ()
93-- | Check a package and start a REPL
94replPkg :: FilePath -> Idris ()
95replPkg fp = do orig <- getIState
96 runIO $ checkPkg False False fp
97 pkgdesc <- runIO $ parseDesc fp -- bzzt, repetition!
98 let opts = idris_opts pkgdesc
99 let mod = idris_main pkgdesc
100 let f = toPath (showCG mod)
101 putIState orig
102 dir <- runIO $ getCurrentDirectory
103 runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc
105 if (f /= "")
106 then idrisMain ((Filename f) : opts)
107 else iputStrLn "Can't start REPL: no main module given"
108 runIO $ setCurrentDirectory dir
110 where toPath n = foldl1' (</>) $ splitOn "." n
112-- | Clean Package build files
113cleanPkg :: FilePath -- ^ Path to ipkg file.
114 -> IO ()
115cleanPkg fp
116 = do pkgdesc <- parseDesc fp
117 dir <- getCurrentDirectory
118 setCurrentDirectory $ dir </> sourcedir pkgdesc
119 clean (makefile pkgdesc)
120 mapM_ rmIBC (modules pkgdesc)
121 rmIdx (pkgname pkgdesc)
122 case execout pkgdesc of
123 Nothing -> return ()
124 Just s -> rmFile $ dir </> s
126-- | Generate IdrisDoc for package
127-- TODO: Handle case where module does not contain a matching namespace
128-- E.g. from prelude.ipkg: IO, Prelude.Chars, Builtins
129--
130-- Issue number #1572 on the issue tracker
131-- https://github.com/idris-lang/Idris-dev/issues/1572
132documentPkg :: FilePath -- ^ Path to .ipkg file.
133 -> IO ()
134documentPkg fp =
135 do pkgdesc <- parseDesc fp
136 cd <- getCurrentDirectory
137 let pkgDir = cd </> takeDirectory fp
138 outputDir = cd </> (pkgname pkgdesc) ++ "_doc"
139 opts = NoREPL : Verbose : idris_opts pkgdesc
140 mods = modules pkgdesc
141 fs = map (foldl1' (</>) . splitOn "." . showCG) mods
142 setCurrentDirectory $ pkgDir </> sourcedir pkgdesc
143 make (makefile pkgdesc)
144 setCurrentDirectory $ pkgDir
145 let run l = runExceptT . execStateT l
146 load [] = return ()
147 load (f:fs) = do loadModule f; load fs
148 loader = do idrisMain opts; load fs
149 idrisInstance <- run loader idrisInit
150 setCurrentDirectory cd
151 case idrisInstance of
152 Left err -> do putStrLn $ pshow idrisInit err; exitWith (ExitFailure 1)
153 Right ist ->
154 do docRes <- generateDocs ist mods outputDir
155 case docRes of
156 Right _ -> return ()
157 Left msg -> do putStrLn msg
158 exitWith (ExitFailure 1)
160-- | Build a package with a sythesized main function that runs the tests
161testPkg :: FilePath -> IO ()
162testPkg fp
163 = do pkgdesc <- parseDesc fp
164 ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc)
165 when (and ok) $
166 do dir <- getCurrentDirectory
167 setCurrentDirectory $ dir </> sourcedir pkgdesc
168 make (makefile pkgdesc)
169 -- Get a temporary file to save the tests' source in
170 (tmpn, tmph) <- tempIdr
171 hPutStrLn tmph $
172 "module Test_______\n" ++
173 concat ["import " ++ show m ++ "\n"
174 | m <- modules pkgdesc] ++
175 "namespace Main\n" ++
176 " main : IO ()\n" ++
177 " main = do " ++
178 concat [show t ++ "\n "
179 | t <- idris_tests pkgdesc]
180 hClose tmph
181 (tmpn', tmph') <- tempfile
182 hClose tmph'
183 m_ist <- idris (Filename tmpn : NoREPL : Verbose : Output tmpn' : idris_opts pkgdesc)
184 rawSystem tmpn' []
185 setCurrentDirectory dir
186 case m_ist of
187 Nothing -> exitWith (ExitFailure 1)
188 Just ist -> do
189 -- Quit with error code if problem building
190 case errSpan ist of
191 Just _ -> exitWith (ExitFailure 1)
192 _ -> return ()
193 where tempIdr :: IO (FilePath, Handle)
194 tempIdr = do dir <- getTemporaryDirectory
195 openTempFile (normalise dir) "idristests.idr"
197-- | Install package
198installPkg :: PkgDesc -> IO ()
199installPkg pkgdesc
200 = do dir <- getCurrentDirectory
201 setCurrentDirectory $ dir </> sourcedir pkgdesc
202 case (execout pkgdesc) of
203 Nothing -> do mapM_ (installIBC (pkgname pkgdesc)) (modules pkgdesc)
204 installIdx (pkgname pkgdesc)
205 Just o -> return () -- do nothing, keep executable locally, for noe
206 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)
208-- ---------------------------------------------------------- [ Helper Methods ]
209-- Methods for building, testing, installing, and removal of idris
210-- packages.
212buildMods :: [Opt] -> [Name] -> IO (Maybe IState)
213buildMods opts ns = do let f = map (toPath . showCG) ns
214 idris (map Filename f ++ opts)
215 where toPath n = foldl1' (</>) $ splitOn "." n
217testLib :: Bool -> String -> String -> IO Bool
218testLib warn p f
219 = do d <- getDataDir
220 gcc <- getCC
221 (tmpf, tmph) <- tempfile
222 hClose tmph
223 let libtest = d </> "rts" </> "libtest.c"
224 e <- rawSystem gcc [libtest, "-l" ++ f, "-o", tmpf]
225 case e of
226 ExitSuccess -> return True
227 _ -> do if warn
228 then do putStrLn $ "Not building " ++ p ++
229 " due to missing library " ++ f
230 return False
231 else fail $ "Missing library " ++ f
233rmIBC :: Name -> IO ()
234rmIBC m = rmFile $ toIBCFile m
236rmIdx :: String -> IO ()
237rmIdx p = do let f = pkgIndex p
238 ex <- doesFileExist f
239 when ex $ rmFile f
241toIBCFile (UN n) = str n ++ ".ibc"
242toIBCFile (NS n ns) = foldl1' (</>) (reverse (toIBCFile n : map str ns))
244installIBC :: String -> Name -> IO ()
245installIBC p m = do let f = toIBCFile m
246 d <- getTargetDir
247 let destdir = d </> p </> getDest m
248 putStrLn $ "Installing " ++ f ++ " to " ++ destdir
249 createDirectoryIfMissing True destdir
250 copyFile f (destdir </> takeFileName f)
251 return ()
252 where getDest (UN n) = ""
253 getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : map str ns))
255installIdx :: String -> IO ()
256installIdx p = do d <- getTargetDir
257 let f = pkgIndex p
258 let destdir = d </> p
259 putStrLn $ "Installing " ++ f ++ " to " ++ destdir
260 createDirectoryIfMissing True destdir
261 copyFile f (destdir </> takeFileName f)
262 return ()
264installObj :: String -> String -> IO ()
265installObj p o = do d <- getTargetDir
266 let destdir = addTrailingPathSeparator (d </> p)
267 putStrLn $ "Installing " ++ o ++ " to " ++ destdir
268 createDirectoryIfMissing True destdir
269 copyFile o (destdir </> takeFileName o)
270 return ()
272#ifdef mingw32_HOST_OS
273mkDirCmd = "mkdir "
274#else
275mkDirCmd = "mkdir -p "
276#endif
278-- ------------------------------------------------------- [ Makefile Commands ]
279-- | Invoke a Makefile's default target.
280make :: Maybe String -> IO ()
281make Nothing = return ()
282make (Just s) = do rawSystem "make" ["-f", s]
283 return ()
285-- | Invoke a Makefile's clean target.
286clean :: Maybe String -> IO ()
287clean Nothing = return ()
288clean (Just s) = do rawSystem "make" ["-f", s, "clean"]
289 return ()
291-- --------------------------------------------------------------------- [ EOF ]