@@ -2,7 +2,8 @@
22{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
33
44module Idris.IBC (loadIBC, loadPkgIndex,
5− writeIBC, writePkgIndex) where
5+ writeIBC, writePkgIndex,
6+ hasValidIBCVersion) where
67
78import Idris.Core.Evaluate
89import Idris.Core.TT
@@ -94,6 +95,14 @@ deriving instance Binary IBCFile
9495initIBC :: IBCFile
9596initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []
9697
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+
97106loadIBC :: Bool -- ^ True = reexport, False = make everything private
98107 -> FilePath -> Idris ()
99108loadIBC reexport fp