git.iko.soy/Idris-dev
on master help sign in
Get cabal to check library after install
commitec7c1b8e24625d1b7db37e4faadae9eba5e439c1 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 15 Dec 2011, 17:01 (15 years ago) parent6d01c6b
4 files changed+49−9
compare with master
unifiedsplit
Setup.hs+33 idris.cabal+2−3 lib/Makefile+5 src/Idris/IBC.hs+9−6
Setup.hsnew file+33
@@ -0,0 +1,33 @@
1+import Distribution.Simple
2+import Distribution.Simple.InstallDirs as I
3+import Distribution.Simple.LocalBuildInfo as L
4+import Distribution.PackageDescription
5+
6+import System.Exit
7+import System.Process
8+
9+-- After Idris is built, we need to check and install the prelude and other libs
10+
11+system' cmd = do
12+ exit <- system cmd
13+ case exit of
14+ ExitSuccess -> return ()
15+ ExitFailure _ -> exitWith exit
16+
17+postCleanLib args flags desc _
18+ = system' "make -C lib clean"
19+
20+addPrefix pfx var c = "export " ++ var ++ "=" ++ show pfx ++ "/" ++ c ++ ":$" ++ var
21+
22+postInstLib args flags desc local
23+ = do let pkg = localPkgDescr local
24+ let penv = packageTemplateEnv (package pkg)
25+ let dirs = substituteInstallDirTemplates penv (installDirTemplates local)
26+ let idir = fromPathTemplate (datadir dirs) ++ "/" ++
27+ fromPathTemplate (datasubdir dirs)
28+ system' $ "make -C lib install TARGET=" ++ idir
29+
30+main = defaultMainWithHooks (simpleUserHooks { postInst = postInstLib,
31+ postClean = postCleanLib })
32+
33+
idris.cabal+2−3
@@ -16,10 +16,9 @@ Description: Idris is an experimental language with full dependent types.
1616 related to Epigram and Agda. There is a tutorial at <http://www.idris-lang.org/tutorial.html>.
1717
1818Cabal-Version: >= 1.6
19−Build-type: Simple
19+Build-type: Custom
2020
21−Data-files: *.idr prelude/*.idr
22−Data-dir: lib
21+Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr
2322
2423Executable idris
2524 Main-is: Main.hs
lib/Makefile+5
@@ -7,6 +7,11 @@ check: .PHONY
77
88recheck: clean check
99
10+install: check
11+ install *.ibc $(TARGET)
12+ mkdir -p $(TARGET)/prelude
13+ install prelude/*.ibc $(TARGET)/prelude
14+
1015clean: .PHONY
1116 rm -f *.ibc
1217 rm -f prelude/*.ibc
src/Idris/IBC.hs+9−6
@@ -16,6 +16,7 @@ import Data.ByteString.Lazy as B hiding (length, elem)
1616import Control.Monad
1717import Control.Monad.State hiding (get, put)
1818import System.FilePath
19+import System.Directory
1920import System.Posix.Files
2021
2122import Paths_idris
@@ -53,7 +54,7 @@ writeIBC src f
5354 = do iLOG $ "Writing ibc " ++ show f
5455 i <- getIState
5556 case idris_metavars i \\ primDefs of
56− (_:_) -> fail "Can't write ibc when there are unsolve metavariables"
57+ (_:_) -> fail "Can't write ibc when there are unsolved metavariables"
5758 [] -> return ()
5859 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })
5960 lift $ encodeFile f ibcf
@@ -108,11 +109,13 @@ process i fn
108109 pDefs (ibc_defs i)
109110
110111timestampOlder :: FilePath -> FilePath -> IO ()
111−timestampOlder src ibc = do srcs <- getFileStatus src
112− ibcs <- getFileStatus ibc
113− if (modificationTime srcs > modificationTime ibcs)
114− then fail "Needs reloading"
115− else return ()
112+timestampOlder src ibc = do srcok <- doesFileExist src
113+ when srcok $ do
114+ srcs <- getFileStatus src
115+ ibcs <- getFileStatus ibc
116+ if (modificationTime srcs > modificationTime ibcs)
117+ then fail "Needs reloading"
118+ else return ()
116119
117120pImports :: [FilePath] -> Idris ()
118121pImports fs