Tips / Pointers for adding support for Lean4 LSP?

[FruitfulApproach]

Hi,

I'm needing to communicate with the Lean4 LSP. Can you point me to any helpful resources?

Thanks.

[LakshyAAAgrawal]

Hi @FruitfulApproach ,

I have shared some general guidelines for adding new language support in #5. I would be glad to discuss any further details that you would like about implementing support for a new language server in multilspy.

For Lean4 specifically, I believe the following existing lean4 clients should provide good starting points:

• https://github.com/leanprover/vscode-lean4 (https://github.com/leanprover/vscode-lean4/blob/d8f81697525abdfe424a7035ed93b0407bb5de55/vscode-lean4/src/leanclient.ts#L4).
• Various mentions of language server in (https://github.com/search?q=repo%3Aleanprover-community%2Flean4game+language+server&type=code).
• https://github.com/onriv/lean4ij

[FruitfulApproach]

Hi @LakshyAAAgrawal :)

How would we go about attaching it to a VSCode/Lean4 plugin's LSP instance? I'm very new to LSP protocol. So I will read up on it first.

The goal would be to "see everything" that the Lean4 info-view sees as you type in Lean4 code in addition to the "static analysis" mentioned on this repo's front page. Would that be possible with this library?

Also, I've already started editing the code. I created a test_multilspy_lean4.py and got it to debug as a Pytest in Wing Pro ide. Question is what would be a good test repository to use? Do you think the lean4-samples is appropriate for the test case?

Thank you.

[LakshyAAAgrawal]

Hi @FruitfulApproach ,

How would we go about attaching it to a VSCode/Lean4 plugin's LSP instance? I'm very new to LSP protocol. So I will read up on it first.

You will have to find the command that launches the Lean4 LSP. I believe that the documentation for Lean4 that I linked should be helpful. If I was doing this, I would install Lean4, and simply run something like lean4 --help and that should hopefully print some useful information about launching the language server. I am sorry but I don't have cycles immediately to look into this myself. But if you could set it up on your machine, and provide me with the output of lean4 --help I could then try and help you with the next steps.

Once you have the command to launch the server, it should be easy to follow the steps provided in #5 . Please feel free to contact me over this thread at any step, and I would be glad to help to my best capability. I apologize again for not being able to take this up myself right now.

The goal would be to "see everything" that the Lean4 info-view sees as you type in Lean4 code in addition to the "static analysis" mentioned on this repo's front page. Would that be possible with this library?

One way to determine this would be:
Setup Lean4 Language Server on VSCode, go to the Lean4 VSCode extension settings, set lsp log mode to verbose, open the "Output" panel in VSCode, and then open the functionality you want to check. If you see a corresponding command being sent from the client to the language server, then it is implemented using the LSP, and should be available through multilspy as well. Again, feel free to share output from any of these steps, and I could try to help you parse the output.

Also, I've already started editing the code. I created a test_multilspy_lean4.py and got it to debug as a Pytest in Wing Pro ide. Question is what would be a good test repository to use? Do you think the lean4-samples is appropriate for the test case?

That is exciting! Thanks a lot for starting the exploration. Any repository written in lean4, that can be verified with lean4 as a project should be a good testcase! I believe lean4-samples should be fine, but it seems archived. Would you be able to look into any of the examples from the following page: https://leanprover-community.github.io/? They seem more up to date, and I believe should also be easier to work with.