Coq: [api] Define private modules

[ejgallego]

Dune offers the ability to declare some modules private to a particular library with (private_modules ...). This has two effects: the modules won't be available outside the library, and the API documentation won't include them [by default].

IMHO the maintainer of each library should declare what modules shouldn't be available outside the lib itself. TODO:

• kernel: @maximedenes @ppedrot @SkySkimmer
• library: @silene @gares
• engine: @ppedrot @SkySkimmer
• pretyping: @mattam82 @gares
• interp: @herbelin @ejgallego
• parsing: @herbelin @mattam82
• proofs: @ppedrot @Zimmi48
• stm: @gares @ejgallego
• vernac: @mattam82 @maximedenes
• toplevel: @ejgallego @gares
• ltac: @ppedrot @herbelin

[gares]

Does it also provide the dual keyword? If so I think it should be preferred since new files may appear in a directory and sneak into the api

[ejgallego]

Does it also provide the dual keyword? If so I think it should be preferred since new files may appear in a directory and sneak into the api

That's a good point; I think the plan is that Dune will have all the modules private by default and indeed will require to use public_modules to make them visible; as of today, and by compatibility with most existing workflows, new modules default to public.

[gares]

Would it be reasonable to wait to merge this until there is a way to make modules private by default? Is it a feature already planned? (they release so often)

[ejgallego]

Sure, this will have to wait quite a bit anyways due what the dependencies are.

Corresponding Dune issues are https://github.com/ocaml/dune/issues/1476 and https://github.com/ocaml/dune/issues/1478 .

But note indeed that the current default works very well for Coq. Surprisingly there are very few modules that can be made private in the current codebase. If the default would be reverted, we would have to manually declare dozen of modules. I am surprised but indeed most modules are really needed by plugins. We have a huge API.