language server

Stream: lean4

[Anders Christiansen Sørby]

I usually develop with nix and use nix develop to set LEAN_PATH and LEAN_SRC_PATH with the respective dependencies. I also add local directories with to LEAN_PATH, but this isn't perfect. Because the language server lean --server complains that there is no .olean files in the local dir. Why can't it just compile them? I want to make several improvements to the Lsp so that it becomes more nix friendly.

On a different note: Would it be possible to integrate the lean parser with tree-sitter so that one doesn't have to reimplement the parser there?

[Sebastian Ullrich]

You should not have to do any of this. lean-dev/emacs-dev/vscode-dev take care of compiling everything on the fly.

[Sebastian Ullrich]

Anders Christiansen Sørby said:

On a different note: Would it be possible to integrate the lean parser with tree-sitter so that one doesn't have to reimplement the parser there?

A static grammar like Tree-sitter's will never fully understand Lean's dynamic syntax. But writing a tool that generates a Tree-sitter grammar from a given set of Lean modules might be possible.

[Anders Christiansen Sørby]

Sebastian Ullrich said:

You should not have to do any of this. lean-dev/emacs-dev/vscode-dev take care of compiling everything on the fly.

Yes, but I'm using helix editor and it would be nice if the language server itself took care of generating olean files IMO.

[Anders Christiansen Sørby]

Now I have to do it manually with lean

[Sebastian Ullrich]

Then use lean-dev from your editor, just like emacs-dev and vscode-dev do

[Alex J. Best]

@Julian Berman has been working on a tree sitter parser iiuc https://github.com/Julian/tree-sitter-lean

[Anders Christiansen Sørby]

Sebastian Ullrich said:

You should not have to do any of this. lean-dev/emacs-dev/vscode-dev take care of compiling everything on the fly.

I missed that part. Maybe move/copy it to an editor specific section?