The root of some of our problems with `commands.py`

[jasonrute]

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 called response_data or something. In the Trio server at least, this is what will be processed and stored by the receiver. Then later the trio send method, when it gets that CommandResponse (or ErrorResponse) can further process it since it knows the type of the request. The commands.py file can have another function called refine_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?

[PatrickMassot]

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 commands.py, this is independent from using trio or Qt or any other event loop.

[jasonrute]

I agree it should stay inside this file. I can add it after we merge the other PRs.

[PatrickMassot]

What's the status of this idea? Is it waiting on #3? On something else?

[jasonrute]

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?

[jasonrute]

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.

[PatrickMassot]

Sure, I'll adjust the Qt code once you're ready.

[jasonrute]

I've been working on this. It is going well. I'm finding (and fixing) a lot of bugs in commands.py. Also here is how this relates to other PRs and issues:

• PR #4 (Fix receiver bug) still needs to be reviewed and merged before I PR this change. This is the remaining bug in the Trio server that is not directly related to the the Lean server logic.
• PR #5 (Address non-happy paths) can be cancelled. I will incorporate that PR into this refactor of commands.py. In particular, I'm finding a lot of similar non-happy path issues in the other server commands, so we might as well address them all at once.
• Similarly, Issue #2 (sync freeze if called on unchanged file) will be fixed in this change instead of PR #5.
• Issue #11 (Unit tests for commands.py) will be addressed in this. I'm carefully going through all of the scenarios (both good and bad), documenting them and making corresponding unit tests.
• Issue #14 (Support Lean 3.15 and widgets) might also be addressed here. I haven't done it yet, but since I'm refactoring commands.py, I might as well also add support for widgets. That way the server works on Lean 3.15.0+.
• Issue #8 (More comprehensive Trio example) might get pushed off until another PR, but I'm carefully documenting the interface through a comprehensive example. That might become an example in the examples directory later.
• I'd also like to tackle Issue #15 (document lean server interface) here, but that is a secondary goal.

[gebner]

I've just learned about this issue in the comments of https://github.com/leanprover/lean-client-js/pull/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.

parse_response is trying (with limited success) to figure out what type a response is from the JSON alone.

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 send(request: any): Promise<any> function (where any is the type of json values). The functions for the other requests are wrappers that serialize, call send, deserialize. (Well, serialization/deserialization is a no-op in javascript.) Such wrappers are useful for type safety anyhow.

[jasonrute]

@gebner

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.

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.)

The javascript library essentially exposes a raw send(request: any): Promise<any> function (where any is the type of json values). The functions for the other requests are wrappers that serialize, call send, deserialize. (Well, serialization/deserialization is a no-op in javascript.) Such wrappers are useful for type safety anyhow.

I'll look at that JS library again.