Merge pull request #1547 from GaloisInc/version-python-cmd

Add `version` command to cryptol-remote-api

cryptol-remote-api/CHANGELOG.md

@@ -1,5 +1,14 @@
 # Revision history for `cryptol-remote-api` and `cryptol-eval-server`
 
+## 3.0.2 -- YYYY-MM-DD
+
+*  NEW CHANGELOG ENTRIES SINCE 3.0.1 GO HERE
+
+## 3.0.1 -- 2023-07-10
+
+* Add `version` command for fetching Cryptol/`cryptol-remote-api` version
+  information
+
 ## 3.0.0 -- 2023-06-26
 
 * The v3.0.0 release is made in tandem with the Cryptol 3.0.0 release. See the

cryptol-remote-api/cryptol-remote-api.cabal

@@ -1,6 +1,6 @@
 cabal-version:       2.4
 name:                cryptol-remote-api
-version:             3.0.0.99
+version:             3.0.1.99
 license:             BSD-3-Clause
 license-file:        LICENSE
 author:              Galois, Inc.
@@ -80,10 +80,12 @@ library
     CryptolServer.Names
     CryptolServer.Sat
     CryptolServer.TypeCheck
+    CryptolServer.Version
     CryptolServer.FileDeps
 
   other-modules:
     CryptolServer.AesonCompat
+    Paths_cryptol_remote_api
 
 executable cryptol-remote-api
   import:              deps, warnings, errors

cryptol-remote-api/cryptol-remote-api/Main.hs

@@ -33,6 +33,7 @@ import CryptolServer.LoadModule
 import CryptolServer.Names ( visibleNames, visibleNamesDescr )
 import CryptolServer.Sat ( proveSat, proveSatDescr )
 import CryptolServer.TypeCheck ( checkType, checkTypeDescr )
+import CryptolServer.Version ( version, versionDescr )
 import CryptolServer.FileDeps( fileDeps, fileDepsDescr )
 
 main :: IO ()
