This MR realizes multi-package repositories: from the Iris repository, this releases a coq-iris package with everything except for HeapLang, and a coq-iris-heap-lang package with HeapLang itself. I already landed the required changes in the rest of the infrastructure (CI scripts and automatic opam publishing), this is the Iris part. This is just an example, we can of course change what we separate how -- but it seemed like the most obvious first split.
For each package, there is a corresponding Coq project (iris and iris_heap_lang) with a separate _CoqProject.PROJECT file, which is generated on-demand from the main _CoqProject file. This means emacs and coqide treat the entire repository as a single project, and do fine-grained dependency tracking even across packages.
We also need one opam file for each package, PACKAGE.opam, which is hooked up to the right _CoqProject file via the new make-package script. This script does not run any tests (as tests are not associated with packages), so tests will no longer be run on opam install.
The files for each project are in PROJECT/, which is why this MR renames almost everything. It turns out we can even install HeapLang as a submodule of the Iris package, so the imports are all compatible. (That will probably work less well for splitting out algebra/, bi/, proofmode/; I am not sure if a package can have "multiple roots" and even if it can I am not sure if that is something we want to do).
Coqdoc is generated for the entire repository at once, we'll have to see how well that looks.