git.iko.soy/Idris-dev
on f2bf55d help sign in
Idris-dev/src/Pkg/Package.hs
244 lines 9.5 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)
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)
163-- | Install package
164installPkg :: PkgDesc -> IO ()
165installPkg pkgdesc
166 = do dir <- getCurrentDirectory
167 setCurrentDirectory $ dir </> sourcedir pkgdesc
168 case (execout pkgdesc) of
169 Nothing -> mapM_ (installIBC (pkgname pkgdesc)) (modules pkgdesc)
170 Just o -> return () -- do nothing, keep executable locally, for noe
171 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)
173-- ---------------------------------------------------------- [ Helper Methods ]
174-- Methods for building, testing, installing, and removal of idris
175-- packages.
177buildMods :: [Opt] -> [Name] -> IO (Maybe IState)
178buildMods opts ns = do let f = map (toPath . showCG) ns
179-- putStrLn $ "MODULE: " ++ show f
180 idris (map Filename f ++ opts)
181 where toPath n = foldl1' (</>) $ splitOn "." n
183testLib :: Bool -> String -> String -> IO Bool
184testLib warn p f
185 = do d <- getDataDir
186 gcc <- getCC
187 (tmpf, tmph) <- tempfile
188 hClose tmph
189 let libtest = d </> "rts" </> "libtest.c"
190 e <- system $ gcc ++ " " ++ libtest ++ " -l" ++ f ++ " -o " ++ tmpf
191 case e of
192 ExitSuccess -> return True
193 _ -> do if warn
194 then do putStrLn $ "Not building " ++ p ++
195 " due to missing library " ++ f
196 return False
197 else fail $ "Missing library " ++ f
199rmIBC :: Name -> IO ()
200rmIBC m = rmFile $ toIBCFile m
202toIBCFile (UN n) = str n ++ ".ibc"
203toIBCFile (NS n ns) = foldl1' (</>) (reverse (toIBCFile n : map str ns))
205installIBC :: String -> Name -> IO ()
206installIBC p m = do let f = toIBCFile m
207 d <- getTargetDir
208 let destdir = d </> p </> getDest m
209 putStrLn $ "Installing " ++ f ++ " to " ++ destdir
210 createDirectoryIfMissing True destdir
211 copyFile f (destdir </> takeFileName f)
212 return ()
213 where getDest (UN n) = ""
214 getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : map str ns))
217installObj :: String -> String -> IO ()
218installObj p o = do d <- getTargetDir
219 let destdir = addTrailingPathSeparator (d </> p)
220 putStrLn $ "Installing " ++ o ++ " to " ++ destdir
221 createDirectoryIfMissing True destdir
222 copyFile o (destdir </> takeFileName o)
223 return ()
225#ifdef mingw32_HOST_OS
226mkDirCmd = "mkdir "
227#else
228mkDirCmd = "mkdir -p "
229#endif
231-- ------------------------------------------------------- [ Makefile Commands ]
232-- | Invoke a Makefile's default target.
233make :: Maybe String -> IO ()
234make Nothing = return ()
235make (Just s) = do system $ "make -f " ++ s
236 return ()
238-- | Invoke a Makefile's clean target.
239clean :: Maybe String -> IO ()
240clean Nothing = return ()
241clean (Just s) = do system $ "make -f " ++ s ++ " clean"
242 return ()
244-- --------------------------------------------------------------------- [ EOF ]