27e3c69 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Use just-built dynamic RTS during library typecheck

Idris has been extended with a flag to choose which dynamic RTS library will be loaded on startup. The build system has been updated to build the dynamic RTS after Idris but before typechecking the stdlib. Typechecking the stdlib now uses the just-build dynmic RTS in dist/.

commit27e3c6961ca331cdb36a0bcd4cf307556e42c6c1 authorDavid Christiansen <david@davidchristiansen.dk> dateThu 4 Apr 2013, 16:01 (14 years ago) parent1f2e714

8 files changed+53−17

compare with master

unifiedsplit

Makefile+2−2 Setup.hs+17 effects/Makefile+3−3 lib/Makefile+3−3 rts/Makefile+5 src/Idris/AbsSyntaxTree.hs+1 src/Idris/REPL.hs+5−9 src/Main.hs+17

Makefile+2−2

@@ -17,8 +17,8 @@ test:

1717 make -C test

1818

1919relib:

20− make -C lib IDRIS=../dist/build/idris/idris clean

21− make -C effects IDRIS=../dist/build/idris/idris clean

20+ make -C lib IDRIS=../dist/build/idris/idris RTS=../dist/build/rts/libidris_rts clean

21+ make -C effects IDRIS=../dist/build/idris/idris DIST=../dist/build clean

2222 $(CABAL) install $(CABALFLAGS)

2323

2424linecount:

Setup.hs+17

@@ -28,8 +28,11 @@ mvn verbosity = P.runProgramInvocation verbosity . P.simpleProgramInvocation "mv

2828(<//>) = (Px.</>)

2929idrisCmd local = Px.joinPath $ splitDirectories $

3030 ".." <//> buildDir local <//> "idris" <//> "idris"

31+rtsDir local = Px.joinPath $ splitDirectories $

32+ ".." <//> buildDir local <//> "rts" <//> "libidris_rts"

3133#else

3234idrisCmd local = ".." </> buildDir local </> "idris" </> "idris"

35+rtsDir local = ".." </> buildDir local </> "rts" </> "libidris_rts"

3336#endif

3437

3538cleanStdLib verbosity

@@ -53,11 +56,13 @@ installStdLib pkg local verbosity copy

5356 [ "-C", "lib", "install"

5457 , "TARGET=" ++ idir

5558 , "IDRIS=" ++ icmd

59+ , "RTS=" ++ rtsDir local

5660 ]

5761 make verbosity

5862 [ "-C", "effects", "install"

5963 , "TARGET=" ++ idir

6064 , "IDRIS=" ++ icmd

65+ , "RTS=" ++ rtsDir local

6166 ]

6267 let idirRts = idir </> "rts"

6368 putStrLn $ "Installing run time system in " ++ idirRts

@@ -65,6 +70,7 @@ installStdLib pkg local verbosity copy

6570 [ "-C", "rts", "install"

6671 , "TARGET=" ++ idirRts

6772 , "IDRIS=" ++ icmd

73+ , "RTS=" ++ rtsDir local

6874 ]

6975

7076installJavaLib pkg local verbosity copy version = do

@@ -99,16 +105,25 @@ checkStdLib local verbosity

99105 make verbosity

100106 [ "-C", "lib", "check"

101107 , "IDRIS=" ++ icmd

108+ , "RTS=" ++ rtsDir local

102109 ]

103110 make verbosity

104111 [ "-C", "effects", "check"

105112 , "IDRIS=" ++ icmd

113+ , "RTS=" ++ rtsDir local

106114 ]

107115 make verbosity

108116 [ "-C", "rts", "check"

109117 , "IDRIS=" ++ icmd

110118 ]

111119

120+buildRTS dir verbosity

121+ = do putStrLn "Building RTS..."

122+ make verbosity

123+ [ "-C", "rts", "build"

124+ , "DIST=../" ++ dir

125+ ]

126+

112127checkJavaLib verbosity = mvn verbosity [ "-f", "java" </> "pom.xml", "package" ]

113128

114129javaFlag flags =

@@ -155,6 +170,8 @@ main = do

155170 cleanJavaLib verb

156171 , postBuild = \ _ flags _ lbi -> do

157172 let verb = S.fromFlag $ S.buildVerbosity flags

173+ let distdir = buildDir lbi

174+ buildRTS distdir verb

158175 checkStdLib lbi verb

159176 when (javaFlag $ configFlags lbi) (checkJavaLib verb)

160177 }

effects/Makefile+3−3

@@ -1,13 +1,13 @@

22check: .PHONY

3− $(IDRIS) --build effects.ipkg

3+ $(IDRIS) --dynamicrts $(RTS) --build effects.ipkg

55recheck: clean check

77install:

8− $(IDRIS) --install effects.ipkg

8+ $(IDRIS) --dynamicrts $(RTS) --install effects.ipkg

1010clean: .PHONY

11− $(IDRIS) --clean effects.ipkg

11+ $(IDRIS) --dynamicrts $(RTS) --clean effects.ipkg

1212

1313.PHONY:

lib/Makefile+3−3

@@ -1,14 +1,14 @@

