I want to DLLize Lean

Stream: new members

[Daniel Donnelly]

I want to DLLize Lean so that I can drive it from a Python app. What are your thoughts on this. Will this already be a feature through some API in version 4? In other words, should I wait? Or will this DLLization be valuable to people?

[Bryan Gin-ge Chen]

Out of curiosity, what are the things you need that you can't get by writing Python code to communicate with Lean's server mode?

It may be some time before Lean 4 is ready for use by anyone outside the core developers. A community fork of Lean 3 is being developed in this repo.

[Daniel Donnelly]

I didn't know there was server mode! Any reference for that in the docs?
I also see that Lean is (at least Lean4 that I know of) is written in Python, so rethinking this, I just should modify the python code which is already communicating with Lean's C++ code.

[Mario Carneiro]

the server mode is what is used by editor interfaces like emacs and vscode

[Mario Carneiro]

lean is definitely not written in python...?

[Daniel Donnelly]

So you have full access to Lean I guess?

[Daniel Donnelly]

What are all those .py files doing in the repo?

[Mario Carneiro]

are you talking about lean 4?

[Daniel Donnelly]

*I mean you have full access through server mode ?

[Daniel Donnelly]

Yep, Lean 4, I cloned it and viewed some of the directories.

[Mario Carneiro]

No, certainly not full access

[Mario Carneiro]

Through server mode you can basically shove lean text around. Even lean code doesn't have full access

[Daniel Donnelly]

What I mean is, you can type in commands on the front end (my python app), and they'll go into Lean's main input, and you can get the reply from Lean sent back to the frontend.

[Mario Carneiro]

you can do that with server mode

[Daniel Donnelly]

Is there an article on how to use server mode?

[Mario Carneiro]

it's not very well documented

[Mario Carneiro]

I would consult the vscode-lean extension

[Daniel Donnelly]

Thanks!

[Daniel Donnelly]

:)

[Mario Carneiro]

You might also ask @Bryan Gin-ge Chen , whose work on observable notebooks seems similar. (Are those python based?)

[Mario Carneiro]

Another place to look for really simple server use is the tests/interactive/ collection. I think there is a bash script in there that composes a really basic query for the server and checks the result

[Daniel Donnelly]

I see, in test_single.sh they're using Lean's command line interface

[Daniel Donnelly]

https://github.com/enjoysmath/lean/blob/master/tests/lean/interactive/test_single.sh

[Bryan Gin-ge Chen]

As Mario said there isn't really any written documentation for the server mode. But basically if you start lean from the command line with lean --server you can pass it messages in JSON format via stdin and recieve JSON responses via stdout. The format for these JSON objects is kind of documented in the lean-client-js repo.

The Observable notebooks are written in Javascript but they also utilize the Lean server interface (for the webassembly build of Lean). If you're comfortable reading JS, you might find this informative: https://observablehq.com/@bryangingechen/hello-lean-prover

[Daniel Donnelly]

@Bryan Gin-ge Chen thank you! That is very helpful

[Bryan Gin-ge Chen]

No problem, feel free to ask if you have more questions!

[Daniel Donnelly]

What's the difference between regular Lean and Lean Community Edition?

[Mario Carneiro]

Lean 3 is frozen until lean 4 comes out

[Daniel Donnelly]

Oh, so community gets updated, I see.

[Mario Carneiro]

the community fork is maintained by the folks on this chat

[Daniel Donnelly]

Not sure which one I should use...

[Daniel Donnelly]

Lean3 vs Lean3 community

[Mario Carneiro]

Right now, mathlib builds on both versions, but the hope is to migrate to the community version

[Daniel Donnelly]

Cool, community version it is!

[Daniel Donnelly]

I'll use whichever one doesn't require me to build it first, lol.

[Mario Carneiro]

There are builds for the community edition at https://github.com/leanprover-community/lean-nightly

[Daniel Donnelly]

Thank you, again!

[Mario Carneiro]

lol, I just noticed that the readme for https://github.com/leanprover-community/lean-nightly has a link to the releases page for the official version, don't go there

[Daniel Donnelly]

Oh, you know where the community release page is?

[Mario Carneiro]

it's the "releases" button on that page (the github one)

[Mario Carneiro]

https://github.com/leanprover-community/lean-nightly/releases

[Daniel Donnelly]

Thx, downloaded.

[Patrick Massot]

@EnjoysMath It would probably help us helping you to learn more about what you actually want to do.

[Patrick Massot]

You can also have a look at this discussion