ec7c1b8 · Idris-dev · git.iko.soy

Setup.hsnew file+33

compare with master

unifiedsplit

@@ -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.

16 related to Epigram and Agda. There is a tutorial at <http://www.idris-lang.org/tutorial.html>.

17

18Cabal-Version: >= 1.6

19−Build-type: Simple

19+Build-type: Custom

20

21−Data-files: *.idr prelude/*.idr

21+Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr

22−Data-dir: lib

23

22

24Executable idris

23Executable idris

25 Main-is: Main.hs

24 Main-is: Main.hs

lib/Makefile+5

@@ -7,6 +7,11 @@ check: .PHONY

7

8recheck: clean check

9

10+install: check

11+ install *.ibc $(TARGET)

12+ mkdir -p $(TARGET)/prelude

13+ install prelude/*.ibc $(TARGET)/prelude

14+

10clean: .PHONY

15clean: .PHONY

11 rm -f *.ibc

16 rm -f *.ibc

12 rm -f prelude/*.ibc

17 rm -f prelude/*.ibc

src/Idris/IBC.hs+9−6

@@ -16,6 +16,7 @@ import Data.ByteString.Lazy as B hiding (length, elem)

16import Control.Monad

17import Control.Monad.State hiding (get, put)

18import System.FilePath

19+import System.Directory

19import System.Posix.Files

20import System.Posix.Files

20

21

21import Paths_idris

22import Paths_idris

@@ -53,7 +54,7 @@ writeIBC src f

53 = do iLOG $ "Writing ibc " ++ show f

54 = do iLOG $ "Writing ibc " ++ show f

54 i <- getIState

55 i <- getIState

55 case idris_metavars i \\ primDefs of

56 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"

57 [] -> return ()

58 [] -> return ()

58 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

59 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

59 lift $ encodeFile f ibcf

60 lift $ encodeFile f ibcf

@@ -108,11 +109,13 @@ process i fn

108 pDefs (ibc_defs i)

109 pDefs (ibc_defs i)

109

110

110timestampOlder :: FilePath -> FilePath -> IO ()

111timestampOlder :: FilePath -> FilePath -> IO ()

112+timestampOlder src ibc = do srcok <- doesFileExist src

113+ when srcok $ do

111−timestampOlder src ibc = do srcs <- getFileStatus src

114+ srcs <- getFileStatus src

112− ibcs <- getFileStatus ibc

115+ ibcs <- getFileStatus ibc

113− if (modificationTime srcs > modificationTime ibcs)

116+ if (modificationTime srcs > modificationTime ibcs)

114− then fail "Needs reloading"

117+ then fail "Needs reloading"

115− else return ()

118+ else return ()

116

119

117pImports :: [FilePath] -> Idris ()

120pImports :: [FilePath] -> Idris ()

118pImports fs

121pImports fs