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