26da5c7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Save index file when installing a package

This is just an IBC file listing the imports in the package, to be used when loading an entire package in one go for purposes of searching it.

commit26da5c740e945ca2df4605eacf306dc21d0f731f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 31 Dec 2014, 16:50 (12 years ago) parentd40cd6f

8 files changed+63−23

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/Help.hs+2 src/Idris/IBC.hs+16 src/Idris/Prover.hs+1−1 src/Idris/REPL.hs+11−2 src/Idris/REPLParser.hs+8−4 src/Idris/TypeSearch.hs+4−3 src/Pkg/Package.hs+19−12

src/Idris/AbsSyntaxTree.hs+2−1

@@ -346,7 +346,7 @@ data Command = Quit

346346 | DynamicLink FilePath

347347 | ListDynamic

348348 | Pattelab PTerm

349− | Search PTerm

349+ | Search [Name] PTerm

350350 | CaseSplitAt Bool Int Name

351351 | AddClauseFrom Bool Int Name

352352 | AddProofClauseFrom Bool Int Name

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

413413 | PkgREPL String

414414 | PkgMkDoc String -- IdrisDoc

415415 | PkgTest String

416+ | PkgIndex FilePath

416417 | WarnOnly

417418 | Pkg String

418419 | BCAsm String

src/Idris/Help.hs+2

@@ -4,6 +4,7 @@ data CmdArg = ExprArg -- ^ The command takes an expression

44 | NameArg -- ^ The command takes a name

55 | FileArg -- ^ The command takes a file

66 | ModuleArg -- ^ The command takes a module name

7+ | PkgArgs -- ^ The command takes a list of package names

78 | NumberArg -- ^ The command takes a number

89 | NamespaceArg -- ^ The command takes a namespace name

910 | OptionArg -- ^ The command takes an option

@@ -22,6 +23,7 @@ instance Show CmdArg where

2223 show NameArg = "<name>"

2324 show FileArg = "<filename>"

2425 show ModuleArg = "<module>"

26+ show PkgArgs = "<package list>"

2527 show NumberArg = "<number>"

2628 show NamespaceArg = "<namespace>"

2729 show OptionArg = "<option>"

src/Idris/IBC.hs+16

@@ -121,6 +121,22 @@ writeIBC src f

121121 (\c -> do iLOG $ "Failed " ++ pshow i c)

122122 return ()

123123

124+-- Write a package index containing all the imports in the current IState

125+-- Used for ':search' of an entire package, to ensure everything is loaded.

126+writePkgIndex :: FilePath -> Idris ()

127+writePkgIndex f

128+ = do i <- getIState

129+ let imps = map (\ (x, y) -> (True, x)) $ idris_imported i

130+ iLOG $ "Writing package index " ++ show f ++ " including\n" ++

131+ show (map snd imps)

132+ resetNameIdx

133+ let ibcf = initIBC { ibc_imports = imps }

134+ idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

135+ runIO $ bencode f ibcf

136+ iLOG "Written")

137+ (\c -> do iLOG $ "Failed " ++ pshow i c)

138+ return ()

139+

124140mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile

125141mkIBC [] f = return f

126142mkIBC (i:is) f = do ist <- getIState

src/Idris/Prover.hs+1−1

@@ -340,4 +340,4 @@ ploop fn d prompt prf e h

340340 return $ pprintDocs ist doc

341341 docStr (Right c) = do ist <- getIState

342342 return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))

343− search t = return (False, e, False, prf, Right $ searchByType t)

343+ search t = return (False, e, False, prf, Right $ searchByType [] t)

src/Idris/REPL.hs+11−2

@@ -33,6 +33,7 @@ import Idris.Output

3333import Idris.Interactive

3434import Idris.WhoCalls

3535import Idris.TypeSearch (searchByType)

36+import Idris.IBC (writePkgIndex)

3637

3738import Idris.Elab.Type

3839import Idris.Elab.Clause

@@ -540,7 +541,7 @@ ideslaveProcess fn (Defn n) = do process fn (Defn n)