@@ -69,6 +70,10 @@ getSearchPaths =
 cryptolMethods :: [AppMethod ServerState]
 cryptolMethods =
   [ command
+    "version"
+    versionDescr
+    version
+  , command
     "check"
     checkDescr
     check

cryptol-remote-api/docs/Cryptol.rst

@@ -237,6 +237,52 @@ JSON representations of types are type schemas. A type schema has three fields:
 Methods
 -------
 
+version (command)
+~~~~~~~~~~~~~~~~~
+
+Version information about this Cryptol server.
+
+Parameter fields
+++++++++++++++++
+
+No parameters
+
+
+Return fields
++++++++++++++
+
+
+``RPC server version``
+  The cryptol-remote-api version string.
+
+
+
+``version``
+  The Cryptol version string.
+
+
+
+``commit hash``
+  The string of the git commit hash during the build of Cryptol.
+
+
+
+``commit branch``
+  The string of the git commit branch during the build of Cryptol.
+
+
+
+``commit dirty``
+  True iff non-committed files were present during the build of Cryptol.
+
+
+
+``FFI enabled``
+  True iff the FFI is enabled.
+
+
+
+
 check (command)
 ~~~~~~~~~~~~~~~
 

cryptol-remote-api/python/CHANGELOG.md

@@ -1,5 +1,15 @@
 # Revision history for `cryptol` Python package
 
+## 3.0.2 -- YYYY-MM-DD
+
+*  NEW CHANGELOG ENTRIES SINCE 3.0.1 GO HERE
+
+## 3.0.1 -- 2023-07-10
+
+* Update `cry_f` to property handle strings, length-0 `BV`s, and 1-tuples
+* Add `version` command for fetching Cryptol/`cryptol-remote-api` version
+  information
+
 ## 3.0.0 -- 2023-06-26
 
 * The v3.0.0 release is made in tandem with the Cryptol 3.0.0 release. See the

cryptol-remote-api/python/cryptol/commands.py

@@ -311,6 +311,18 @@ def process_result(self, res : Any) -> Any:
         return res
 
 
+class CryptolVersion(argo.Command):
+    def __init__(self, connection : HasProtocolState, timeout: Optional[float]) -> None:
+        super(CryptolVersion, self).__init__(
+            'version',
+            {},
+            connection,
+            timeout=timeout)
+
+    def process_result(self, res : Any) -> Any:
+        return res
+
+
 class CryptolReset(argo.Notification):
     def __init__(self, connection : HasProtocolState) -> None:
         super(CryptolReset, self).__init__(

cryptol-remote-api/python/cryptol/connection.py

@@ -421,6 +421,14 @@ def focused_module(self, *, timeout:Optional[float] = None) -> argo.Command:
         self.most_recent_result = CryptolFocusedModule(self, timeout)
         return self.most_recent_result
 
+    def version(self, *, timeout:Optional[float] = None) -> argo.Command:
+        """Returns version information about the Cryptol server.
+
+        :param timeout: Optional timeout for this request (in seconds)."""
+        timeout = timeout if timeout is not None else self.timeout
+        self.most_recent_result = CryptolVersion(self, timeout)
+        return self.most_recent_result
+
     def reset(self) -> None:
         """Resets the connection, causing its unique state on the server to be freed (if applicable).
 

cryptol-remote-api/python/cryptol/single_connection.py

@@ -11,7 +11,7 @@
 from .solver import OfflineSmtQuery, Solver, OnlineSolver, OfflineSolver, Z3
 from .connection import CryptolValue, CheckReport
 from . import synchronous
-from .synchronous import Qed, Safe, Counterexample, Satisfiable, Unsatisfiable
+from .synchronous import Qed, Safe, Counterexample, Satisfiable, Unsatisfiable, CryptolVersionInfo
 from . import cryptoltypes
 
 
@@ -236,6 +236,10 @@ def focused_module(*, timeout:Optional[float] = None) -> cryptoltypes.CryptolMod
     """Returns the name and other information about the currently-focused module."""
     return __get_designated_connection().focused_module(timeout=timeout)
 
+def version(*, timeout:Optional[float] = None) -> CryptolVersionInfo:
+    """Returns version information about the Cryptol server."""
+    return __get_designated_connection().version(timeout=timeout)
+
 def reset() -> None:
     """Resets the connection, causing its unique state on the server to be freed (if applicable).
     After a reset a connection may be treated as if it were a fresh connection with the server if desired."""

cryptol-remote-api/python/cryptol/synchronous.py

@@ -78,6 +78,25 @@ def __bool__(self) -> Literal[False]:
     def __nonzero__(self) -> Literal[False]:
         return False
 
+@dataclass
+class CryptolVersionInfo:
+    """
+    Class containing version information about the Cryptol server.
+
+    :param rpc_version: The cryptol-remote-api version string.
+    :param version: The Cryptol version string.
+    :param commit_hash: The string of the git commit hash during the build of Cryptol.
+    :param commit_branch: The string of the git commit branch during the build of Cryptol.
+    :param commit_dirty: True iff non-committed files were present during the build of Cryptol.
+    :param ffi_enabled: True iff the FFI is enabled.
+    """
+    rpc_version: str
+    version: str
+    commit_hash: str
+    commit_branch: str
+    commit_dirty: bool
+    ffi_enabled: bool 
+
 
 def connect(command : Optional[str]=None,
             *,
@@ -377,6 +396,18 @@ def focused_module(self, *, timeout:Optional[float] = None) -> cryptoltypes.Cryp
         """Returns the name and other information about the currently-focused module."""
         return cryptoltypes.to_cryptol_module_info(self.connection.focused_module(timeout=timeout).result())
 
+    def version(self, *, timeout:Optional[float] = None) -> CryptolVersionInfo:
+        """Returns version information about the Cryptol server."""
+        res = self.connection.version(timeout=timeout).result()
+        return CryptolVersionInfo(
+                rpc_version   = res['RPC server version'],
+                version       = res['version'],
+                commit_hash   = res['commit hash'],
+                commit_branch = res['commit branch'],
+                commit_dirty  = res['commit dirty'],
+                ffi_enabled   = res['FFI enabled']
+                )
+
     def reset(self) -> None:
         """Resets the connection, causing its unique state on the server to be freed (if applicable).
         After a reset a connection may be treated as if it were a fresh connection with the server if desired."""

cryptol-remote-api/python/pyproject.toml

@@ -1,6 +1,6 @@
 [tool.poetry]
 name = "cryptol"
-version = "3.0.0.99"
+version = "3.0.1.99"
 readme = "README.md"
 keywords = ["cryptography", "verification"]
 description = "Cryptol client for the Cryptol RPC server"

cryptol-remote-api/src/CryptolServer/Version.hs

@@ -0,0 +1,60 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
+module CryptolServer.Version
+  ( version
+  , versionDescr
+  , VersionParams(..)
+  ) where
+
+import qualified Argo.Doc as Doc
+import Data.Aeson as JSON
+
+import qualified Paths_cryptol_remote_api as RPC
+import qualified Cryptol.Version as Cry
+import Data.Version (showVersion)
+
+import CryptolServer
+
+versionDescr :: Doc.Block
+versionDescr =
+  Doc.Paragraph
+    [Doc.Text "Version information about this Cryptol server."]
+
+version :: VersionParams -> CryptolCommand JSON.Value
+version _ =
+  return $ JSON.object [ "RPC server version" .= showVersion RPC.version
+                       , "version"            .= showVersion Cry.version
+                       , "commit hash"        .= Cry.commitHash
+                       , "commit branch"      .= Cry.commitBranch
+                       , "commit dirty"       .= Cry.commitDirty
+                       , "FFI enabled"        .= Cry.ffiEnabled
+                       ]
+
+data VersionParams = VersionParams
+
+instance JSON.FromJSON VersionParams where
+  parseJSON _ = pure VersionParams
+
+instance Doc.DescribedMethod VersionParams JSON.Value where
+  parameterFieldDescription = []
+
+  resultFieldDescription =
+    [ ("RPC server version",
+      Doc.Paragraph [ Doc.Text "The cryptol-remote-api version string."
+                    ])
+    , ("version",
+      Doc.Paragraph [ Doc.Text "The Cryptol version string."
+                    ])
+    , ("commit hash",
+      Doc.Paragraph [ Doc.Text "The string of the git commit hash during the build of Cryptol."
+                    ])
+    , ("commit branch",
+      Doc.Paragraph [ Doc.Text "The string of the git commit branch during the build of Cryptol."
+                    ])
+    , ("commit dirty",
+      Doc.Paragraph [ Doc.Text "True iff non-committed files were present during the build of Cryptol."
+                    ])
+    , ("FFI enabled",
+      Doc.Paragraph [ Doc.Text "True iff the FFI is enabled."
+                    ])
+    ]

src/Cryptol/Version.hs

@@ -13,13 +13,15 @@ module Cryptol.Version (
   , commitShortHash
   , commitBranch
   , commitDirty
+  , ffiEnabled
   , version
   , displayVersion
   ) where
 
 import Paths_cryptol
 import qualified GitRev
 import Data.Version (showVersion)
+import Control.Monad (when)
 
 commitHash :: String
 commitHash = GitRev.hash
@@ -33,15 +35,20 @@ commitBranch = GitRev.branch
 commitDirty :: Bool
 commitDirty = GitRev.dirty
 
+ffiEnabled :: Bool
+#ifdef FFI_ENABLED
+ffiEnabled = True
+#else
+ffiEnabled = False
+#endif
+
 displayVersion :: Monad m => (String -> m ()) -> m ()
 displayVersion putLn = do
     let ver = showVersion version
     putLn ("Cryptol " ++ ver)
     putLn ("Git commit " ++ commitHash)
     putLn ("    branch " ++ commitBranch ++ dirtyLab)
-#ifdef FFI_ENABLED
-    putLn "FFI enabled"
-#endif
+    when ffiEnabled $ putLn "FFI enabled"
       where
       dirtyLab | commitDirty = " (non-committed files present during build)"
                | otherwise   = ""