feat: timeout for cryptol python client methods

cryptol-remote-api/python/CHANGELOG.md

@@ -1,5 +1,12 @@
 # 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. Also add an optional
+  `timeout` keyword parameter to each `CryptolConnection` method which can
+  specify a timeout for a particular method call.
+
 ## 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

@@ -59,44 +59,46 @@ def from_cryptol_arg(val : Any) -> Any:
 
 
 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 CryptolEvalExpr(argo.Command):
-    def __init__(self, connection : HasProtocolState, expr : Any) -> None:
+    def __init__(self, connection : HasProtocolState, expr : Any, timeout: Optional[float]) -> None:
         super(CryptolEvalExpr, self).__init__(
             'evaluate expression',
             {'expression': expr},
-            connection
+            connection,
+            timeout=timeout
         )
 
     def process_result(self, res : Any) -> Any:
         return from_cryptol_arg(res['value'])
 
 class CryptolCall(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(CryptolCall, self).__init__(
             'call',
             {'function': fun, 'arguments': args},
-            connection
+            connection,
+            timeout=timeout
         )
 
     def process_result(self, res : Any) -> Any:
@@ -113,15 +115,19 @@ class CheckReport:
     tests_possible: Optional[int]
 
 class CryptolCheck(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(CryptolCheck, self).__init__(
             'check',
             args,
-            connection
+            connection,
+            timeout=timeout
         )
 
     def process_result(self, res : Any) -> 'CheckReport':
@@ -151,11 +157,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:
@@ -167,15 +174,22 @@ class SmtQueryType(str, Enum):
     SAT   = 'sat'
 
 class CryptolProveSat(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(CryptolProveSat, 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
 
@@ -200,30 +214,31 @@ def process_result(self, res : Any) -> Any:
             raise ValueError("Unknown SMT result: " + str(res))
 
 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 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 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: