on master help sign in
Merge pull request #2441 from paulkoerbitz/1163-Replace-outdated-IBC-files
7a67320Niklas Larsson
src/Idris/Chaser.hs+15−18
@@ -116,29 +116,26 @@ buildTree built fp = btree [] fp
116 else return []
116 else return []
117 mt <- idrisCatch (runIO $ getModificationTime fn)
117 mt <- idrisCatch (runIO $ getModificationTime fn)
118 (\c -> runIO $ getIModTime src)
118 (\c -> runIO $ getIModTime src)
119− ok <- checkIBCUpToDate fn src
119+ -- FIXME: It's also not up to date if anything it imports has
120+ -- been modified since its own ibc has.
121+ --
122+ -- Issue #1592 on the issue tracker.
123+ --
124+ -- https://github.com/idris-lang/Idris-dev/issues/1592
125+ ibcOutdated <- fn `younger` (getSrcFile src)
126+ ibcValid <- hasValidIBCVersion fn
120− return [MTree (IBC fn src) ok mt ms]
127+ return [MTree (IBC fn src) (ibcOutdated || not ibcValid) mt ms]
121
128
122 getSrcFile (IBC _ src) = getSrcFile src
129 getSrcFile (IBC _ src) = getSrcFile src
123 getSrcFile (LIDR src) = src
130 getSrcFile (LIDR src) = src
124 getSrcFile (IDR src) = src
131 getSrcFile (IDR src) = src
125
132
126− -- FIXME: It's also not up to date if anything it imports has
127− -- been modified since its own ibc has.
128− --
129− -- Issue #1592 on the issue tracker.
130− --
131− -- https://github.com/idris-lang/Idris-dev/issues/1592
132−
133− checkIBCUpToDate fn (LIDR src) = older fn src
134− checkIBCUpToDate fn (IDR src) = older fn src
135−
136− older ibc src = do exist <- runIO $ doesFileExist src
133+ younger ibc src = do exist <- runIO $ doesFileExist src
137− if exist then do
134+ if exist then do
138− ibct <- runIO $ getModificationTime ibc
135+ ibct <- runIO $ getModificationTime ibc
139− srct <- runIO $ getModificationTime src
136+ srct <- runIO $ getModificationTime src
140− return (srct >= ibct)
137+ return (srct > ibct)
141− else return False
138+ else return False
142
139
143 children :: Bool -> FilePath -> [FilePath] -> Idris [ModuleTree]
140 children :: Bool -> FilePath -> [FilePath] -> Idris [ModuleTree]
144 children lit f done = -- idrisCatch
141 children lit f done = -- idrisCatch
src/Idris/IBC.hs+10−1
@@ -2,7 +2,8 @@
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3
3
4module Idris.IBC (loadIBC, loadPkgIndex,
4module Idris.IBC (loadIBC, loadPkgIndex,
5− writeIBC, writePkgIndex) where
5+ writeIBC, writePkgIndex,
6+ hasValidIBCVersion) where
6
7
7import Idris.Core.Evaluate
8import Idris.Core.Evaluate
8import Idris.Core.TT
9import Idris.Core.TT
@@ -94,6 +95,14 @@ deriving instance Binary IBCFile
94initIBC :: IBCFile
95initIBC :: IBCFile
95initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []
96initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []
96
97
98+hasValidIBCVersion :: FilePath -> Idris Bool
99+hasValidIBCVersion fp = do
100+ archiveFile <- runIO $ B.readFile fp
101+ case toArchiveOrFail archiveFile of
102+ Left _ -> return False
103+ Right archive -> do ver <- getEntry 0 "ver" archive
104+ return (ver == ibcVersion)
105+
97loadIBC :: Bool -- ^ True = reexport, False = make everything private
106loadIBC :: Bool -- ^ True = reexport, False = make everything private
98 -> FilePath -> Idris ()
107 -> FilePath -> Idris ()
99loadIBC reexport fp
108loadIBC reexport fp