Skip to content

Commit

Permalink
feat(rpc): make python client compat with python 3.7
Browse files Browse the repository at this point in the history
  • Loading branch information
Andrew Kent committed May 7, 2021
1 parent ac4500a commit a65e776
Show file tree
Hide file tree
Showing 15 changed files with 159 additions and 247 deletions.
13 changes: 11 additions & 2 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,11 @@ jobs:

- uses: actions/setup-python@v2
with:
python-version: '3.x'
python-version: '3.7'

- uses: abatilo/actions-poetry@v2.0.0
with:
poetry-version: 1.1.6

- uses: actions/setup-haskell@v1
id: setup-haskell
Expand Down Expand Up @@ -300,7 +304,12 @@ jobs:
- if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api'
uses: actions/setup-python@v2
with:
python-version: '3.x'
python-version: '3.7'

- if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api'
uses: abatilo/actions-poetry@v2.0.0
with:
poetry-version: 1.1.6

- if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api'
name: Test cryptol-remote-api
Expand Down
4 changes: 2 additions & 2 deletions cryptol-remote-api/python/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ $ docker run --name=cryptol-remote-api -d \
ghcr.io/galoisinc/cryptol-remote-api:nightly-portable
$ export CRYPTOL_SERVER_URL="http://localhost:8080/"
```
6. Install the Python client (requires Python v3.8 or newer -- we recommend using [`poetry`](https://python-poetry.org/docs/#installation) to install the package):
6. Install the Python client (requires Python v3.7 or newer -- we recommend using [`poetry`](https://python-poetry.org/docs/#installation) to install the package):
```
$ poetry install
```
Expand Down Expand Up @@ -151,7 +151,7 @@ configured properly) should then appear as `cryptol-remote-api` in a user's `PAT
# Running Python Cryptol scripts

Once the server is setup and any path variables are setup as desired, the
Python (>= v3.8) client can be installed using
Python (>= v3.7) client can be installed using
[`poetry`](https://python-poetry.org/docs/#installation) as follows:

```
Expand Down
10 changes: 7 additions & 3 deletions cryptol-remote-api/python/cryptol/bitvector.py
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,7 @@ def concat(self, *others : 'BV') -> 'BV':
``others`` in order on the right.
"""
return reduce(lambda acc, b: acc.__concat_single(b), others, self)

@staticmethod
def join(*bs : 'BV') -> 'BV':
"""Concatenate the given ``BV``s in order.
Expand Down Expand Up @@ -178,6 +178,10 @@ def __index__(self) -> int:
"""Equivalent to ``self.value()``."""
return self.__value

def __int__(self) -> int:
"""Equivalent to ``self.value()``."""
return self.__value

def __len__(self) -> int:
"""Equivalent to ``self.size()``."""
return self.__size
Expand All @@ -190,7 +194,7 @@ def __bytes__(self) -> bytes:

def split(self, size : int) -> List['BV']:
"""Split ``self`` into a list of ``BV``s of length ``size``.
:param size: Size of segments to partition ``self`` into (must evently divide ``self.size()``).
"""
if not isinstance(size, int) or size <= 0:
Expand All @@ -209,7 +213,7 @@ def popcount(self) -> int:
@staticmethod
def from_bytes(bs : bytes, *, size : Optional[int] =None, byteorder : str ='big') -> 'BV':
"""Convert the given bytes ``bs`` into a ``BV``.
:param bs: Bytes to convert to a ``BV``.
:param size, optional: Desired ``BV``'s size (must be large enough to represent ``bs``). The
default (i.e., ``None``) will result in a ``BV`` of size ``len(bs) * 8``.
Expand Down
37 changes: 26 additions & 11 deletions cryptol-remote-api/python/cryptol/connection.py
Original file line number Diff line number Diff line change
Expand Up @@ -51,24 +51,39 @@ def connect(command : Optional[str]=None,
if url is not None:
raise ValueError("A Cryptol server URL cannot be specified with a command currently.")
c = CryptolConnection(command, cryptol_path)
elif url is not None:
# User-passed url?
if c is None and url is not None:
c = CryptolConnection(ServerConnection(HttpProcess(url)), cryptol_path)
elif (command := os.getenv('CRYPTOL_SERVER')) is not None and (command := find_executable(command)) is not None:
c = CryptolConnection(command+" socket", cryptol_path=cryptol_path)
elif (url := os.getenv('CRYPTOL_SERVER_URL')) is not None:
c = CryptolConnection(ServerConnection(HttpProcess(url)), cryptol_path)
elif (command := find_executable('cryptol-remote-api')) is not None:
c = CryptolConnection(command+" socket", cryptol_path=cryptol_path)
# Check `CRYPTOL_SERVER` env var if no connection identified yet
if c is None:
command = os.getenv('CRYPTOL_SERVER')
if command is not None:
command = find_executable(command)
if command is not None:
c = CryptolConnection(command+" socket", cryptol_path=cryptol_path)
# Check `CRYPTOL_SERVER_URL` env var if no connection identified yet
if c is None:
url = os.getenv('CRYPTOL_SERVER_URL')
if url is not None:
c = CryptolConnection(ServerConnection(HttpProcess(url)), cryptol_path)
# Check if `cryptol-remote-api` is in the PATH if no connection identified yet
if c is None:
command = find_executable('cryptol-remote-api')
if command is not None:
c = CryptolConnection(command+" socket", cryptol_path=cryptol_path)
# Raise an error if still no connection identified yet
if c is not None:
if reset_server:
CryptolResetServer(c)
return c
else:
raise ValueError(
"""cryptol.connect requires one of the following:",
1) a command to launch a cryptol server is the first positional argument,
2) a URL to connect to a running cryptol server is provided via the `url` keyword argument,
3) the environment variable `CRYPTOL_SERVER` must refer to a valid server executable, or
4) the environment variable `CRYPTOL_SERVER_URL` must refer to the URL of a running cryptol server.""")
if reset_server:
CryptolResetServer(c)
return c



def connect_stdio(command : str, cryptol_path : Optional[str] = None) -> CryptolConnection:
Expand Down Expand Up @@ -102,7 +117,7 @@ class CryptolConnection:
proc: ServerProcess

def __init__(self,
command_or_connection : Union[str, ServerConnection, ServerProcess],
command_or_connection : Union[str, ServerConnection, ServerProcess],
cryptol_path : Optional[str] = None) -> None:
self.most_recent_result = None
if isinstance(command_or_connection, ServerProcess):
Expand Down
83 changes: 41 additions & 42 deletions cryptol-remote-api/python/poetry.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions cryptol-remote-api/python/pyproject.toml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[tool.poetry]
name = "cryptol"
version = "2.11.0"
version = "2.11.1"
readme = "README.md"
keywords = ["cryptography", "verification"]
description = "Cryptol client for the Cryptol 2.11 RPC server"
Expand All @@ -12,7 +12,7 @@ include = [
]

[tool.poetry.dependencies]
python = "^3.8"
python = ">=3.7.0"
requests = "^2.25.1"
BitVector = "^3.4.9"
argo-client = "0.0.4"
Expand Down
Loading

0 comments on commit a65e776

Please sign in to comment.