-
Notifications
You must be signed in to change notification settings - Fork 6
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
The root of some of our problems with commands.py
#6
Comments
Yes, this sounds very reasonable. I wish this could be handled by Lean itself. One can argue this is really fixing the Lean server protocol... Anyway, I would much prefer if we can do all that inside |
I agree it should stay inside this file. I can add it after we merge the other PRs. |
What's the status of this idea? Is it waiting on #3? On something else? |
Right now there is a back log of PRs that precede this, including #3 (testing) and #5 (not requiring line and column). Now, I guess I don't need either of them to get started, so I'll try to code something up this weekend. Another issue with this (and with PR #5) is the it will require a simultaneous change to the Trio and QT. So far, I've only focused on the Trio code. If I made a change to the trio code in a branch, would you be willing to adjust the QT code to match? |
Also, another reason for the delay is that I took a month long break from working on any of this code. Once the interest increased recently, I knew I had to come back to it and finish stuff up. |
Sure, I'll adjust the Qt code once you're ready. |
I've been working on this. It is going well. I'm finding (and fixing) a lot of bugs in
|
I've just learned about this issue in the comments of leanprover/lean-client-js#12. To repeat my comment there: the unspoken assumption with JSON-based protocols is that it is always safe to add new fields, and we explicitly reserve the possibility of adding new fields in the future.
Yes, indeed. You need to know the request (it suffices to know the command name) to parse the response. The javascript library essentially exposes a raw |
I'm in the middle of refactoring our deserializer. I'll take this assumption into account (and add some unit tests to make sure it stays that way). If this product is used by more than 2 people in the future, a word of warning would still be nice so that we can make sure we support the newest features. (Also, maybe I can add integration tests which check for new fields in the latest versions of Lean.)
I'll look at that JS library again. |
As for the
commands.py
, I think it suffers from the following possible problem.parse_response
is trying (with limited success) to figure out what type a response is from the JSON alone.I think there should be two levels of
parse_response
. The first level just turns the JSON into one of fours types:AllMessagesResponse
,CurrentTasksResponse
,CommandResponse
,ErrorResponse
. If it is a CommandResponse (or we could call it OkResponse), most of the dictionary should be stored in some field calledresponse_data
or something. In the Trio server at least, this is what will be processed and stored by the receiver. Then later the triosend
method, when it gets that CommandResponse (or ErrorResponse) can further process it since it knows the type of the request. Thecommands.py
file can have another function calledrefine_command_response
(or it can be a method under command response) which takes in the CommandResponse and the Request object (or type) and returns a ResponseObject of the specific command type (SyncResponse, InfoResponse, etc). This will ensure, for example, if we send an InfoRequest, we get an InfoResponse (or ErrorResponse), even if the InfoRecord is empty. This should simplify code like the state method. Thoughts?The text was updated successfully, but these errors were encountered: