Add flag to explicitly refresh the project

cryptol-repl-internal/REPL/Haskeline.hs

@@ -132,8 +132,12 @@ loadCryRC cryrc =
                            else return status
 
 -- | Haskeline-specific repl implementation.
-repl :: Cryptolrc -> Maybe Project.Config -> ReplMode -> Bool -> Bool -> REPL () -> IO CommandResult
-repl cryrc projectConfig replMode callStacks stopOnError begin =
+repl ::
+  Cryptolrc ->
+  Maybe Project.Config ->
+  Bool {- ^ refresh project -} ->
+  ReplMode -> Bool -> Bool -> REPL () -> IO CommandResult
+repl cryrc projectConfig projectRefresh replMode callStacks stopOnError begin =
   runREPL isBatch callStacks stdoutLogger replAction
 
  where
@@ -152,7 +156,7 @@ repl cryrc projectConfig replMode callStacks stopOnError begin =
        if crSuccess status then do
           begin
           case projectConfig of
-            Just config -> loadProjectREPL config
+            Just config -> loadProjectREPL projectRefresh config
             Nothing     -> crySession replMode stopOnError
        else return status
 

cryptol/Main.hs

@@ -51,6 +51,7 @@ data Options = Options
   , optHelp            :: Bool
   , optBatch           :: ReplMode
   , optProject         :: Maybe FilePath
+  , optProjectRefresh  :: Bool
   , optCallStacks      :: Bool
   , optCommands        :: [String]
   , optColorMode       :: ColorMode
@@ -67,6 +68,7 @@ defaultOptions  = Options
   , optHelp            = False
   , optBatch           = InteractiveRepl
   , optProject         = Nothing
+  , optProjectRefresh  = False
   , optCallStacks      = True
   , optCommands        = []
   , optColorMode       = AutoColor
@@ -87,6 +89,9 @@ options  =
   , Option "p" ["project"] (ReqArg setProject "CRYPROJECT")
     ("Load and verify a Cryptol project using the provided project "
       ++ "configuration file or directory containing 'cryproject.toml'")
+
+  , Option "" ["refresh-project"] (NoArg setProjectRefresh)
+    "Ignore a pre-existing cache file when loading a project."
 
   , Option "e" ["stop-on-error"] (NoArg setStopOnError)
     "stop script execution as soon as an error occurs."
@@ -149,6 +154,9 @@ setInteractiveBatchScript path = modify $ \ opts -> opts { optBatch = Interactiv
 setProject :: String -> OptParser Options
 setProject path = modify $ \opts -> opts { optProject = Just path }
 
+setProjectRefresh :: OptParser Options
+setProjectRefresh = modify $ \opts -> opts { optProjectRefresh = True }
+
 -- | Set the color mode of the terminal output.
 setColorMode :: String -> OptParser Options
 setColorMode "auto"   = modify $ \ opts -> opts { optColorMode = AutoColor }
@@ -240,6 +248,7 @@ main  = do
           (opts'', mConfig) <- setupProject opts'
           status <- repl (optCryptolrc opts'')
                          mConfig
+                         (optProjectRefresh opts'')
                          (optBatch opts'')
                          (optCallStacks opts'')
                          (optStopOnError opts'')

src/Cryptol/Project.hs

@@ -33,9 +33,9 @@ import Cryptol.Parser.Position (Located(..))
 
 -- | Load a project.
 -- Returns information about the modules that are part of the project.
-loadProject :: Config -> M.ModuleM (Map CacheModulePath FullFingerprint, Map ModulePath ScanStatus, Map CacheModulePath (Maybe Bool))
-loadProject cfg =
-   do (fps, statuses, out) <- runLoadM cfg (for_ (modules cfg) scanPath >> getOldDocstringResults)
+loadProject :: Bool -> Config -> M.ModuleM (Map CacheModulePath FullFingerprint, Map ModulePath ScanStatus, Map CacheModulePath (Maybe Bool))
+loadProject refresh cfg =
+   do (fps, statuses, out) <- runLoadM refresh cfg (for_ (modules cfg) scanPath >> getOldDocstringResults)
       let deps = depMap [p | Scanned _ _ ps <- Map.elems statuses, p <- ps]
       let needLoad = [thing (P.mName m) | Scanned Changed _ ps <- Map.elems statuses, (m, _) <- ps]
       let order = loadOrder deps needLoad

src/Cryptol/Project/Cache.hs

@@ -36,6 +36,7 @@ instance Toml.ToValue LoadCache where
 
 instance Toml.ToTable LoadCache where
   toTable x = Toml.table [
+    "version" Toml..= (1 :: Int), -- increase this to invalidate old files
     "modules" Toml..= [
       Toml.table $ [
         case k of
@@ -60,7 +61,8 @@ instance Toml.ToTable LoadCache where
 
 instance Toml.FromValue LoadCache where
   fromValue = Toml.parseTableFromValue
-   do kvs <- Toml.reqKeyOf "modules"
+   do 1 <- Toml.reqKey "version" :: Toml.ParseTable l Int
+      kvs <- Toml.reqKeyOf "modules"
            $ Toml.listOf \ _ix ->
              Toml.parseTableFromValue
              do k <- Toml.pickKey [

src/Cryptol/Project/Monad.hs

@@ -133,14 +133,15 @@ liftCallback f (LoadM m) =
 
 -- | Run a LoadM computation using the given configuration.
 runLoadM ::
+  Bool {- ^ force a refresh -} ->
   Config ->
   LoadM NoErr a ->
   M.ModuleM (Map CacheModulePath FullFingerprint, Map ModulePath ScanStatus, Either ModuleError a)
-runLoadM cfg (LoadM m) =
+runLoadM refresh cfg (LoadM m) =
   do loadCfg <-
        M.io
          do path  <- canonicalizePath (root cfg)
-            cache <- loadLoadCache
+            cache <- if refresh then pure emptyLoadCache else loadLoadCache
             pure LoadConfig { canonRoot = path
                             , loadCache = cache
                             }

src/Cryptol/REPL/Command.hs

@@ -2238,10 +2238,10 @@ checkModName mn =
 -- | Load a project.
 -- Note that this does not update the Cryptol environment, it only updates
 -- the project cache.
-loadProjectREPL :: Proj.Config -> REPL CommandResult
-loadProjectREPL cfg =
+loadProjectREPL :: Bool -> Proj.Config -> REPL CommandResult
+loadProjectREPL refresh cfg =
  do minp <- getModuleInput
-    (res, warnings) <- io $ M.runModuleM minp $ Proj.loadProject cfg
+    (res, warnings) <- io $ M.runModuleM minp $ Proj.loadProject refresh cfg
     printModuleWarnings warnings
     case res of
       Left err ->