540541ideslaveProcess fn (TotCheck n) = process fn (TotCheck n)

541542ideslaveProcess fn (DebugInfo n) = do process fn (DebugInfo n)

542543 iPrintResult ""

543−ideslaveProcess fn (Search t) = process fn (Search t)

544+ideslaveProcess fn (Search ps t) = process fn (Search ps t)

544545ideslaveProcess fn (Spec t) = process fn (Spec t)

545546-- RmProof and AddProof not supported!

546547ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')

@@ -957,7 +958,7 @@ process fn (DebugInfo n)

957958 when (not (null cg')) $ do iputStrLn "Call graph:\n"

958959 iputStrLn (show cg')

959960 when (not (null fn)) $ iputStrLn (show fn)

960−process fn (Search t) = searchByType t

961+process fn (Search pkgs t) = searchByType pkgs t

961962process fn (CaseSplitAt updatefile l n)

962963 = caseSplitAt fn updatefile l n

963964process fn (AddClauseFrom updatefile l n)

@@ -1568,6 +1569,10 @@ idrisMain opts =

15681569

15691570 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir

15701571

1572+ when ok $ case opt getPkgIndex opts of

1573+ (f : _) -> writePkgIndex f

1574+ _ -> return ()

1575+

15711576 when (runrepl && not idesl) $ do

15721577-- clearOrigPats

15731578 startServer port orig inputs

@@ -1706,6 +1711,10 @@ getExecScript :: Opt -> Maybe String

17061711getExecScript (InterpretScript expr) = Just expr

17071712getExecScript _ = Nothing

17081713

1714+getPkgIndex :: Opt -> Maybe FilePath

1715+getPkgIndex (PkgIndex file) = Just file

1716+getPkgIndex _ = Nothing

1717+

17091718getEvalExpr :: Opt -> Maybe String

17101719getEvalExpr (EvalExpr expr) = Just expr

17111720getEvalExpr _ = Nothing

src/Idris/REPLParser.hs+8−4

@@ -385,10 +385,14 @@ cmd_colour name = do

385385

386386

387387cmd_search :: String -> P.IdrisParser (Either String Command)

388−cmd_search name = do

389− P.whiteSpace;

390− t <- P.typeExpr (defaultSyntax { implicitAllowed = True })

391− return (Right (Search t))

388+cmd_search name =

389+ try (do P.whiteSpace

390+ pkgs <- sepBy P.name (P.lchar ',')

391+ t <- P.typeExpr (defaultSyntax { implicitAllowed = True })

392+ return (Right (Search pkgs t)))

393+ <|> do P.whiteSpace;

394+ t <- P.typeExpr (defaultSyntax { implicitAllowed = True })

395+ return (Right (Search [] t))

392396

393397cmd_proofsearch :: String -> P.IdrisParser (Either String Command)

394398cmd_proofsearch name = do

src/Idris/TypeSearch.hs+4−3

@@ -20,7 +20,7 @@ import qualified Data.Set as S

2020import qualified Data.Text as T (pack, isPrefixOf)

2121import Data.Traversable (traverse)

2222

23−import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit)

23+import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit, logLvl)

2424import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, eqTy, Idris,

2525 IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),

2626 implicitAllowed, OutputMode(..), PTerm, toplevel)

@@ -36,8 +36,9 @@ import Prelude hiding (pred)

3636

3737import Util.Pretty (text, char, vsep, (<>), Doc, annotate)

3838

39−searchByType :: PTerm -> Idris ()

40−searchByType pterm = do

39+searchByType :: [Name] -> PTerm -> Idris ()

40+searchByType pkgs pterm = do

41+ logLvl 0 $ "Searching in " ++ show pkgs

4142 pterm' <- addUsingConstraints syn emptyFC pterm

4243 pterm'' <- implicit toplevel syn name pterm'

4344 i <- getIState

src/Pkg/Package.hs+19−12

@@ -23,6 +23,7 @@ import Idris.Parser (loadModule)

2323import Idris.Output (pshow)

