Stream: Dune devs & users

Topic: Can public Coq theories depend on private OCaml libraries?


view this post on Zulip Paolo Giarrusso (Jul 10 2022 at 15:44):

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.

view this post on Zulip Paolo Giarrusso (Jul 10 2022 at 16:02):

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.

view this post on Zulip Ali Caglayan (Jul 10 2022 at 17:57):

Public theories can only depend on public OCaml libraries

view this post on Zulip Ali Caglayan (Jul 10 2022 at 17:59):

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.

view this post on Zulip Ali Caglayan (Jul 10 2022 at 17:59):

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.

view this post on Zulip Ali Caglayan (Jul 10 2022 at 18:01):

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.

view this post on Zulip Ali Caglayan (Jul 10 2022 at 18:03):

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.

view this post on Zulip Ali Caglayan (Jul 10 2022 at 18:13):

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.

view this post on Zulip Paolo Giarrusso (Jul 10 2022 at 22:10):

Yeah, that fits with what I suspected

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 14:18):

We can have private plugins, we just need someone to implement that

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 14:18):

as of now we still rely on the legacy plugin system

view this post on Zulip Ali Caglayan (Jul 11 2022 at 14:54):

Emilio Jesús Gallego Arias said:

We can have private plugins, we just need someone to implement that

*we could have

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 15:14):

please do _not_ treat the above as a feature request

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 15:15):

I'm just exploring what's possible, and I don't know what's sensible

view this post on Zulip Ali Caglayan (Jul 11 2022 at 15:18):

The ability to load private OCaml code (in a private theory) seems to be a sensible use case to me.

view this post on Zulip Ali Caglayan (Jul 11 2022 at 15:18):

But this will require modifying Coq in a way which I am not so comfortable with at the moment.

view this post on Zulip Ali Caglayan (Jul 11 2022 at 15:19):

Somebody who knows what they are doing would need to write something, but those are in short supply. :shrug:

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:21):

I don't think we need to modify Coq

view this post on Zulip Ali Caglayan (Jul 11 2022 at 15:21):

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.

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 15:21):

my vote is still for vos/vok first

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:21):

to support a private plugin, we only need dune to extend OCAMPATH with a pointer $build_context/.lib/

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:22):

Paolo Giarrusso said:

my vote is still for vos/vok first

that's not hard, let's coordinate in Rudi's PR

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:22):

tho vok is a bit tricky

view this post on Zulip Ali Caglayan (Jul 11 2022 at 15:22):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:22):

but for .vos we already handle that in coq_dune

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:23):

so for public plugins, Dune already sets the loadpath ok, and we can just depend on isntall/lib/foo/META and the cmxs

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:23):

as it won't be an absolute path we won't hit the bug we are hitting now due to coqdep

view this post on Zulip Rudi Grinberg (Jul 11 2022 at 16:44):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 17:19):

Indeed, and to place the META there


Last updated: Oct 13 2024 at 01:02 UTC