-
Notifications
You must be signed in to change notification settings - Fork 4
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
feat: notifications delay new request handling while running #183
Conversation
0374aab
to
28a00aa
Compare
28a00aa
to
3749d49
Compare
This set of changes has two main consequences:
|
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.
This looks awesome! I have a few questions, but they could just be due to me not having a full understanding of this codebase yet.
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.
This looks good to me. I hope we don't need to keep the delay in the Python client for long, and can figure out how to remove the need on the server side, but I think it's okay to include for now.
Makes it so that the handling of a notification cannot be interrupted/interleaved with new commands/queries/notifications. This may be enough to fix GaloisInc/cryptol#1261
Tweaking the default state eviction policy to remove older requests automatically instead of reject new ones if the server is full (thus removing the need for scripts to call
reset
when connecting) may also be helpful.