Cryptol Projects (#1526)

* Add support for incrementally loading projects via cryptol's `--project` flag as documented in the reference manual. ([#1641](#1641)) --------- Co-authored-by: Iavor Diatchki <[email protected]> Co-authored-by: Eric Mertens <[email protected]>
GaloisInc · Dec 20, 2024 · 8406878 · 8406878
1 parent 9cb3eed
commit 8406878
Show file tree

Hide file tree

Showing 32 changed files with 1,195 additions and 197 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -24,6 +24,10 @@
 * The REPL properly supports tab completion for the `:t` and `:check` commands.
   ([#1780](https://github.com/GaloisInc/cryptol/issues/1780))
 
+* Add support for incrementally loading projects via cryptol's `--project`
+  flag as documented in the reference manual.
+  ([#1641](https://github.com/GaloisInc/cryptol/issues/1641))
+
 # 3.2.0 -- 2024-08-20
 
 ## Language changes

diff --git a/cryptol-remote-api/python/tests/cryptol/test_filedeps.py b/cryptol-remote-api/python/tests/cryptol/test_filedeps.py
@@ -10,7 +10,7 @@ def test_FileDeps(self) -> None:
         connect(verify=False)
         path = str(Path('tests','cryptol','test-files','Id.cry'))
         result = file_deps(path,True)
-        self.assertEqual(result['fingerprint'],"8A49C6A461AF276DF56C4FE4279BCFC51D891214")
+        self.assertEqual(result['fingerprint'],"8316fb4e38d33ec3b9f89d355597c058b2e4baf653bf18dc4ead7e166a8a32f8")
         self.assertEqual(result['foreign'],[])
         self.assertEqual(result['imports'],['Cryptol'])
         self.assertEqual(result['includes'],[])

diff --git a/cryptol-remote-api/src/CryptolServer.hs b/cryptol-remote-api/src/CryptolServer.hs
@@ -195,6 +195,6 @@ validateServerState =
         InMem{} -> continue
         InFile file ->
           do fp <- fingerprintFile file
-             if fp == Just (fiFingerprint (lmFileInfo lm))
+             if fp == Right (fiFingerprint (lmFileInfo lm))
                then continue
                else return False
diff --git a/cryptol-remote-api/src/CryptolServer/Exceptions.hs b/cryptol-remote-api/src/CryptolServer/Exceptions.hs
@@ -57,17 +57,19 @@ cryptolError modErr warns =
       CantFindFile path ->
         (20050, [ ("path", jsonString path)
                 ])
-      BadUtf8 path ue ->
+      BadUtf8 path fp ue ->
         (20010, [ ("path", jsonShow path)
                 , ("error", jsonShow ue)
+                , ("fingerprint", jsonShow fp)
                 ])
       OtherIOError path exn ->
         (20060, [ ("path", jsonString path)
                 , ("error", jsonShow exn)
                 ])
-      ModuleParseError source message ->
+      ModuleParseError source fp message ->
         (20540, [ ("source", jsonShow source)
                 , ("error", jsonShow message)
+                , ("fingerprint", jsonShow fp)
                 ])
       RecursiveModules mods ->
         (20550, [ ("modules", jsonList (reverse (map jsonPretty mods)))

diff --git a/cryptol-remote-api/src/CryptolServer/FileDeps.hs b/cryptol-remote-api/src/CryptolServer/FileDeps.hs
@@ -9,6 +9,7 @@ module CryptolServer.FileDeps
 import Data.Text (Text)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
+import qualified Data.Map.Strict as Map
 
 import qualified Data.Aeson as JSON
 import Data.Aeson (FromJSON(..),ToJSON(..),(.=),(.:))
@@ -67,7 +68,7 @@ instance ToJSON FileDeps where
                            InFile f  -> toJSON f
                            InMem l _ -> JSON.object [ "internal" .= l ]
       , "fingerprint" .= fingerprintHexString (fiFingerprint fi)
-      , "includes"    .= Set.toList (fiIncludeDeps fi)
+      , "includes"    .= Map.keys (fiIncludeDeps fi)
       , "imports"     .= map (show . pp) (Set.toList (fiImportDeps fi))
       , "foreign"     .= Map.toList (fiForeignDeps fi)
       ]

diff --git a/cryptol-repl-internal/REPL/Haskeline.hs b/cryptol-repl-internal/REPL/Haskeline.hs
@@ -14,6 +14,7 @@
 
 module REPL.Haskeline where
 
+import qualified Cryptol.Project as Project
 import           Cryptol.REPL.Command
 import           Cryptol.REPL.Monad
 import           Cryptol.REPL.Trie
@@ -131,22 +132,33 @@ loadCryRC cryrc =
                            else return status
 
 -- | Haskeline-specific repl implementation.
-repl :: Cryptolrc -> ReplMode -> Bool -> Bool -> REPL () -> IO CommandResult
-repl cryrc 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
   -- this flag is used to suppress the logo and prompts
-  isBatch = case replMode of
-              InteractiveRepl -> False
-              Batch _ -> True
-              InteractiveBatch _ -> True
+  isBatch =
+    case projectConfig of
+      Just _ -> True
+      Nothing ->
+        case replMode of
+          InteractiveRepl -> False
+          Batch _ -> True
+          InteractiveBatch _ -> True
 
   replAction =
     do status <- loadCryRC cryrc
-       if crSuccess status
-         then begin >> crySession replMode stopOnError
-         else return status
+       if crSuccess status then do
+          begin
+          case projectConfig of
+            Just config -> loadProjectREPL projectRefresh config
+            Nothing     -> crySession replMode stopOnError
+       else return status
 
 -- | Try to set the history file.
 setHistoryFile :: Settings REPL -> IO (Settings REPL)

diff --git a/cryptol.cabal b/cryptol.cabal
@@ -54,7 +54,7 @@ library
                        array             >= 0.4,
                        containers        >= 0.5,
                        criterion-measurement,
-                       cryptohash-sha1   >= 0.11 && < 0.12,
+                       cryptohash-sha256 >= 0.11 && < 0.12,
                        deepseq           >= 1.3,
                        directory         >= 1.2.2.0,
                        exceptions,
@@ -63,6 +63,7 @@ library
                        gitrev            >= 1.0,
                        ghc-prim,
                        GraphSCC          >= 1.0.4,
+                       heredoc           >= 0.2,
                        language-c99,
                        language-c99-simple,
                        libBF             >= 0.6 && < 0.7,
@@ -80,6 +81,7 @@ library
                        strict,
                        text              >= 1.1,
                        tf-random         >= 0.5,
+                       toml-parser       >= 2.0 && <2.1,
                        transformers-base >= 0.4,
                        vector,
                        mtl               >= 2.2.1,
@@ -238,7 +240,12 @@ library
                        Cryptol.REPL.Help,
                        Cryptol.REPL.Browse,
                        Cryptol.REPL.Monad,
-                       Cryptol.REPL.Trie
+                       Cryptol.REPL.Trie,
+
+                       Cryptol.Project
+                       Cryptol.Project.Config
+                       Cryptol.Project.Monad
+                       Cryptol.Project.Cache
 
   Other-modules:       Cryptol.Parser.LexerUtils,
                        Cryptol.Parser.ParserUtils,

diff --git a/cryptol/Main.hs b/cryptol/Main.hs
@@ -8,6 +8,7 @@
 
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
 module Main where
 
@@ -18,6 +19,7 @@ import Cryptol.REPL.Monad (REPL,updateREPLTitle,setUpdateREPLTitle,
                    io,prependSearchPath,setSearchPath,parseSearchPath)
 import qualified Cryptol.REPL.Monad as REPL
 import Cryptol.ModuleSystem.Env(ModulePath(..))
+import qualified Cryptol.Project as Project
 
 import REPL.Haskeline
 import REPL.Logo
@@ -26,6 +28,7 @@ import Cryptol.Utils.PP
 import Cryptol.Version (displayVersion)
 
 import Control.Monad (when, void)
+import Data.Maybe (isJust, isNothing)
 import GHC.IO.Encoding (setLocaleEncoding, utf8)
 import System.Console.GetOpt
     (OptDescr(..),ArgOrder(..),ArgDescr(..),getOpt,usageInfo)
@@ -47,6 +50,8 @@ data Options = Options
   , optVersion         :: Bool
   , optHelp            :: Bool
   , optBatch           :: ReplMode
+  , optProject         :: Maybe FilePath
+  , optProjectRefresh  :: Bool
   , optCallStacks      :: Bool
   , optCommands        :: [String]
   , optColorMode       :: ColorMode
@@ -62,6 +67,8 @@ defaultOptions  = Options
   , optVersion         = False
   , optHelp            = False
   , optBatch           = InteractiveRepl
+  , optProject         = Nothing
+  , optProjectRefresh  = False
   , optCallStacks      = True
   , optCommands        = []
   , optColorMode       = AutoColor
@@ -79,6 +86,13 @@ options  =
   , Option "" ["interactive-batch"] (ReqArg setInteractiveBatchScript "FILE")
     "run the script provided and exit, but behave as if running an interactive session"
 
+  , 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."
 
@@ -137,6 +151,12 @@ setBatchScript path = modify $ \ opts -> opts { optBatch = Batch path }
 setInteractiveBatchScript :: String -> OptParser Options
 setInteractiveBatchScript path = modify $ \ opts -> opts { optBatch = InteractiveBatch path }
 
+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 }
@@ -225,11 +245,14 @@ main  = do
       | optVersion opts -> displayVersion putStrLn
       | otherwise       -> do
           (opts', mCleanup) <- setupCmdScript opts
-          status <- repl (optCryptolrc opts')
-                         (optBatch opts')
-                         (optCallStacks opts')
-                         (optStopOnError opts')
-                         (setupREPL opts')
+          (opts'', mConfig) <- setupProject opts'
+          status <- repl (optCryptolrc opts'')
+                         mConfig
+                         (optProjectRefresh opts'')
+                         (optBatch opts'')
+                         (optCallStacks opts'')
+                         (optStopOnError opts'')
+                         (setupREPL opts'')
           case mCleanup of
             Nothing -> return ()
             Just cmdFile -> removeFile cmdFile
@@ -249,7 +272,27 @@ setupCmdScript opts =
       hClose h
       when (optBatch opts /= InteractiveRepl) $
         putStrLn "[warning] --command argument specified; ignoring batch file"
-      return (opts { optBatch = InteractiveBatch path }, Just path)
+      when (isJust (optProject opts)) $
+        putStrLn $
+          "[warning] --command argument specified; "
+          ++ "ignoring project configuration file"
+      return
+        ( opts { optBatch = InteractiveBatch path, optProject = Nothing }
+        , Just path )
+
+setupProject :: Options -> IO (Options, Maybe Project.Config)
+setupProject opts =
+  case optProject opts of
+    Nothing -> pure (opts, Nothing)
+    Just path -> do
+      when (optBatch opts /= InteractiveRepl) $
+        putStrLn "[warning] --project argument specified; ignoring batch file"
+      Project.loadConfig path >>= \case
+        Left err -> do
+          print $ pp err
+          exitFailure
+        Right config ->
+          pure (opts { optBatch = InteractiveRepl }, Just config)
 
 setupREPL :: Options -> REPL ()
 setupREPL opts = do
@@ -281,18 +324,20 @@ setupREPL opts = do
     Batch file -> prependSearchPath [ takeDirectory file ]
     _ -> return ()
 
-  case optLoad opts of
-    []  -> loadPrelude `REPL.catch` \x -> io $ print $ pp x
-    [l] -> void (loadCmd l) `REPL.catch` \x -> do
-             io $ print $ pp x
-             -- If the requested file fails to load, load the prelude instead...
-             loadPrelude `REPL.catch` \y -> do
-               io $ print $ pp y
-             -- ... but make sure the loaded module is set to the file
-             -- we tried, instead of the Prelude
-             REPL.setEditPath l
-             REPL.setLoadedMod REPL.LoadedModule
-               { REPL.lFocus = Nothing
-               , REPL.lPath = InFile l
-               }
-    _   -> io $ putStrLn "Only one file may be loaded at the command line."
+  when (isNothing (optProject opts)) $
+    case optLoad opts of
+      []  -> loadPrelude `REPL.catch` \x -> io $ print $ pp x
+      [l] -> void (loadCmd l) `REPL.catch` \x -> do
+              io $ print $ pp x
+              -- If the requested file fails to load,
+              -- load the prelude instead...
+              loadPrelude `REPL.catch` \y -> do
+                io $ print $ pp y
+              -- ... but make sure the loaded module is set to the file
+              -- we tried, instead of the Prelude
+              REPL.setEditPath l
+              REPL.setLoadedMod REPL.LoadedModule
+                { REPL.lFocus = Nothing
+                , REPL.lPath = InFile l
+                }
+      _   -> io $ putStrLn "Only one file may be loaded at the command line."