Stream: Dune devs & users

Topic: Can public Coq theories depend on private OCaml libraries

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.

Last updated: Feb 04 2023 at 02:03 UTC