Zulip Chat Archive

Stream: new members

Topic: I want to DLLize Lean


view this post on Zulip Daniel Donnelly (Aug 24 2019 at 06:49):

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?

view this post on Zulip Bryan Gin-ge Chen (Aug 24 2019 at 07:03):

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.

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:06):

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.

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:07):

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

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:07):

lean is definitely not written in python...?

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:07):

So you have full access to Lean I guess?

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:07):

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

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:08):

are you talking about lean 4?

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:08):

*I mean you have full access through server mode ?

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:08):

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

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:09):

No, certainly not full access

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:10):

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

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:11):

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.

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:11):

you can do that with server mode

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:12):

Is there an article on how to use server mode?

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:12):

it's not very well documented

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:12):

I would consult the vscode-lean extension

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:13):

Thanks!

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:13):

:)

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:14):

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

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:16):

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

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:19):

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

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:19):

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

view this post on Zulip Bryan Gin-ge Chen (Aug 24 2019 at 07:20):

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

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:21):

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

view this post on Zulip Bryan Gin-ge Chen (Aug 24 2019 at 07:23):

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

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:23):

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

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:23):

Lean 3 is frozen until lean 4 comes out

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:24):

Oh, so community gets updated, I see.

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:24):

the community fork is maintained by the folks on this chat

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:24):

Not sure which one I should use...

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:24):

Lean3 vs Lean3 community

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:25):

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

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:25):

Cool, community version it is!

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:26):

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

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:26):

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

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:27):

Thank you, again!

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:27):

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

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:28):

Oh, you know where the community release page is?

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:30):

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

view this post on Zulip Mario Carneiro (Aug 24 2019 at 07:30):

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

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 07:32):

Thx, downloaded.

view this post on Zulip Patrick Massot (Aug 24 2019 at 07:55):

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

view this post on Zulip Patrick Massot (Aug 24 2019 at 07:56):

You can also have a look at this discussion


Last updated: May 14 2021 at 06:16 UTC