feat: timeout for cryptol python client methods (#1282)

interrupt and timeout methods for cryptol python client

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

@@ -22,6 +22,8 @@ import CryptolServer.Check ( check, checkDescr )
 import CryptolServer.ClearState
     ( clearState, clearStateDescr, clearAllStates, clearAllStatesDescr)
 import Cryptol.Eval (EvalOpts(..), defaultPPOpts)
+import CryptolServer.Interrupt
+    ( interruptServer, interruptServerDescr )
 import Cryptol.ModuleSystem (ModuleInput(..), loadModuleByPath, loadModuleByName)
 import Cryptol.ModuleSystem.Monad (runModuleM, setFocusedModule)
 import Cryptol.TypeCheck.AST (mName)
@@ -166,4 +168,8 @@ cryptolEvalMethods =
     "clear all states"
     clearAllStatesDescr
     clearAllStates
+  , notification
+     "interrupt"
+     interruptServerDescr
+     interruptServer
   ]

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

@@ -74,6 +74,7 @@ library
     CryptolServer.ExtendSearchPath
     CryptolServer.Exceptions
     CryptolServer.FocusedModule
+    CryptolServer.Interrupt
     CryptolServer.LoadModule
     CryptolServer.Options
     CryptolServer.Names

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

@@ -26,6 +26,8 @@ import CryptolServer.ExtendSearchPath
     ( extSearchPath, extSearchPathDescr )
 import CryptolServer.FocusedModule
     ( focusedModule, focusedModuleDescr )
+import CryptolServer.Interrupt
+    ( interruptServer, interruptServerDescr )
 import CryptolServer.LoadModule
     ( loadFile, loadFileDescr, loadModule, loadModuleDescr )
 import CryptolServer.Names ( visibleNames, visibleNamesDescr )
@@ -113,4 +115,8 @@ cryptolMethods =
      "prove or satisfy"
      proveSatDescr
      proveSat
+  , notification
+     "interrupt"
+     interruptServerDescr
+     interruptServer
   ]

cryptol-remote-api/docs/Cryptol.rst

@@ -611,6 +611,24 @@ Return fields
 
 
 
+interrupt (notification)
+~~~~~~~~~~~~~~~~~~~~~~~~
+
+Interrupt the server, terminating it's current task (if one exists).
+
+Parameter fields
+++++++++++++++++
+
+No parameters
+
+
+Return fields
++++++++++++++
+
+No return fields
+
+
+
 
 
 

cryptol-remote-api/python/CHANGELOG.md

@@ -1,5 +1,14 @@
 # Revision history for `cryptol` Python package
 
+## 2.11.6 -- 2021-09-10
+
+* Add a `timeout` field to the `CryptolConnection` class which can be used
+  to set a default timeout for all RPC interactions.
+* Add an optional `timeout` keyword parameter to each `CryptolConnection` method
+  which can specify a timeout for a particular method call.
+* Add an `interrupt` method to the `CryptolConnection` class which interrupts
+  any active requests on the server.
+
 ## 2.11.5 -- 2021-08-25
 
 * From argo: Change the behavior of the `Command` `state` method so that after

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

@@ -62,33 +62,34 @@ def from_cryptol_arg(val : Any) -> CryptolValue:
 
 
 class CryptolLoadModule(argo.Command):
-    def __init__(self, connection : HasProtocolState, mod_name : str) -> None:
-        super(CryptolLoadModule, self).__init__('load module', {'module name': mod_name}, connection)
+    def __init__(self, connection : HasProtocolState, mod_name : str, timeout: Optional[float]) -> None:
+        super(CryptolLoadModule, self).__init__('load module', {'module name': mod_name}, connection, timeout=timeout)
 
     def process_result(self, res : Any) -> Any:
         return res
 
 class CryptolLoadFile(argo.Command):
