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)?
Why not look for the root of the project? And if there is none, just use the current directory.
as in look for dune-project, or Make or _CoqProject...
I think I received a better suggestion in the elpi stream
reuse the loadpath, and add a From clause to elpi file loading directives
Last updated: Dec 07 2023 at 09:01 UTC