Examples of communicating with Lean

Stream: general

[Jason Rute]

Miguel Raz Guzmán Macedo said:

Hello Patrick Massot ! Don't mean to hijack your thread, but would you know of any examples of C++ or Python wrappers of Lean?
I am looking to call Lean from Julia, and a Python or C++ wrapper as an example would help. Thanks!

I decided to move the conversation here into it's own thread. (But like I said in the previous thread, I'd love more information about what you are trying to accomplish.)

[Jason Rute]

The simplest way to "talk" to Lean is to use the Lean server. If you run lean --server it starts a server which is what vs-code and the online editors use to check Lean files and provide information in the hovers and side bar. It communicates asynchronously via JSON. The one problem is that it is a language server, so using it for communication with Lean is a bit of a hack and has a few upsides and downsides:

• You write Lean code in a file (or just send via text) and have the server "check" that code. You can also ask for certain types of information about lines in the code. This is an upside since you can use any Lean code, but it is also a downside since you have to write Lean code programmatically.
• There is a hard coded 200 ms delay to process any changes to a file. Depending on your application, this may be prohibitively slow, especially if you want to write Lean code, check it (e.g. look at the goal state), and then write more code based on that. (This is still much faster however than calling the Lean compiler directly on a file. Also, the 200 ms delay is just hard coded, so you could remove it if you are willing to hack Lean.)
• You can output information by tracing it, and then using the server to find that traced information.
• The interface isn’t documented.
• The server is asynchronous. You send it a request, and eventually you will get a response of the type you need. If you try to handle it synchronously, you may end up getting a cut-off response missing some of the information you want. (It will still be valid JSON, but missing information.

Here are a number of projects using the Lean server to call Lean from another programming language:

• Here is a semi-official lean-python client which calls the Lean server It properly handles the async communication. There are however some bugs that need to be fixed.
• Here is an example of how to use that server for some sort of back and forth exploration of proofs. It doesn’t properly handle the async communication, but it is a good example of ways to communicate interactively with Lean.
• Here is an app where Mathematica calls Lean via the server
• This tool calls the Lean server on every character of every file to get information about that file Again, it doesn’t handle the async correctly and that leads to problems with the results.
• This tool use the Lean server to format Lean files

[Jason Rute]

Lean also has a simple IO interface. You can write a stand alone Lean app (with a main function) which can communicate with stdin and stdout. This is a reasonable way to communicate with an external process, but does require a fair amount of writing code in Lean's monad style and you have to know how to get to the stuff you want inside Lean. Lean 3 for hackers is a very short tutorial on the IO interface. Moreover, the IO interface can be used to call another process inside Lean (also mentioned in that tutorial). This is used for the other direction of the Lean-Mathematica interface to call Mathematica from within Lean.

[Jason Rute]

I'm using this IO approach to build a tool for machine learning purposes which lets Python (or another language, like Julia) interact with the tactic environment with Lean. It is very slow going since I have to directly expose everything I want in Lean. However, when it is built I think it could be very useful for certain purposes. My purpose is a tool for training machine learning agents to make Lean proofs. A prototype should be available soon, and a more fully featured version later.

[Jason Rute]

Last, if you talk with any of the official Lean developers, I think the answer you will get is that Lean 4 will make this sort of interfacing easier. This might be true, but Lean 4 is a long ways away.

[Kevin Buzzard]

Do you know that Lean 4 is a long way away? Is it not the case that for all we know, they will release it tomorrow? Or is it somehow completely clear to people that the release date is X years away for some explicit value of X? I thought literally nothing about X was known

[Jason Rute]

First, I always assume if something is in the future and a developer is making that something, it will be a long time coming, especially if there is no provided deliverable date. This is both a pessimistic view and a pragmatic one from my time in industry. I don't want to be stuck waiting months or years for Lean 4, when we have Lean 3 now.

Another point is that if Lean 4 was released tomorrow that it would take a lot of work to port mathlib over to Lean 4, and get folks using Lean 4, so that is additional time. Also, I doubt any solid Lean 4-Python communication tools will come with Lean 4, so those will also have to be built. There probably will be a language server and and IO interface however in Lean 4. If we already build tools that interact with the Lean 3 language server and the Lean 3 IO interface, it will be easier to start working with the Lean 4 language server and IO interface, so I say, let's start building that stuff now. If there turns out to be a much better way to interact with Lean 4 via Python (or Julia) then we can switch to that when it comes.

[Mario Carneiro]

Also, if you watch the rss stream you can see daily commits to lean 4, which can give you a vague idea of what's currently being worked on. It still looks a long way from finished to me

[Mario Carneiro]

(I also think that they have been somewhat sidetracked from the goal of shipping lean 4 ASAP. I'm not sure if this is because they want things to write papers about or something but stuff like the tactic framework seems to be taking a back seat to more syntax stuff, which is not critical to getting an MVP. But they have their own priorities and I can only guess at them.)

[Kevin Buzzard]

I do watch the rss stream but because I am quite un-CS it all means nothing to me. So there is no progress on the tactic framework? What does that even mean? Do they have begin ... end yet?

[Mario Carneiro]

I don't know if it's in the grammar yet, but I'm pretty sure there are no instances of begin end use in lean 4 yet

[Jason Rute]

I've never tried to run Lean 4 so I don't know for sure, but there appear to be lots of begin ... end blocks in the tests. Also, there are various parsers for begin ... end blocks too. Of course, I'd still like more news on what the tactic framework does and doesn't currently have.

[Mario Carneiro]

Oh you are right. The tactic grammar is defined here: https://github.com/leanprover/lean4/blob/master/src/Lean/Parser/Tactic.lean but I don't think these tactic names are hooked up to anything

[Jason Rute]

https://github.com/leanprover/lean4/tree/master/src/Lean/Meta/Tactic ?

[Mario Carneiro]

there are also some tactics, but they look like non-interactive tactics to me

[Mario Carneiro]

not sure where the front end is declared

[Mario Carneiro]

but this is indeed more progress than I thought

[Mario Carneiro]

Ah, here's the front end: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/Basic.lean

[Mario Carneiro]

There are definitely tactics in the grammar with no definition, like allGoals, but some of the basic tactics like intros seem to be defined

[Patrick Massot]

Mario Carneiro said:

(I also think that they have been somewhat sidetracked from the goal of shipping lean 4 ASAP. I'm not sure if this is because they want things to write papers about or something but stuff like the tactic framework seems to be taking a back seat to more syntax stuff, which is not critical to getting an MVP. But they have their own priorities and I can only guess at them.)

I don't think they got sidetracked. I think they never were on that track. The P in MVP means product, right? But Lean is not a product. And also Lean 3 is much more than minimally viable.

[Mario Carneiro]

by minimally viable I mean ready to open up to users to finish the job of making it more full featured

[Mario Carneiro]

The whole point has been to make lean more configurable so that Leo & co don't have to implement everything, they give the tools to the users (us, hopefully)

[Miguel Raz Guzmán Macedo]

Thanks a million for this response!
I just saw this because I didn't get a proper notification from Zulip and am a bit new at this - sorry for the delay.

1. I will check out those examples that you posted.
   2.It seems that I need to start a lean server and hack that 200ms delay to 0 if possible. As I undestand it, it is best to start up a process with a lean --server, and query it continuously, rather than paying the startup cost of the compiler everytime?

2. I should not have a problem with talking with the lean server asynchronously, in theory :tm: .

[Miguel Raz Guzmán Macedo]

Update:
I have the dependency thing worked out, I just need to poke a bit at running processes from Julia and I should get a hello world (Make a Julia package download Lean on Windows/Mac/Linux, build it, and solve the simple m + n = n + m by calling out to Lean via Julia)

[Jason Rute]

I wouldn’t say you need to hack the delay. It depends on your use case. What is that again? And yes, by using the lean server continuously you avoid paying the lean startup cost more than once. (Also it should be able to handle incremental checking of a lean file.)

[Miguel Raz Guzmán Macedo]

I want to open up Julia as a tool for formal verification with Lean. Though a Lean <-> Julia bridge for ML purposes would also be awesome. (I'm a diehard Julia fan, and I think it totally dunks on Python for ML stuff, so you're welcome to join the darkside!)

[Miguel Raz Guzmán Macedo]

Oh, incremental checking sounds great.

[Mario Carneiro]

I want to open up Julia as a tool for formal verification with Lean

@Miguel Raz Guzmán Macedo I'm also curious what you mean by this statement. What role is Julia playing here? Is it an alternative way to write proofs in lean, like a REPL? Is Julia being used as a way to get souped up CAS style tactics for lean proofs? It's not clear how having access to lean helps your Julia workflow, or vice versa.

[Miguel Raz Guzmán Macedo]

I want to use Lean to prove properties about code written in Julia.

[Miguel Raz Guzmán Macedo]

(for now)

[Mario Carneiro]

That's pretty tough TBH. Lean normally can only be used to prove properties about functions defined in its logic, i.e. as non-meta lean functions. Is it possible to extract the syntax of a function from Julia so that it can be translated somehow to lean? Is Julia sufficiently well typed that there is a reasonable translation here?

[Miguel Raz Guzmán Macedo]

1. I know that extracting syntax from Julia functions is baked into the language - it is homoiconic.
2. Translating that to Lean, don't know.
3. About sufficient well typed-ness, don't know enough about types, but I know the Julia people who know about types don't lose sleep over what can/can't be expressed in the type system.

[Patrick Stevens]

Julia is dynamically-typed - I'd be surprised if it were at all easy

[Mario Carneiro]

You will probably have to do translations manually in that case. Just copy and paste the source and lean-ize it

[Sebastian Ullrich]

Is mutation not rampant in Julia? I assume you would need a deep embedding of it into Lean and your own formal semantics (with heap) on top of that to say anything about nontrivial programs.

[Ryan Lahfa]

Miguel Raz Guzmán Macedo said:

(… I think it totally dunks on Python for ML stuff, so you're welcome to join the darkside!)

[citation needed] :P

[Ryan Lahfa]

On the subject, I'm curious whether we can use Lean for Rust, notably stuff like this: https://plv.mpi-sws.org/rustbelt/

[Jason Rute]

Ryan Lahfa said:

On the subject, I'm curious whether we can use Lean for Rust, notably stuff like this: https://plv.mpi-sws.org/rustbelt/

Like this? https://pp.ipd.kit.edu/uploads/publikationen/ullrich16masterarbeit.pdf

[Patrick Massot]

Ryan Lahfa said:

On the subject, I'm curious whether we can use Lean for Rust, notably stuff like this: https://plv.mpi-sws.org/rustbelt/

@Sebastian Ullrich probably has something to say here.

[Patrick Massot]

Arg! Jason was faster!

[Sebastian Ullrich]

RustBelt's and my approach are quite complementary - a deep embedding with a separation logic semantics focused on unsafe code vs a shallow embedding focused on a pure-ish subset of safe Rust code. In general, a nice separation logic framework like Iris is something that Lean is sorely lacking to be more attractive to CS people, or at least PL people.

[Simon Hudon]

I'm working on it but it takes a lot of work

[Jason Rute]

There has been a lot of discussion here. What are you working on? Lean4?

[Simon Hudon]

A separation logic framework