-    def __init__(self, connection : HasProtocolState, filename : str) -> None:
-        super(CryptolLoadFile, self).__init__('load file', {'file': filename}, connection)
+    def __init__(self, connection : HasProtocolState, filename : str, timeout: Optional[float]) -> None:
+        super(CryptolLoadFile, self).__init__('load file', {'file': filename}, connection, timeout=timeout)
 
     def process_result(self, res : Any) -> Any:
         return res
 
 class CryptolExtendSearchPath(argo.Command):
-    def __init__(self, connection : HasProtocolState, dirs : List[str]) -> None:
-        super(CryptolExtendSearchPath, self).__init__('extend search path', {'paths': dirs}, connection)
+    def __init__(self, connection : HasProtocolState, dirs : List[str], timeout: Optional[float]) -> None:
+        super(CryptolExtendSearchPath, self).__init__('extend search path', {'paths': dirs}, connection, timeout=timeout)
 
     def process_result(self, res : Any) -> Any:
         return res
 
 
 class CryptolEvalExprRaw(argo.Command):
-    def __init__(self, connection : HasProtocolState, expr : Any) -> None:
+    def __init__(self, connection : HasProtocolState, expr : Any, timeout: Optional[float]) -> None:
         super(CryptolEvalExprRaw, self).__init__(
             'evaluate expression',
             {'expression': expr},
-            connection
+            connection,
+            timeout=timeout
         )
 
     def process_result(self, res : Any) -> Any:
@@ -100,11 +101,12 @@ def process_result(self, res : Any) -> Any:
 
 
 class CryptolCallRaw(argo.Command):
-    def __init__(self, connection : HasProtocolState, fun : str, args : List[Any]) -> None:
+    def __init__(self, connection : HasProtocolState, fun : str, args : List[Any], timeout: Optional[float]) -> None:
         super(CryptolCallRaw, self).__init__(
             'call',
             {'function': fun, 'arguments': args},
-            connection
+            connection,
+            timeout=timeout
         )
 
     def process_result(self, res : Any) -> Any:
@@ -153,15 +155,19 @@ def to_check_report(res : Any) -> CheckReport:
         raise ValueError("Unknown check result " + str(res))
 
 class CryptolCheckRaw(argo.Command):
-    def __init__(self, connection : HasProtocolState, expr : Any, num_tests : Union[Literal['all'],int, None]) -> None:
+    def __init__(self, connection : HasProtocolState,
+                 expr : Any,
+                 num_tests : Union[Literal['all'],int, None],
+                 timeout: Optional[float]) -> None:
         if num_tests:
             args = {'expression': expr, 'number of tests':num_tests}
         else:
             args = {'expression': expr}
         super(CryptolCheckRaw, self).__init__(
             'check',
             args,
-            connection
+            connection,
+            timeout=timeout
         )
 
     def process_result(self, res : Any) -> Any:
@@ -173,11 +179,12 @@ def process_result(self, res : Any) -> 'CheckReport':
 
 
 class CryptolCheckType(argo.Command):
-    def __init__(self, connection : HasProtocolState, expr : Any) -> None:
+    def __init__(self, connection : HasProtocolState, expr : Any, timeout: Optional[float]) -> None:
         super(CryptolCheckType, self).__init__(
             'check type',
             {'expression': expr},
-            connection
+            connection,
+            timeout=timeout
         )
 
     def process_result(self, res : Any) -> Any:
@@ -190,15 +197,22 @@ class SmtQueryType(str, Enum):
     SAT   = 'sat'
 
 class CryptolProveSatRaw(argo.Command):
-    def __init__(self, connection : HasProtocolState, qtype : SmtQueryType, expr : Any, solver : Solver, count : Optional[int]) -> None:
+    def __init__(self,
+                 connection : HasProtocolState,
+                 qtype : SmtQueryType,
+                 expr : Any,
+                 solver : Solver,
+                 count : Optional[int],
+                 timeout: Optional[float]) -> None:
         super(CryptolProveSatRaw, self).__init__(
             'prove or satisfy',
             {'query type': qtype,
              'expression': expr,
              'prover': solver.name(),
              'hash consing': "true" if solver.hash_consing() else "false",
              'result count': 'all' if count is None else count},
-            connection
+            connection,
+            timeout=timeout
         )
         self.qtype = qtype
 
