Topic: Lean server mode - tactics
Notification Bot (Aug 06 2020 at 14:09):
This topic was moved here from #new members > Lean server mode - tactics by Jalex Stark
Gabriel Ebner (Aug 06 2020 at 14:20):
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 (Aug 06 2020 at 15:00):
@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
Gabriel Ebner (Aug 06 2020 at 15:00):
Jason Rute (Aug 06 2020 at 15:05):
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 (Aug 06 2020 at 15:15):
@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 (Aug 06 2020 at 15:21):
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 (Aug 06 2020 at 16:46):
Thank you very much for the answers! I will be happy to discuss this together with @Stanislas Polu .
Last updated: May 16 2021 at 05:21 UTC