From 1f7cdb83c333d440e9cd8c7bee11c85729a54186 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 6 Jul 2023 15:41:42 -0400 Subject: [PATCH 1/7] 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 ddebd8c77..97673b728 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 1008f5947..e03e0d29f 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 ca6aa0292..318ee7b57 100644 --- a/cryptol-remote-api/python/cryptol/commands.py +++ b/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__( diff --git a/cryptol-remote-api/python/cryptol/connection.py b/cryptol-remote-api/python/cryptol/connection.py index 230f57a11..c17bf42da 100644 --- a/cryptol-remote-api/python/cryptol/connection.py +++ b/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). diff --git a/cryptol-remote-api/python/cryptol/single_connection.py b/cryptol-remote-api/python/cryptol/single_connection.py index 016ec7a39..3538ec1ef 100644 --- a/cryptol-remote-api/python/cryptol/single_connection.py +++ b/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.""" diff --git a/cryptol-remote-api/python/cryptol/synchronous.py b/cryptol-remote-api/python/cryptol/synchronous.py index c886a39a0..9cb7573eb 100644 --- a/cryptol-remote-api/python/cryptol/synchronous.py +++ b/cryptol-remote-api/python/cryptol/synchronous.py @@ -78,6 +78,15 @@ def __bool__(self) -> Literal[False]: 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 @@ 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( + 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 000000000..6dc108003 --- /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 88c9da67e..43433b79a 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 = "" From 39759bba06588f664c883d7b7cb1bc9c4b355a9d Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 6 Jul 2023 15:59:10 -0400 Subject: [PATCH 2/7] include cryptol-remote-api version in version command --- cryptol-remote-api/CHANGELOG.md | 5 ++++ cryptol-remote-api/cryptol-remote-api.cabal | 1 + .../python/cryptol/synchronous.py | 13 ++++++++++- .../src/CryptolServer/Version.hs | 23 +++++++++++-------- 4 files changed, 32 insertions(+), 10 deletions(-) diff --git a/cryptol-remote-api/CHANGELOG.md b/cryptol-remote-api/CHANGELOG.md index 0fde7f15f..334d693cb 100644 --- a/cryptol-remote-api/CHANGELOG.md +++ b/cryptol-remote-api/CHANGELOG.md @@ -1,5 +1,10 @@ # Revision history for `cryptol-remote-api` and `cryptol-eval-server` +## 3.0.1 -- YYYY-MM-DD + +* 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 diff --git a/cryptol-remote-api/cryptol-remote-api.cabal b/cryptol-remote-api/cryptol-remote-api.cabal index 97673b728..ded4a5807 100644 --- a/cryptol-remote-api/cryptol-remote-api.cabal +++ b/cryptol-remote-api/cryptol-remote-api.cabal @@ -85,6 +85,7 @@ library other-modules: CryptolServer.AesonCompat + Paths_cryptol_remote_api executable cryptol-remote-api import: deps, warnings, errors diff --git a/cryptol-remote-api/python/cryptol/synchronous.py b/cryptol-remote-api/python/cryptol/synchronous.py index 9cb7573eb..cc85729d6 100644 --- a/cryptol-remote-api/python/cryptol/synchronous.py +++ b/cryptol-remote-api/python/cryptol/synchronous.py @@ -80,7 +80,17 @@ def __nonzero__(self) -> Literal[False]: @dataclass class CryptolVersionInfo: - """Class containing version information about the Cryptol server.""" + """ + 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 @@ -390,6 +400,7 @@ 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'], diff --git a/cryptol-remote-api/src/CryptolServer/Version.hs b/cryptol-remote-api/src/CryptolServer/Version.hs index 6dc108003..30d9caed7 100644 --- a/cryptol-remote-api/src/CryptolServer/Version.hs +++ b/cryptol-remote-api/src/CryptolServer/Version.hs @@ -9,6 +9,7 @@ module CryptolServer.Version 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) @@ -21,11 +22,12 @@ versionDescr = 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 + 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 @@ -37,17 +39,20 @@ instance Doc.DescribedMethod VersionParams JSON.Value where parameterFieldDescription = [] resultFieldDescription = - [ ("version", + [ ("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." + 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." + 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." + 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." From d914b803ce75c77c557a8d2d9ba938afe0f96dd6 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 6 Jul 2023 16:44:19 -0400 Subject: [PATCH 3/7] update CHANGELOG for Python API --- cryptol-remote-api/python/CHANGELOG.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/cryptol-remote-api/python/CHANGELOG.md b/cryptol-remote-api/python/CHANGELOG.md index 1ff5c0561..c30594e97 100644 --- a/cryptol-remote-api/python/CHANGELOG.md +++ b/cryptol-remote-api/python/CHANGELOG.md @@ -1,5 +1,11 @@ # Revision history for `cryptol` Python package +## 3.0.1 -- YYYY-MM-DD + +* 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 From 9831dc8ddd5ddc52aa3215b3beb5ccb8e27cd58b Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 6 Jul 2023 16:57:20 -0400 Subject: [PATCH 4/7] update docs with version command --- cryptol-remote-api/docs/Cryptol.rst | 46 +++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/cryptol-remote-api/docs/Cryptol.rst b/cryptol-remote-api/docs/Cryptol.rst index fab75c3b1..d8fe93a44 100644 --- a/cryptol-remote-api/docs/Cryptol.rst +++ b/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) ~~~~~~~~~~~~~~~ From a5366b97ffa802a40e0c574aebd34e11cd4c2020 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Mon, 10 Jul 2023 13:08:03 -0400 Subject: [PATCH 5/7] use when function in Version.hs --- src/Cryptol/Version.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Cryptol/Version.hs b/src/Cryptol/Version.hs index 43433b79a..8c20ef99d 100644 --- a/src/Cryptol/Version.hs +++ b/src/Cryptol/Version.hs @@ -21,6 +21,7 @@ module Cryptol.Version ( import Paths_cryptol import qualified GitRev import Data.Version (showVersion) +import Control.Monad (when) commitHash :: String commitHash = GitRev.hash @@ -47,8 +48,7 @@ displayVersion putLn = do putLn ("Cryptol " ++ ver) putLn ("Git commit " ++ commitHash) putLn (" branch " ++ commitBranch ++ dirtyLab) - if ffiEnabled then putLn "FFI enabled" - else return () + when ffiEnabled $ putLn "FFI enabled" where dirtyLab | commitDirty = " (non-committed files present during build)" | otherwise = "" From 75d00d9dfcb14021eecbe0a2fe120c32195a33d4 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Mon, 10 Jul 2023 13:20:17 -0400 Subject: [PATCH 6/7] Bump cryptol-remote-api versions to 3.0.1 --- cryptol-remote-api/CHANGELOG.md | 6 +++++- cryptol-remote-api/cryptol-remote-api.cabal | 2 +- cryptol-remote-api/python/CHANGELOG.md | 6 +++++- cryptol-remote-api/python/pyproject.toml | 2 +- 4 files changed, 12 insertions(+), 4 deletions(-) diff --git a/cryptol-remote-api/CHANGELOG.md b/cryptol-remote-api/CHANGELOG.md index 334d693cb..af06812f9 100644 --- a/cryptol-remote-api/CHANGELOG.md +++ b/cryptol-remote-api/CHANGELOG.md @@ -1,6 +1,10 @@ # Revision history for `cryptol-remote-api` and `cryptol-eval-server` -## 3.0.1 -- YYYY-MM-DD +## 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 diff --git a/cryptol-remote-api/cryptol-remote-api.cabal b/cryptol-remote-api/cryptol-remote-api.cabal index ded4a5807..3f017361e 100644 --- a/cryptol-remote-api/cryptol-remote-api.cabal +++ b/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 license: BSD-3-Clause license-file: LICENSE author: Galois, Inc. diff --git a/cryptol-remote-api/python/CHANGELOG.md b/cryptol-remote-api/python/CHANGELOG.md index c30594e97..5953664b3 100644 --- a/cryptol-remote-api/python/CHANGELOG.md +++ b/cryptol-remote-api/python/CHANGELOG.md @@ -1,6 +1,10 @@ # Revision history for `cryptol` Python package -## 3.0.1 -- YYYY-MM-DD +## 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 diff --git a/cryptol-remote-api/python/pyproject.toml b/cryptol-remote-api/python/pyproject.toml index a9505521f..db2ccaaca 100644 --- a/cryptol-remote-api/python/pyproject.toml +++ b/cryptol-remote-api/python/pyproject.toml @@ -1,6 +1,6 @@ [tool.poetry] name = "cryptol" -version = "3.0.0.99" +version = "3.0.1" readme = "README.md" keywords = ["cryptography", "verification"] description = "Cryptol client for the Cryptol 2.13 RPC server" From 9e86c0fa258d7dd72fe31bc9eb62f07d038a8253 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Mon, 10 Jul 2023 13:28:32 -0400 Subject: [PATCH 7/7] Bump cryptol-remote-api versions to 3.0.1.99 development version --- cryptol-remote-api/cryptol-remote-api.cabal | 2 +- cryptol-remote-api/python/pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/cryptol-remote-api/cryptol-remote-api.cabal b/cryptol-remote-api/cryptol-remote-api.cabal index 3f017361e..19dfeab2c 100644 --- a/cryptol-remote-api/cryptol-remote-api.cabal +++ b/cryptol-remote-api/cryptol-remote-api.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: cryptol-remote-api -version: 3.0.1 +version: 3.0.1.99 license: BSD-3-Clause license-file: LICENSE author: Galois, Inc. diff --git a/cryptol-remote-api/python/pyproject.toml b/cryptol-remote-api/python/pyproject.toml index db2ccaaca..366048c87 100644 --- a/cryptol-remote-api/python/pyproject.toml +++ b/cryptol-remote-api/python/pyproject.toml @@ -1,6 +1,6 @@ [tool.poetry] name = "cryptol" -version = "3.0.1" +version = "3.0.1.99" readme = "README.md" keywords = ["cryptography", "verification"] description = "Cryptol client for the Cryptol 2.13 RPC server"