@@ -228,41 +242,42 @@ def process_result(self, res : Any) -> Any:
             raise ValueError("Unknown SMT result: " + str(res))
 
 class CryptolProveRaw(CryptolProveSatRaw):
-    def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver) -> None:
-        super(CryptolProveRaw, self).__init__(connection, SmtQueryType.PROVE, expr, solver, 1)
+    def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, timeout: Optional[float]) -> None:
+        super(CryptolProveRaw, self).__init__(connection, SmtQueryType.PROVE, expr, solver, 1, timeout)
 class CryptolProve(CryptolProveSat):
-    def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver) -> None:
-        super(CryptolProve, self).__init__(connection, SmtQueryType.PROVE, expr, solver, 1)
+    def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, timeout: Optional[float]) -> None:
+        super(CryptolProve, self).__init__(connection, SmtQueryType.PROVE, expr, solver, 1, timeout=timeout)
 
 class CryptolSatRaw(CryptolProveSatRaw):
-    def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, count : int) -> None:
-        super(CryptolSatRaw, self).__init__(connection, SmtQueryType.SAT, expr, solver, count)
+    def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, count : int, timeout: Optional[float]) -> None:
+        super(CryptolSatRaw, self).__init__(connection, SmtQueryType.SAT, expr, solver, count, timeout=timeout)
 class CryptolSat(CryptolProveSat):
-    def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, count : int) -> None:
-        super(CryptolSat, self).__init__(connection, SmtQueryType.SAT, expr, solver, count)
+    def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, count : int, timeout: Optional[float]) -> None:
+        super(CryptolSat, self).__init__(connection, SmtQueryType.SAT, expr, solver, count, timeout=timeout)
 
 class CryptolSafeRaw(CryptolProveSatRaw):
-    def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver) -> None:
-        super(CryptolSafeRaw, self).__init__(connection, SmtQueryType.SAFE, expr, solver, 1)
+    def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, timeout: Optional[float]) -> None:
+        super(CryptolSafeRaw, self).__init__(connection, SmtQueryType.SAFE, expr, solver, 1, timeout=timeout)
 class CryptolSafe(CryptolProveSat):
-    def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver) -> None:
-        super(CryptolSafe, self).__init__(connection, SmtQueryType.SAFE, expr, solver, 1)
+    def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, timeout: Optional[float]) -> None:
+        super(CryptolSafe, self).__init__(connection, SmtQueryType.SAFE, expr, solver, 1, timeout=timeout)
 
 
 class CryptolNames(argo.Command):
-    def __init__(self, connection : HasProtocolState) -> None:
-        super(CryptolNames, self).__init__('visible names', {}, connection)
+    def __init__(self, connection : HasProtocolState, timeout: Optional[float]) -> None:
+        super(CryptolNames, self).__init__('visible names', {}, connection, timeout=timeout)
 
     def process_result(self, res : Any) -> Any:
         return res
 
 
 class CryptolFocusedModule(argo.Command):
-    def __init__(self, connection : HasProtocolState) -> None:
+    def __init__(self, connection : HasProtocolState, timeout: Optional[float]) -> None:
         super(CryptolFocusedModule, self).__init__(
             'focused module',
             {},
-            connection
+            connection,
+            timeout=timeout
         )
 
     def process_result(self, res : Any) -> Any:
@@ -285,3 +300,11 @@ def __init__(self, connection : HasProtocolState) -> None:
             {},
             connection
         )
+
+class CryptolInterrupt(argo.Notification):
+    def __init__(self, connection : HasProtocolState) -> None:
+        super(CryptolInterrupt, self).__init__(
+            'interrupt',
+            {},
+            connection
+        )