2424import Idris.AbsSyntax

2525import Idris.IdrisDoc

26+import Idris.IBC

2627import Idris.Output

2728

2829import IRTS.System

@@ -36,21 +37,26 @@ import Pkg.PParser

3637-- * invoke idris on each module, with idris_opts

3738-- * install everything into datadir/pname, if install flag is set

3839

40+-- | Get the index file name for a package name

41+pkgIndex :: String -> FilePath

42+pkgIndex s = "00" ++ s ++ "-idx.ibc"

43+

3944-- | Run the package through the idris compiler.

4045buildPkg :: Bool -> (Bool, FilePath) -> IO ()

4146buildPkg warnonly (install, fp)

4247 = do pkgdesc <- parseDesc fp

48+ let idx = PkgIndex (pkgIndex (pkgname pkgdesc))

4349 ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)

4450 when (and ok) $

4551 do dir <- getCurrentDirectory

4652 setCurrentDirectory $ dir </> sourcedir pkgdesc

4753 make (makefile pkgdesc)

4854 m_ist <- case (execout pkgdesc) of

49− Nothing -> buildMods (NoREPL : Verbose : idris_opts pkgdesc)

55+ Nothing -> buildMods (idx : NoREPL : Verbose : idris_opts pkgdesc)

5056 (modules pkgdesc)

5157 Just o -> do let exec = dir </> o

5258 buildMods

53− (NoREPL : Verbose : Output exec : idris_opts pkgdesc)

59+ (idx : NoREPL : Verbose : Output exec : idris_opts pkgdesc)

5460 [idris_main pkgdesc]

5561 setCurrentDirectory dir

5662 case m_ist of

@@ -60,14 +66,7 @@ buildPkg warnonly (install, fp)

6066 case errSpan ist of

6167 Just _ -> exitWith (ExitFailure 1)

6268 _ -> return ()

63− -- Also give up if there are metavariables to solve

64− case (map fst (idris_metavars ist) \\ primDefs) of

65− _ -> when install $ installPkg pkgdesc

66−-- ms -> do if install

67−-- then putStrLn "Can't install: there are undefined metavariables:"

68−-- else putStrLn "There are undefined metavariables:"

69−-- putStrLn $ "\t" ++ show ms

70−-- exitWith (ExitFailure 1)

69+ when install $ installPkg pkgdesc

7170

7271-- | Type check packages only

7372--

@@ -203,7 +202,8 @@ installPkg pkgdesc

203202 = do dir <- getCurrentDirectory

204203 setCurrentDirectory $ dir </> sourcedir pkgdesc

205204 case (execout pkgdesc) of

206− Nothing -> mapM_ (installIBC (pkgname pkgdesc)) (modules pkgdesc)

205+ Nothing -> do mapM_ (installIBC (pkgname pkgdesc)) (modules pkgdesc)

206+ installIdx (pkgname pkgdesc)

207207 Just o -> return () -- do nothing, keep executable locally, for noe

208208 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)

209209

@@ -213,7 +213,6 @@ installPkg pkgdesc

213213

214214buildMods :: [Opt] -> [Name] -> IO (Maybe IState)

215215buildMods opts ns = do let f = map (toPath . showCG) ns

216−-- putStrLn $ "MODULE: " ++ show f

217216 idris (map Filename f ++ opts)

218217 where toPath n = foldl1' (</>) $ splitOn "." n

219218

@@ -250,6 +249,14 @@ installIBC p m = do let f = toIBCFile m

250249 where getDest (UN n) = ""

251250 getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : map str ns))

252251

252+installIdx :: String -> IO ()

253+installIdx p = do d <- getTargetDir

254+ let f = pkgIndex p

255+ let destdir = d </> p

256+ putStrLn $ "Installing " ++ f ++ " to " ++ destdir

257+ createDirectoryIfMissing True destdir

258+ copyFile f (destdir </> takeFileName f)

259+ return ()

253260

254261installObj :: String -> String -> IO ()

255262installObj p o = do d <- getTargetDir