-
Notifications
You must be signed in to change notification settings - Fork 43
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
Concurrent kore-rpc
strikes back
#3708
Conversation
…or codes of the successive errors
…add a module at the same time
…f name-as-id is true
…when name-as-id is true
kore-rpc-booster
strikes backkore-rpc
strikes back
Could you also update the docs according to these changes, please? |
I opened a PR for the necessary changes in I also added a few integration tests, and one of them is failing: if you add a module, then add the same module with Running the tests: ensure the right K version is on $ make test-integration TEST_ARGS='-n0 -k TestAddModule' |
… with a name failed. also fixed logic of adding the sanem named module with name-as-id true
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Code LGTM
(:+1: new code does what we wanted)
Pre-approving, but let's add add-module/add-again
to the test script.
Expected: | ||
* Module successfully added even though it has been added already, because the content is exactly the same. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Probably the module would be added twice then?
How is add-module/add-again
executed? The test script does not mention it.
This is a revert of the revert of #3704. Needs to be merged in sync with runtimeverification/hs-backend-booster#427 and also a change to
pyk
to handle the new modules IDs.