Skip to content

[RPC] Single-connection interface#1285

Merged
m-yac merged 8 commits intomasterfrom
rpc/single-conn-interface
Sep 22, 2021
Merged

[RPC] Single-connection interface#1285
m-yac merged 8 commits intomasterfrom
rpc/single-conn-interface

Conversation

@m-yac
Copy link
Contributor

@m-yac m-yac commented Sep 14, 2021

This PR adds a single-connection interface for the python Cryptol RPC bindings based on the existing synchronous, typed interface. Since the argo server's default setting is to only allow a single connection at a time, this interface is a better fit for the expected use case of these bindings. The existing interfaces, where multiple Connection objects can be created, still exist and are unchanged.

Compared to the synchronous interface, this change lets us get rid of the "c."s in front of every command. Compared to the old interface, this change also lets us get rid of the .result() calls and adds more types. For example, what was before:

c.call("f", x).result()   # type: Any
c.prove("prop").result()  # type: Any

is now:

call("f", x)   # type: CryptolValue
prove("prop")  # type: Union[Qed, Counterexample]

Link for comparing this interface to the old interface: 5a668a4...rpc/single-conn-interface (e.g. check out the test cases)

Copy link
Contributor

@atomb atomb left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this looks really nice, and should make simple scripts less noisy. The one CI failure is, I believe, and issue with the CVC4 binaries we're using. I'm looking into fixing it separately.

@m-yac m-yac marked this pull request as ready for review September 17, 2021 19:29
@atomb
Copy link
Contributor

atomb commented Sep 21, 2021

Perhaps try rebasing/merging with master and see if CI succeeds now. I think it should.

@atomb atomb added this to the 2.12.0 milestone Sep 21, 2021
@pnwamk
Copy link
Contributor

pnwamk commented Sep 21, 2021

This PR should probably bump the client version and document what is added briefly in the CHANGELOG.md file.

@m-yac
Copy link
Contributor Author

m-yac commented Sep 22, 2021

This should be ready to merge, the RPC bits of the CI have passed.

The changes made in this latest batch of commits are:

  • Update the synchronous and single-connection interfaces with timeout parameters
  • Add a timeout property to the synchronous interface to match the timeout member field in the old interface
  • Add get_default_timeout/set_default_timeout methods to all three interfaces (since the single-connection interface can't have a timeout member field or property)
  • Update the changelog and bump the version number to 2.11.7

@m-yac
Copy link
Contributor Author

m-yac commented Sep 22, 2021

The CI passed for the second most recent commit, and the most recent commit just fixes a typo in CHANGELOG.md - so I'm going to merge this

@m-yac m-yac merged commit 553a78e into master Sep 22, 2021
@m-yac m-yac deleted the rpc/single-conn-interface branch September 22, 2021 20:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants