Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use gRPC reflection to retrieve CmdExecutor file #1075

Merged
merged 6 commits into from
Aug 3, 2023

Conversation

rnbguy
Copy link
Member

@rnbguy rnbguy commented Jul 24, 2023

This PR removes dependency to APALACHE_DIST while retrieving CmdExecutor.proto file.

If APALACHE_DIST is not set, it retrieves the file directly from the default gRPC endpoint localhost:8822.

  • Put reflection.proto in local package and remove axios dependency to make http requests.
  • Improved coding style with Quint team (I am not sure about my either-monad usage)
  • Tests added for any new code
  • Documentation added for any new functionality
  • Entries added to the respective CHANGELOG.md for any new functionality
  • Feature table on README.md updated for any listed functionality

Related to #701, #823

@rnbguy rnbguy requested a review from thpani July 24, 2023 22:33
@thpani thpani force-pushed the grpc-client-via-reflection branch 2 times, most recently from 6298820 to 56bd398 Compare July 25, 2023 10:00
Copy link
Contributor

@thpani thpani left a comment

Choose a reason for hiding this comment

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

Really cool! 🎉 Thanks a lot for the contribution, @rnbguy! 🙏

I've cleaned up the code a bit, and added the reflection proto locally.
Would also like to get @shonfeder's opinion before approving.

Is there a reason why you used v1alpha/reflection.proto instead of v1/reflection.proto?

quint/src/quintVerifier.ts Outdated Show resolved Hide resolved
@thpani thpani self-assigned this Jul 25, 2023
Copy link
Contributor

@shonfeder shonfeder left a comment

Choose a reason for hiding this comment

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

Thanks for the contribution, Rano!

quint/package.json Show resolved Hide resolved
quint/src/reflection.proto Show resolved Hide resolved
quint/src/quintVerifier.ts Outdated Show resolved Hide resolved
quint/src/quintVerifier.ts Outdated Show resolved Hide resolved
@rnbguy
Copy link
Member Author

rnbguy commented Jul 25, 2023

@thpani hey good catch ! I think I randomly searched online and picked a link from the official repo.

You should use v1 over v1alpha.

@shonfeder
Copy link
Contributor

My outstanding reservations notwithstanding, I am fine with proceeding! LMK when it is ready for review :)

@rnbguy rnbguy marked this pull request as ready for review July 26, 2023 08:53
@rnbguy rnbguy force-pushed the grpc-client-via-reflection branch 2 times, most recently from 219458a to 1921175 Compare July 26, 2023 14:44
@rnbguy
Copy link
Member Author

rnbguy commented Jul 26, 2023

I finalized the PR. Let me know if I should add any test or update changelog or readme for this.

@rnbguy
Copy link
Member Author

rnbguy commented Jul 29, 2023

@thpani FYI, I just noticed apalache server users v1alpha.

$ apalache server &
$ grpcurl -plaintext localhost:8822 list
grpc.reflection.v1alpha.ServerReflection
shai.cmdExecutor.CmdExecutor
shai.transExplorer.TransExplorer

@thpani
Copy link
Contributor

thpani commented Jul 31, 2023

@thpani FYI, I just noticed apalache server users v1alpha.

Aaah yes! It looks like v1alpha is the version baked into grpc-java (and all the other languages): https://github.com/grpc/grpc-java/blob/944de93f7987d050a58c8414ec79d677c4aa7709/documentation/server-reflection-tutorial.md#enable-server-reflection

thpani
thpani previously approved these changes Jul 31, 2023
Copy link
Contributor

@thpani thpani left a comment

Choose a reason for hiding this comment

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

LGTM
Thanks for helping out here, @rnbguy! 👍

@thpani
Copy link
Contributor

thpani commented Jul 31, 2023

I will adapt the Apalache integration tests that currently fail CI, then this is good to merge from my side.

@thpani thpani force-pushed the grpc-client-via-reflection branch 3 times, most recently from f3a6df8 to ad0ddca Compare August 2, 2023 07:56
@thpani thpani dismissed their stale review August 2, 2023 08:04

contributed major parts, someone else should review

@thpani thpani force-pushed the grpc-client-via-reflection branch from 60fb43b to f9223ea Compare August 2, 2023 08:26
@thpani
Copy link
Contributor

thpani commented Aug 2, 2023

It took a some iterations, but I'm finally happy with this 😄
Squashed the main changes into a single commit, to help with reviewing.

@shonfeder PTAL?

@thpani thpani requested a review from shonfeder August 2, 2023 08:29
Copy link
Contributor

@shonfeder shonfeder left a comment

Choose a reason for hiding this comment

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

Looks great! Awesome work you both and thanks for improving the interface and kicking this off, @rnbguy !

@thpani thpani enabled auto-merge August 3, 2023 06:28
@thpani thpani merged commit 91d53a8 into informalsystems:main Aug 3, 2023
15 checks passed
@shonfeder shonfeder mentioned this pull request Aug 3, 2023
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