Stream: coq-lsp

Topic: Error messages, locations and paths — an LSP solution?

view this post on Zulip Paolo Giarrusso (Jul 25 2022 at 11:31):

Coq errors use relative pathnames that are not trivial to resolve, unless you know what to resolve them against.
This comes up in both and, and probably elsewhere — I have a sketch fix for the first issue, but @Rudi Grinberg suggested locations might be a blocker. The latter says

We have the usual problem with storing locations that paths are relative to whatever the current directory was when compiling, so for instance says negb is from File "./Datatypes.v", line 69, characters 0-54.
Yes that's another problem, and must be more specified before we merge. How do you think we should solve that?
There is some discussion on Zulip (coq-lsp stream) , for now, I think indeed that the name is actually useless, so indeed we must use the DirPath.t in the location, and call Loadpath to resolve the module name to a filename.

I'd file an issue for reference, but I wouldn't be sure what to write.

view this post on Zulip Rudi Grinberg (Jul 25 2022 at 21:15):

Wouldn't say that locations are a blocker. But it does seem like it would reduce usability

view this post on Zulip Emilio Jesús Gallego Arias (Jul 26 2022 at 15:40):

coq-lsp is aware of the project structure so indeed it can resolve a location to the right file, but indeed that does require project-wide knowledge

Last updated: Feb 06 2023 at 05:03 UTC