Lean Server Returning Empty Responses?

Stream: new members

[Andrew Elsey]

Hi, not sure if anyone has any experience with the lean server, but I've run into some strange behavior. Essentially, when I send sync or info requests, I'll get an empty response back that looks like "{"response":"ok","seq_num":113}'". The only thing I am able to get working is a sync request, and only by sending the file contents directly, rather than just a file name, in the sync request, and to make some small permutation in the file (adding a trivial line), although maybe this is expected behavior as synching the same file should be idempotent. However, I am hoping for more granular output via the info command and I'm running out of ideas.

[Jason Rute]

Sorry for the trivial questions and ideas:

• You are running the server asynchronously right, i.e. you are continuously reading all the responses from the server and not just the first response?
• It also might help to look at https://leanprover-community.github.io/lean-web-editor/ and compare their traffic with yours. You can see their traffic by going to the question mark, selecting "Log server messages to console", and then opening up the javascript console.
• You may help to post a minimal working example including all the back and forth communication.

[Jason Rute]

Also, yes, re-syncing a file you didn't modify won't have the same response as syncing a file you modified. I forget the details off hand. You may want to use (or look at the code for) https://github.com/leanprover-community/lean-client-python/tree/refactor-commands-api (I sent you to a properly working branch as the master branch is broken). Use the trio server.

[Jason Rute]

That tool takes care of some of those subtleties .

[Jason Rute]

Also, finally, don't forget to check if there are any messages in the traffic. Those may indicate errors.

[Andrew Elsey]

Jason Rute said:

Also, yes, re-syncing a file you didn't modify won't have the same response as syncing a file you modified. I forget the details off hand. You may want to use (or look at the code for) https://github.com/leanprover-community/lean-client-python/tree/refactor-commands-api (I sent you to a properly working branch as the master branch is broken). Use the trio server.

I'm actually using a hacked version of your code (thank you a ton)! I'll try adapting your updated trio server code/commands file. That might do the trick.

[Andrew Elsey]

Didn't seem to work :(. Not sure if it this is helpful for you, but I did run into a few bugs: image.png
Essentially, in the commands file, json.dumps turns the line and column properties into strings instead of integers, but the server is expecting numbers.
Also, looks like the server's seq_num varies from the seq_num maintained by the server, so I had to change a few lines: image.png image.png
I'll keep playing around with it - probably doing something wrong. Thanks again.

[Jason Rute]

Thanks. I’ll look into the bugs.

[Jason Rute]

If you can isolate the problem in the lean server, you may want to post the bug in general to get more visibility. I don’t know who maintains it. Otherwise, again a minimal working example with the json traffic would help. The lean Python server has two debug parameters which print the traffic.

[Patrick Massot]

Jason Rute said:

I forget the details off hand. You may want to use (or look at the code for) https://github.com/leanprover-community/lean-client-python/tree/refactor-commands-api (I sent you to a properly working branch as the master branch is broken). Use the trio server.

I completely lost track of what happens there. Are you waiting for me to hit a merge button?

[Jason Rute]

@Patrick Massot Sorry. I haven't been doing a good job at keeping on track of it myself. Basically, yes I'd like someone (probably you or @Julian Berman), when they have time, to look over https://github.com/leanprover-community/lean-client-python/pull/19. If you like it (and it works) you can merge it. Now, I thought it worked fine last I checked it, but @Andrew Elsey claims there is a bug. Maybe I'm misunderstanding, but it seems this error would have been quite noticeable. I find this surprising since it would be a pretty glaring error, but maybe either Lean has changed or I made a big mistake. Unfortunately, I'm leaving today for a one week vacation. If there is stuff that needs to be fixed, I can address it when I get back.

[Jason Rute]

@Andrew Elsey I'm not sure I understand your bugs or your changes (for example), but regardless, the new PR changes a lot of the code you pointed out. I would try that out by using the trio server in the branch refactor-commands-api. I just tested that branch on the newest version of Lean 3.31.0 and I didn't see any obvious problems. Also all the unit tests pass.

[Jason Rute]

Of course, if you encounter problems still, feel free to make an issue or PR.

[Jason Rute]

@Patrick Massot Given that is seems to work fine, if you have time to look over the PR and merge it (if you are happy with it), I would real appreciate it. It would be good to have a working version of this project.

[Andrew Elsey]

Jason Rute said:

Andrew Elsey I'm not sure I understand your bugs or your changes (for example), but regardless, the new PR changes a lot of the code you pointed out. I would try that out by using the trio server in the branch refactor-commands-api. I just tested that branch on the newest version of Lean 3.31.0 and I didn't see any obvious problems. Also all the unit tests pass.

Yes, I was using your newer branch when I ran into the issues (although the new branch worked way better - repeated sync calls seemed to freeze the client on the main branch, even if the file has been edited). Maybe it's just related to my environment/python installation. Either way, I apologize if I wasted your time. I was able to get everything I needed for my solution working, although it did seem like the API, probably not your code base, is a little buggy. Things like having to make certain calls in a a certain order, having to make some info requests at a different column than it should be, etc. I ended up just wrapping every expression I wanted to query for in "(("expr":_))" which appears to let you make an info request at the first parenthesis uniformly. At any rate, thank you again for everything.