Lean server mode - tactics

Stream: general

[Notification Bot]

This topic was moved here from #new members > Lean server mode - tactics by Jalex Stark

[Gabriel Ebner]

I looked into the 200 milliseconds issue a while back. It's not easy to resolve, although we could add a command-line flag to reduce it to, say, 100ms or 50ms. The server doesn't have a "finished" event internally that we could hook into. The problem is that the 200ms is a polling interval, and reducing it will just cause extra json traffic.

[Jason Rute]

@Gabriel Ebner I think a flag would be a good compromise. Also, by "extra JSON traffic", do you mean the we would see more all_messages responses and current_tasks responses?

[Gabriel Ebner]

Yes.

[Jason Rute]

I think if we were working with the lean server programmatically, there is no issue having more JSON messages (or at least any cost in processing two extra JSON messages every 50 ms would be negligible to the 50 ms wait). While I see the point of the the 200 ms when used as a language server, I don't see the issue with reducing the wait even more with a flag.

[Jason Rute]

@Auguste Poiroux I'm glad I asked. I've sketched some of what I've been working on to @Stanislas Polu in this conversation. For Lean 3, I've found some simple hacks to record tactic steps in the library. Basically, one can modify the base .lean files to record the tactic name, goal, and all the parameters of the interactive tactics. If you like, we can discuss my ideas further. I've implemented some of them so far, but I still need to get around to doing it at scale with all or most of the interactive tactics. As for interactive back and forth with Lean, there is the lean server mode. Other than that, I'm building a more direct prototype tool, but that is still in an incomplete stage. I'd be happy to talk about this further, either on Zulip or in a face-to-face chat.

[Jason Rute]

As for Lean 4, I am not sure what is being added that would support this. I get the vague sense that it will be easier since major parts of the Lean compiler and parser will be written in Lean, but I doubt there will be any tactic-based proof recording or programatic interactivity with Lean out of the box. (I'm not involved in Lean 4, so take my predictions with a grain of salt.)

[Auguste Poiroux]

Thank you very much for the answers! I will be happy to discuss this together with @Stanislas Polu .