Paolo Giarrusso (Jul 25 2022 at 11:31): 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 https://github.com/ocaml/dune/issues/6005 and https://github.com/coq/coq/pull/16261, 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 gitlab.com/coq/coq/-/jobs/2668453330#L4464 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.
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
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