Lean server mode - tactics

Stream: new members

[Auguste Poiroux]

Hello!

I'm trying to use Lean in server mode to get the status of a proof after applying a tactic. Currently, I'm using the full-sync function of lean-client-python (thanks to @Jason Rute and @Patrick Massot for this great tool) to do that. The problem is that it's a bit slow (~0.2s). Is there another way to do this? From what I understand, we're working on a "file" that we sync with Lean. Is it possible, for example, to modify only a part of the file, so that we don't have to resync the whole file (and so that Lean doesn't rebuild it from scratch)? Also, I didn't find the doc for using Lean in server mode, where can I find it?

Thanks in advance!

[Bryan Gin-ge Chen]

Regarding the delay, there's some previous (unresolved) discussion here. Sadly, there's no official docs on the commands in server mode. I was able to figure out how to work with it from the source code of lean-client-js (see also this file), but maybe lean-client-python is easier to read now. See also https://github.com/leanprover-community/lean-client-python/issues/15

Maybe you've already seen this, but Jason gave a nice summary of the situation regarding Lean 3 server mode here.

[Auguste Poiroux]

Thank you very much! I got all the answers I need :smile:

[Jason Rute]

And for anyone else coming to this thread who doesn’t know already, the 0.2 seconds is hard coded into the lean server. See the linked discussions above for more information.

[Jason Rute]

Auguste Poiroux said:

I'm trying to use Lean in server mode to get the status of a proof after applying a tactic.

Would you be willing to share what kind of application you are trying to build here, and also for your other thread where you say:

Is there a tool to extract the whole structure of a Lean file? The goal is to extract all the tactics from each proof (for proof in tactic mode) and to transform a term proof into a tactic proof.

[Jason Rute]

The reason I ask is that I've slowly been building some tools which do these sort of things. I've worked on versions which use the Lean server (slow) and that don't (faster but more work to build). Unfortunately, Lean doesn't have any form of nice tactic-level proof recording and doesn't have a great way to interact with it programatically.

[Jason Rute]

(Also, I initially missed your other conversation. I don't follow the new member stream.)

[Auguste Poiroux]

I am currently working with Stanislas Polu to do ML with Lean. My goal right now is to extract mathlib proofs in tactic mode. As you say, it's not an easy thing. But your tools are very useful to me. I'm also very interested in a tool that doesn't have that 0.2s delay. Do you think Lean4 will have a different (better) interface to do this?

[Notification Bot]

This topic was moved by Jalex Stark to #general > Lean server mode - tactics