Stream: Coq devs & plugin devs

Topic: Installing plugin requires -R ?


view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Sep 14 2021 at 15:34):

from memory, you have to also set -Q plugin SimpleIO to get it to install

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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/

view this post on Zulip Karl Palmskog (Sep 14 2021 at 15:51):

ah, so it's limited to coq_makefile. I thought there was some querying of paths inside Coq going on.


Last updated: Oct 16 2021 at 07:02 UTC