main idea: use findlib rather than puting everythin in a single user-contrib directory
not much interaction yet in the PR, feel free to ahve a look / discuss it
currently things not very clean when two packages share a common path
in current proposition, multiple packages are not forbidden to use a common prefix, shouldn't be an issue (outside of actual conflicts with exact same path&filename)
have a rocq find (wrapper to ocamlfind) that would output the correct syntax with all the -Q (c.f., small prototype in the PR)
multiple people in favor of doing it
what's the future of findlib? (no strong concern though)
rocq makefile will need some adaptation (maybe some syntax similar to ocaml findlib packages for plugins)
metarocq, still using rocq makefile may be a good test
what about backward compat in dune?
rocq makefile could be adapted by Enrico during next Rocq'n'share
plan:
rocq find and other changes so that it work "by hand" (Rodolphe)
dune (Rodolphe) and rocq makefile can then be done in parallel
Support for .vos / .vok in dune
empty files are painful for dune
Gaëtan to stop generating empty files and adapt rocq makefile to create the empty files
Policy around CODEOWNERS
the file is in need of some care
-> Yann to open PR and ask people if they agree with the changes related to them