From 1f7cdb83c333d440e9cd8c7bee11c85729a54186 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 6 Jul 2023 15:41:42 -0400 Subject: [PATCH] add version command to cryptol-remote-api --- cryptol-remote-api/cryptol-remote-api.cabal | 1 + cryptol-remote-api/cryptol-remote-api/Main.hs | 5 ++ cryptol-remote-api/python/cryptol/commands.py | 12 ++++ .../python/cryptol/connection.py | 8 +++ .../python/cryptol/single_connection.py | 6 +- .../python/cryptol/synchronous.py | 20 +++++++ .../src/CryptolServer/Version.hs | 55 +++++++++++++++++++ src/Cryptol/Version.hs | 13 ++++- 8 files changed, 116 insertions(+), 4 deletions(-) create mode 100644 cryptol-remote-api/src/CryptolServer/Version.hs diff --git a/cryptol-remote-api/cryptol-remote-api.cabal b/cryptol-remote-api/cryptol-remote-api.cabal index ddebd8c7..97673b72 100644 --- a/cryptol-remote-api/cryptol-remote-api.cabal +++ b/cryptol-remote-api/cryptol-remote-api.cabal @@ -80,6 +80,7 @@ library CryptolServer.Names CryptolServer.Sat CryptolServer.TypeCheck + CryptolServer.Version CryptolServer.FileDeps other-modules: diff --git a/cryptol-remote-api/cryptol-remote-api/Main.hs b/cryptol-remote-api/cryptol-remote-api/Main.hs index 1008f594..e03e0d29 100644 --- a/cryptol-remote-api/cryptol-remote-api/Main.hs +++ b/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 diff --git a/cryptol-remote-api/python/cryptol/commands.py b/cryptol-remote-api/python/cryptol/commands.py index ca6aa029..318ee7b5 100644 --- a/cryptol-remote-api/python/cryptol/commands.py +++ b/cryptol-remote-api/python/cryptol/commands.py @@ -311,6 +311,18 @@ class CryptolFocusedModule(argo.Command): 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__( diff --git a/cryptol-remote-api/python/cryptol/connection.py b/cryptol-remote-api/python/cryptol/connection.py index 230f57a1..c17bf42d 100644 --- a/cryptol-remote-api/python/cryptol/connection.py +++ b/cryptol-remote-api/python/cryptol/connection.py @@ -421,6 +421,14 @@ class CryptolConnection: 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). diff --git a/cryptol-remote-api/python/cryptol/single_connection.py b/cryptol-remote-api/python/cryptol/single_connection.py index 016ec7a3..3538ec1e 100644 --- a/cryptol-remote-api/python/cryptol/single_connection.py +++ b/cryptol-remote-api/python/cryptol/single_connection.py @@ -11,7 +11,7 @@ from .quoting import * 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.""" diff --git a/cryptol-remote-api/python/cryptol/synchronous.py b/cryptol-remote-api/python/cryptol/synchronous.py index c886a39a..9cb7573e 100644 --- a/cryptol-remote-api/python/cryptol/synchronous.py +++ b/cryptol-remote-api/python/cryptol/synchronous.py @@ -78,6 +78,15 @@ class Unsatisfiable: def __nonzero__(self) -> Literal[False]: return False +@dataclass +class CryptolVersionInfo: + """Class containing version information about the Cryptol server.""" + version: str + commit_hash: str + commit_branch: str + commit_dirty: bool + ffi_enabled: bool + def connect(command : Optional[str]=None, *, @@ -377,6 +386,17 @@ class CryptolSyncConnection: """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( + 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.""" diff --git a/cryptol-remote-api/src/CryptolServer/Version.hs b/cryptol-remote-api/src/CryptolServer/Version.hs new file mode 100644 index 00000000..6dc10800 --- /dev/null +++ b/cryptol-remote-api/src/CryptolServer/Version.hs @@ -0,0 +1,55 @@ +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +module CryptolServer.Version + ( version + , versionDescr + , VersionParams(..) + ) where + +import qualified Argo.Doc as Doc +import Data.Aeson as JSON + +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 [ "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 = + [ ("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." + ]) + , ("commit branch", + Doc.Paragraph [ Doc.Text "The string of the git commit branch during the build." + ]) + , ("commit dirty", + Doc.Paragraph [ Doc.Text "True iff non-committed files were present during the build." + ]) + , ("FFI enabled", + Doc.Paragraph [ Doc.Text "True iff the FFI is enabled." + ]) + ] diff --git a/src/Cryptol/Version.hs b/src/Cryptol/Version.hs index 88c9da67..43433b79 100644 --- a/src/Cryptol/Version.hs +++ b/src/Cryptol/Version.hs @@ -13,6 +13,7 @@ module Cryptol.Version ( , commitShortHash , commitBranch , commitDirty + , ffiEnabled , version , displayVersion ) where @@ -33,15 +34,21 @@ 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 + if ffiEnabled then putLn "FFI enabled" + else return () where dirtyLab | commitDirty = " (non-committed files present during build)" | otherwise = ""