LSP lakefile discovery uses PWD but should use LSP workspace

Stream: lean4

[Christopher Lang]

I'm adding some basic lean lsp support to the kakoune text editor. The relevant kak-lsp PR is here.

Problem is that lake serve and lean --serve seem to be using their present working directory to find lakefile.{toml,lean} and not the workspace folder transmitted via LSP. Is this intentional? AFAIK other LSP's do not rely on the working directory they are started in.

[Marc Huisinga]

Yes, this is intentional. Note that we don't set the workspaceFolders server capability, either.

[Julian Berman]

I don't recall having any issue with neovim here. Presumably rootUri is still supported by Lean? I believe that's what we ultimately are setting by setting root_dir in nvim. Does kakoune (or your PR) not set that?

[Marc Huisinga]

Julian Berman said:

Presumably rootUri is still supported by Lean?

It isn't. We just use the cwd.

[Julian Berman]

Huh. Interesing, I don't think we actually set any different working directory in neovim, let's see if nvim execs the process by default in the directory we pass but its docs seem to suggest it doesn't.

[Christopher Lang]

Is there any reason rootUri isnt supported? Would it not be better to use rootUri over cwd in order to be more consistent with how other LSPs are implemented?

If there is no plan to use rootUri in the future than can I suggest a comment is added to Data/Lsp/InitShutdown.lean to explain. I feel that the current structure definition implies that rootUri is supported because of the commented out rootPath directly above:

structure InitializeParams where
  processId? : Option Int := none
  clientInfo? : Option ClientInfo := none
  /- We don't support the deprecated rootPath
  (rootPath? : Option String) -/
  rootUri? : Option String := none
  initializationOptions? : Option InitializationOptions := none
  capabilities : ClientCapabilities
  /-- If omitted, we default to off. -/
  trace : Trace := Trace.off
  workspaceFolders? : Option (Array WorkspaceFolder) := none
  deriving ToJson

[Marc Huisinga]

Sure, happy to add a comment to that structure and a note to our protocol overview that attempts to document all of our LSP protocol violations and extensions.