Enrico Tassi (Feb 01 2022 at 15:52): 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)?
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.
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
Enrico Tassi (Feb 01 2022 at 16:42):reuse the loadpath, and add a From clause to elpi file loading directives
Last updated: Dec 07 2023 at 09:01 UTC