Zulip Chat Archive
Stream: general
Topic: How do you use Lean at command line?
Daniel Donnelly (Dec 03 2019 at 22:35):
Hi, I'm not liking working with the Coffee/TypeScript code of VSCode, so I'm wanting to just communicate some other way with Lean itself. How can I do this?
Bryan Gin-ge Chen (Dec 03 2019 at 22:38):
What exactly are you trying to do and what is unsatisfactory about VS Code? By the way, there is no coffeescript in the vscode-lean extension, only typescript and some HTML / JS for the info view...
Bryan Gin-ge Chen (Dec 03 2019 at 22:40):
lean -h displays a list of command line options. If you want to write a program to communicate with Lean, then lean --server accepts JSON commands from stdin and returrns JSON responses to stdout.
Daniel Donnelly (Dec 03 2019 at 22:41):
What exactly are you trying to do and what is unsatisfactory about VS Code? By the way, there is no coffeescript in the vscode-lean extension, only typescript and some HTML / JS for the info view...
I was connecting my app BananaCats as a program to send and receive the same traffic that goes to / from Lean to VSCode. However, working with the typescript got really annoying. What I would like is to create an IDE for Lean essentially, and without learning the TypeScript interface.
Daniel Donnelly (Dec 03 2019 at 22:41):
@Bryan Gin-ge Chen yes that's what I need
Daniel Donnelly (Dec 03 2019 at 22:42):
lean -hdisplays a list of command line options. If you want to write a program to communicate with Lean, thenlean --serveraccepts JSON commands from stdin and returrns JSON responses to stdout.
Is there any reference yet for this interface?
Bryan Gin-ge Chen (Dec 03 2019 at 22:45):
Sadly, the best documentation for the server mode commands and responses is the following typescript file https://github.com/leanprover/lean-client-js/blob/master/lean-client-js-core/src/server.ts . Feel free to ask if you have any questions though.
Bryan Gin-ge Chen (Dec 03 2019 at 22:48):
Oh, this file is also useful https://github.com/leanprover/lean-client-js/blob/master/lean-client-js-core/src/commands.ts
Daniel Donnelly (Dec 03 2019 at 22:52):
Thanks. So it's mostly a reverse engineering jerb. I will ask lots of questions :)
Daniel Donnelly (Dec 03 2019 at 22:53):
@Bryan Gin-ge Chen is there a grammar reference for Lean somewhere or is it just embedded in the main manual?
Bryan Gin-ge Chen (Dec 03 2019 at 23:26):
The only grammar reference for Lean that I know of is this page of the manual.
Last updated: Dec 20 2023 at 11:08 UTC