Retrieve actual path in vscode

Stream: lean4

[Xubai Wang]

Currently when we use Context.fileName (← read) in TermElabM, the VSCode extension return "<input>" rather than the file's actual path, which lead to the errors shown in the screen capture.

screen capture

Can we switch to actual path, or is there any alternative way to retrieve FilePath of current file?

[Mac]

Does this work when the file is elaborated directly with lean? I suspect the problem is that the Lean LSP is not setting the fileName of the Context to the file being interactively elaborated.

[Xubai Wang]

It builds with lake. so the problem is from LSP. "<input>" is used instead of actual file name in Lean.Server

[Sebastian Ullrich]

Should be fixed with https://github.com/leanprover/lean4/commit/6c6f66b812e009d74a2021674bac842543b40ca0, please give it a try