Calling lean from command line

Stream: general

[Tomas Skrivan]

I would like to use lean to check some expressions in an external program. Currently I run lean main.lean where main.lean is on the fly created file, for example when I want to check fun x, x

import system.io

#check (fun x, x)

def main : io unit :=
    io.print ""

and I get λ (x : ?M_1), x : ?M_1 → ?M_1. The problem is that lean main.lean is super slow, is there a way to make this faster. Most probably, I should use lean --server unfortunately I was unable to figure out how does it work. Tried looking at the code of emacs package lean-mode but without a success.

[Shing Tak Lam]

Have you seen https://github.com/leanprover-community/lean-client-python ? I think this might be useful, either as a library or to see how they handle communication with the Lean server.

[Tomas Skrivan]

Sweet, I'm using Python inside of the external application anyway. I will definitely have a look at it!

[Jason Rute]

The lean server is definitely a good way to go, and if you are using python I recommend the lean-client-python mentioned above since it correctly handles the asynchronous issues you run into with the lean server. It isn't well documented so here is some advice:

• The current master branch is broken when used with a recent version of Lean. I recommend the branch on this PR.
• I recommend using the trio server (not the qt server).
• There is really only one example so far and it isn't very detailed. A TODO item of mine is to make some better examples. (I'm not doing a good job on getting to it though. :smile:)
• There really is only one example so far. Play with that. Besides that example, this file is the closest thing to documentation of the lean API server.
• Also, see some of the discussion and examples in this thread: #Machine Learning for Theorem Proving > Lean client for Python
• The two best ways to get information from the Lean server is to use the info server command and also to look in the messages for any errors. (This is not documented, but maybe there are some examples in that Zulip thread.)
• If you have never used an asynchronous library like asyncio or trio before in Python, you can basically get by with two rules: (1) Every function which is defined with async def foo(...): should be called with await foo(...). (2) Every function foo which has an await inside its body should be declared with async def foo(...):.
• When you sync, you don't need to have an actual file on your computer. The "filename" is just an identifier, so it can be "dummy.lean". In that case, use the contents parameter to put in the string of your "file".
• I recommend using the same filename every time (or just a few filenames). The server doesn't forget files, and if you use fresh filenames every time, you might start to have a memory leak.
• Every sync command takes at least a hardcoded 200 ms. This isn't horrible, but for some applications where you are running many lean checks repeatedly it will be noticeable.

[Tomas Skrivan]

Thank you very much Jason for the detailed answer and tips!

The 200ms worries me a bit for my application because I'm developing a node based editor and using lean to check if the node graph is correctly set up. Thus each time user changes the network I might want to do several calls to lean to check the network.

[Jason Rute]

The only way I know of to get around the 200ms is by writing a light weight server (like a REPL) using Lean's metaprogramming framework. That does require learning to program in Lean however... I can point you to resources (or just look at previous similar conversations I've been in here on Zulip).

[Jason Rute]

Maybe widgets are another possible solution. It would use the Lean server, but maybe (not sure) it would avoid the 200ms timeouts. Again you would need to use Lean metapgramming and learn the widgets framework. It probably isn't worth it.

[Jason Rute]

There is also Lean 4. I don't know enough about it to give you solid advice, but it is a better programming language (more pleasant and faster) than Lean 3.

[Jason Rute]

Actually, I just looked at your application again, that is, checking expressions. This is similar to what @Joe Palermo is also doing (obviously likely for a different purpose). You may want to look at conversations he has had on Zulip here, including this one: #Machine Learning for Theorem Proving > Lean client for Python.

[Tomas Skrivan]

Concerning Lean 4, I'm really excited about it. However, I have spent one day attempting to translate my code from lean3 to lean4 and gave up. Right now, the lack of documentation of certain parts is just too big of a barrier for me. In particular, I'm doing some manipulations with expr and there is no chapter on metaprograming in the lean 4 manual. Furthermore, once I get the basics of my node graph editor done I will start using some parts of mathlib(linear algebra and basic calculus) and I'm not sure how is the move of mathlib to lean 4 is going(it it is happening at all).

[Gabriel Ebner]

The written documentation is indeed lacking. However we have very good oral documentation over in the lean4 stream. Feel free to ask if you're running into any issues.

[Tomas Skrivan]

I will get the core done in lean 3 first, as I'm familiar with it, then I'm happy start translating it to lean 4 and ask gazillion questions how to do this and that.