Concretely, once I've made a Coq theory public by adding (package foo)
(where foo.opam
exists), plugins aren't found any more unless I make the plugins into public libraries via public_name
(as in the example). That makes some sense, but I was wondering whether making plugins into private libraries should be enough? That might be nonsense if you understand the implementation (e.g. maybe findlib
can't load private libraries), but I don't really OCaml :-|
OCaml docs say:
(package <package>) installs a private [OCaml] library under the specified package. Such a library is now usable by public libraries defined in the same project.
OTOH the Coq docs make a different choice:
A private [Coq] theory may depend on both private and public theories; however, a public theory may only depend on other public theories.
A smaller matter: it seems that, after adding public_name foo.libname
, using (libraries libname)
still works when declaring OCaml libraries, but Coq theories must switch to (libraries foo.libname)
as demonstrated here: https://github.com/ejgallego/coq-plugin-template/blob/c0cc512a43e170d8843d7d7fb2310def8e2c3b66/theories/dune#L10.
Public theories can only depend on public OCaml libraries
Since the OCaml library has to be available to Coq in order to run a library, you can imagine that installing a public Coq theory that depended on a private OCaml library (which won't be installed) would cause Coq to not work.
However you can "sort of do the opposite" which is have a private theory which gets extracted to a public OCaml library. This could be useful for privately checking an implementation for instance.
The install layout of Coq means that we can't replicate OCaml's "private install feature" since we don't really have a place to put the source.
Regarding your final point, you must put the public_name of your OCaml library in your coq.theory libraries field. The fact that private names were accepted before was a bug. By the way, the libraries field of coq.theory has been renamed in 3.4 to plugins.
Another way to think about it is this: If somebody wants to run your Coq code, they will need to load your plugin for it to work. Having that plugin be private doesn't let them do that.
Yeah, that fits with what I suspected
We can have private plugins, we just need someone to implement that
as of now we still rely on the legacy plugin system
Emilio Jesús Gallego Arias said:
We can have private plugins, we just need someone to implement that
*we could have
please do _not_ treat the above as a feature request
I'm just exploring what's possible, and I don't know what's sensible
The ability to load private OCaml code (in a private theory) seems to be a sensible use case to me.
But this will require modifying Coq in a way which I am not so comfortable with at the moment.
Somebody who knows what they are doing would need to write something, but those are in short supply. :shrug:
I don't think we need to modify Coq
Coq plugins today have to be public with the new loading mechanism due to the round trip of going to the META file to find out where the cmxs live. The legacy plugin loading system doesn't need to do this AFAIK, but it is confusing keeping both around tbh.
my vote is still for vos/vok
first
to support a private plugin, we only need dune to extend OCAMPATH
with a pointer $build_context/.lib/
Paolo Giarrusso said:
my vote is still for
vos/vok
first
that's not hard, let's coordinate in Rudi's PR
tho vok is a bit tricky
Paolo Giarrusso said:
my vote is still for
vos/vok
first
Would you like to discuss this in a separate thread, I would be willing to push this along.
but for .vos we already handle that in coq_dune
so for public plugins, Dune already sets the loadpath ok, and we can just depend on isntall/lib/foo/META and the cmxs
as it won't be an absolute path we won't hit the bug we are hitting now due to coqdep
Emilio Jesús Gallego Arias said:
to support a private plugin, we only need dune to extend
OCAMPATH
with a pointer$build_context/.lib/
And to generate META files for private libraries.
Indeed, and to place the META there
Last updated: Oct 13 2024 at 01:02 UTC