Li-yao (Sep 14 2021 at 15:33): Li-yao (Sep 14 2021 at 15:33):Somehow my 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?
Karl Palmskog (Sep 14 2021 at 15:34):from memory, you have to also set -Q plugin SimpleIO to get it to install
Karl Palmskog (Sep 14 2021 at 15:34):I have no idea why, I just know that I solved the same problem using that approach
Karl Palmskog (Sep 14 2021 at 15:39):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.
Gaëtan Gilbert (Sep 14 2021 at 15:47):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: Oct 13 2024 at 01:02 UTC