Stream: Coq devs & plugin devs

Topic: API to know the current file name


view this post on Zulip Enrico Tassi (Feb 01 2022 at 15:52):

In elpi I have a command to read external files. It turns out that while coqc and coqidetop do run from where you start them, eg the root of your project, PG starts coqtop from the directory where the .v file is.

One way to skin the cat would be to use paths relative to the .v file (or in absence of it, to . as it is currently). The STM is initialized by passing it the .v file path, if any, but there is API to access it after the facts. I can expose a new API, but that would be for 8.16.

Any other ways to know that path (which works in 8.15)?

view this post on Zulip Guillaume Melquiond (Feb 01 2022 at 16:21):

Why not look for the root of the project? And if there is none, just use the current directory.

view this post on Zulip Enrico Tassi (Feb 01 2022 at 16:42):

as in look for dune-project, or Make or _CoqProject...
I think I received a better suggestion in the elpi stream

view this post on Zulip Enrico Tassi (Feb 01 2022 at 16:42):

reuse the loadpath, and add a From clause to elpi file loading directives


Last updated: Mar 28 2024 at 21:01 UTC