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