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