mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-21 19:08:51 +03:00
Merge pull request #1547 from GaloisInc/version-python-cmd
Add `version` command to cryptol-remote-api
This commit is contained in:
commit
2064a38b8c
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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)
|
||||
~~~~~~~~~~~~~~~
|
||||
|
||||
|
@ -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
|
||||
|
@ -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__(
|
||||
|
@ -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).
|
||||
|
||||
|
@ -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."""
|
||||
|
@ -78,6 +78,25 @@ class Unsatisfiable:
|
||||
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 @@ 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(
|
||||
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."""
|
||||
|
@ -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"
|
||||
|
60
cryptol-remote-api/src/CryptolServer/Version.hs
Normal file
60
cryptol-remote-api/src/CryptolServer/Version.hs
Normal file
@ -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."
|
||||
])
|
||||
]
|
@ -13,6 +13,7 @@ module Cryptol.Version (
|
||||
, commitShortHash
|
||||
, commitBranch
|
||||
, commitDirty
|
||||
, ffiEnabled
|
||||
, version
|
||||
, displayVersion
|
||||
) where
|
||||
@ -20,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
|
||||
@ -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 = ""
|
||||
|
Loading…
Reference in New Issue
Block a user