plugin/plugin.mlpack file gets installed when I have
-R src SimpleIO -I plugin, but not when I have
-Q src SimpleIO -I plugin (I get
SKIP ... since it has no logical path). What gives?
from memory, you have to also set
-Q plugin SimpleIO to get it to install
I have no idea why, I just know that I solved the same problem using that approach
maybe @Emilio Jesús Gallego Arias can explain, I'm pretty sure he has looked at that code and it may be why he insists on
-R in Dune.
I guess coq_makefile assumes that the current project is the one using -R
indeed we can see
$ coq_makefile -destination-of plugin/kappa.cmxs -R theories Potato -I plugin Potato/ $ coq_makefile -destination-of plugin/kappa.cmxs -Q theories Potato -I plugin $ # ^ no output $ coq_makefile -destination-of plugin/kappa.cmxs -Q plugin Potato # optionally -I plugin Potato/
ah, so it's limited to coq_makefile. I thought there was some querying of paths inside Coq going on.
Last updated: Jun 09 2023 at 08:01 UTC