lean-language-server parameters

Stream: general

[Julian Berman]

I am trying to increase the memory limit for lean (i.e. the equivalent of lean.memoryLimit) via lean-language-server, but as far as I can tell, there isn't a way to pass through command line options.

I found https://github.com/leanprover/lean-client-js/blob/master/lean-language-server/src/index.ts#L30 which I think is what'll run when running lean-language-server --stdio, but that line will always pass [] as argv to the lean subprocess.

Can someone just confirm I didn't miss something there / whether there's some command line option to lean-language-server that indeed will passthrough to lean?

[Bryan Gin-ge Chen]

That looks right. It shouldn't be too hard to modify that line to read options from the command line; for reference, here's the analogous part of the vscode-lean code.

Can I ask what you're using lean-language-server for?

[Julian Berman]

OK thanks, will have a look. I'm using it to talk to from vim's LSP.

[Julian Berman]

Well, I managed to get this working the caveman way, by taking extra argv and passing it along.

I would have liked to get it working in a more native LSP way, the same way the vscode extension does it (by supporting workspace/configuration requests) but it looks like the version of vscode-languageserver used by lean-language-server is too old, and upgrading to the newest one has other changes that make it not work.

Wish I knew slightly more about LSP than I do I suppose... Will give it one more go maybe tomorrow and if I can't get it to work will give up and do it the easier way.