How do you set the Lean exec?

Stream: new members

[Daniel Donnelly]

I'm working on BananaCats and figured I would reverse engineer the protocol for talking to Lean that VSCode uses. I will do this by replacing the lean.exe with my own, and forwarding commands to the real lean. So where does "elan" install Lean, and how do I specify a custom exe path?

EDIT: found the Executable path in settings. Would it be best if my app installed VSCode for the user too, so that I don't have to make any sort of Lean editor? I think so... It will have one lean file per app instance maybe, or should it be per diagram? I think per app instance, so you can have many BanCats open, and one VSCode / Lean. VSCode / Lean is much more processor intensive than my GUI code.

[Daniel Donnelly]

Thinks will be drag / droppable, so maybe if I'm dragging to the application lean.exe I can convert the objects in question into Lean data statements

[Andrew Ashworth]

you do not need to reverse engineer it

[Andrew Ashworth]

the base protocol is documented at https://github.com/Microsoft/language-server-protocol

[Mario Carneiro]

I don't think lean is based on LSP

[Mario Carneiro]

I would suggest modifying the vscode extension to log all JSON packets

[Andrew Ashworth]

ahh, there is a dummy lsp implementation then at https://github.com/leanprover/lean-client-js/tree/master/lean-language-server

[Andrew Ashworth]

which i guess is nonfunctional? idk

[Daniel Donnelly]

Thx

[Mario Carneiro]

actually it probably is pretty easy to modify the extension to call lean --server | tee lean.log instead of lean --server

[Daniel Donnelly]

Yes, I don't mean rev engineering. If I just hooked up an EXE between them, I could even maybe do the final version that way (a middle man). Well doing the EXE between and you just print the JSON...

[Daniel Donnelly]

In fact, a Lean EXE can only connect to one thing at a time, so I'd have to be the middle man anyway. There's logically no other way to do it

[Daniel Donnelly]

Lean <-> BanCats <-> VSCode

[Mario Carneiro]

Presumably there is no need for vscode in the "final version" though?

[Daniel Donnelly]

Lean <--> VSCode -> LogFile, BanCats -> ?

[Daniel Donnelly]

There's no way I'm writing an IDE as good as VSCode

[Mario Carneiro]

but that's not the goal, right? You just need lean to act as backend for your theorem goals

[Daniel Donnelly]

I'm going to use it in version 1.0 so that I will create a VSCode + Lean installer for us too. On OSX / Linux, I will need help on getting the VSCode equivalents (to Windows 10)

[Mario Carneiro]

unless you are doing the text editor whole nine yards

[Daniel Donnelly]

@Mario Carneiro I want the user to be able to extend the system and be part of the Lean community as well

[Mario Carneiro]

I'm not sure I follow. How do you envision the interaction?

[Daniel Donnelly]

So if there's something missing, like some new math area, then my system can support it by adding Lean support

[Mario Carneiro]

Is the user using your tool to edit lean files? Or are they using VSCode?

[Daniel Donnelly]

They're using my tool 100% graphically (2D graphics) to create lean code on-the-fly. This gets sent to Lean, and somehow I'd have to make VSCode update, not sure how.

[Daniel Donnelly]

But optionally they can go into VSCode to add in their custom "perfectoid spaces of the future"

[Mario Carneiro]

I would guess that the easiest way to intervene is to make VSCode interact with your program by writing your own extension extending vscode-lean

[Mario Carneiro]

i.e. Lean <-> VSCode <-> BanCats

[Daniel Donnelly]

The language of categories won't change, so there's less to extend with BanCats, and more so with Lean

[Mario Carneiro]

that way you can set the protocol on the BanCats side

[Daniel Donnelly]

Interesting!

[Daniel Donnelly]

So I'll look at that plugin. Thank you!

[Mario Carneiro]

and vscode-lean has already done the messy work of parsing the lean protocol

[Daniel Donnelly]

Right right right

[Daniel Donnelly]

:D

[Daniel Donnelly]

In about 7 months, people can start to use BananCats as an alternative way to install and use Lean.

[Daniel Donnelly]

Maybe in 1 year it will be useable

[Daniel Donnelly]

But the first release will have a proof of Yoneda's Lemma. Since that's one of my design tests of the UX.