22check: .PHONY

3− $(IDRIS) --build base.ipkg

3+ $(IDRIS) --dynamicrts $(RTS) --build base.ipkg

55recheck: clean check

77install:

8− $(IDRIS) --install base.ipkg

8+ $(IDRIS) --dynamicrts $(RTS) --install base.ipkg

1010clean: .PHONY

11− $(IDRIS) --clean base.ipkg

11+ $(IDRIS) --dynamicrts $(RTS) --clean base.ipkg

1212

1313linecount: .PHONY

1414 wc -l *.idr Network/*.idr Language/*.idr Prelude/*.idr Data/*.idr Control/Monad/*.idr Control/*.idr

rts/Makefile+5

@@ -20,6 +20,11 @@ $(LIBTARGET) : $(OBJS)

2020$(DYLIBTARGET) : $(OBJS)

2121 $(CC) $(CFLAGS) -shared -o $(DYLIBTARGET) $(OBJS)

2222

23+build: $(DYLIBTARGET)

24+ mkdir -p $(DIST)/rts

25+ install $(DYLIBTARGET) $(DIST)/rts

26+

27+

2328install : .PHONY

2429 mkdir -p $(TARGET)

2530 install $(LIBTARGET) $(DYLIBTARGET) $(HDRS) $(TARGET)

src/Idris/AbsSyntaxTree.hs+1

@@ -232,6 +232,7 @@ data Opt = Filename String

232232 | UseTarget Target

233233 | OutputTy OutputType

234234 | Extension LanguageExt

235+ | DynamicRTS FilePath

235236 deriving (Show, Eq)

236237

237238-- Parsed declarations

src/Idris/REPL.hs+5−9

@@ -496,6 +496,7 @@ parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)

496496parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

497497parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)

498498parseArgs ("-XTypeProviders":ns) = Extension TypeProviders : (parseArgs ns)

499+parseArgs ("--dynamicrts":f:ns) = DynamicRTS f : (parseArgs ns)

499500parseArgs (n:ns) = Filename n : (parseArgs ns)

500501

501502helphead =

@@ -552,15 +553,6 @@ idrisMain opts =

552553 [] -> setIBCSubDir ""

553554 (d:_) -> setIBCSubDir d

554555 setImportDirs importdirs

555− -- attempt to load the RTS as a shared lib in the interpreter

556− idrisCatch (do rtslib <- lift (getDataFileName $ "rts" </> "libidris_rts")

557− handle <- lift (tryLoadLib rtslib)

558− case handle of

559− Nothing -> return ()

560− Just x -> do i <- getIState

561− let libs = idris_dynamic_libs i

562− putIState $ i { idris_dynamic_libs = x:libs })

563− (\e -> iputStrLn (show e))

564556

565557 addPkgDir "base"

566558 mapM_ addPkgDir pkgdirs

@@ -645,6 +637,10 @@ getLanguageExt :: Opt -> Maybe LanguageExt

645637getLanguageExt (Extension e) = Just e

646638getLanguageExt _ = Nothing

647639

640+getDynamicRTS :: Opt -> Maybe FilePath

641+getDynamicRTS (DynamicRTS f) = Just f

642+getDynamicRTS _ = Nothing

643+

648644opt :: (Opt -> Maybe a) -> [Opt] -> [a]

649645opt = mapMaybe

650646

src/Main.hs+17

@@ -29,6 +29,7 @@ import Idris.Imports

2929import Idris.Error

3030

3131import Util.System ( getLibFlags, getIdrisLibDir, getIncFlags )

32+import Util.DynamicLinker

3233

3334import Pkg.Package

3435

@@ -48,6 +49,7 @@ runIdris opts = do

4849 when (ShowIncs `elem` opts) $ liftIO showIncs

4950 when (ShowLibs `elem` opts) $ liftIO showLibs

5051 when (ShowLibdir `elem` opts) $ liftIO showLibdir

52+ loadRTS opts

5153 case opt getPkgClean opts of

5254 [] -> return ()

5355 fs -> do liftIO $ mapM_ cleanPkg fs

@@ -94,3 +96,18 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

9496 "\t--link Show C library directories and exit (for C linking)\n" ++

9597 "\t--include Show C include directories and exit (for C linking)\n" ++

9698 "\t--target [target] Type the target: C, Java, bytecode, javascript, node\n"

99+

100+-- | Attempt to load the RTS as a shared lib in the interpreter

101+loadRTS :: [Opt] -> Idris ()

102+loadRTS opts = (flip idrisCatch) (\e -> iputStrLn (show e)) $

103+ do rtslib <- liftIO $

104+ case listToMaybe . catMaybes . map getDynamicRTS $ opts of

105+ Just path -> return path

106+ Nothing -> getDataFileName ("rts" </> "libidris_rts")

107+ handle <- liftIO (tryLoadLib rtslib)

108+ case handle of

109+ Nothing -> return ()

110+ Just x -> do i <- getIState

111+ let libs = idris_dynamic_libs i

112+ putIState $ i { idris_dynamic_libs = x:libs }

113+