Clarify structure

[proux01]

This implements, together with coq/coq#19530 , the part of CEP#83 that reached a common agreement during the dedicated Coq call discussions (tl;dr: give stdlib its own repository, clarify its internal dependencies and ensure they are kept with a CI check, "coq" metapackage keeps depending on "coq-stdlib" and no distribution of packages for induvidual subcomponents)

• split code in stdlib into subcomponents, according to the CEP
  added graph in doc/stdib/depends.png, included in doc/stdlib/index.html
• add CI checks
  • job checking for no duplicate filenames
  • job stdlib-subcomponents checking subcomponents dependencies (easy thanks to Nix)
  • job checking that all files are in exactly one subcomponent

Look at dev/doc/structure.md for more details.

[proux01]

Due to the extreme strictness of dune (in particular the fact that (include_subdirs unqualified) never got implemented for Coq), I gave up on my attempts to improve the directory structure of the library, while remaining highly backwards compatible. So this is just documenting some structure and adding a CI job to ensure this documentation remains up to date. The chosen structure may not be perfect, but since we are not publishing any package, it can be easily refined later (c.f. dev/doc/structure.md).

[SkySkimmer]

WTF are all these added new files? Why is there a committed generated file (the .dot)?

[proux01]

WTF are all these added new files?

Just symlinks needed by the CI job (and ignored by dune) to check the subcomponents structure. Since dune forbids to change the directory structure without chaning the logical names (i.e. having some impact in terms of backward compatibility), those are needed for the CI job (based on coq_makefile) to compile parts of some directories in different subcomponents. (it's all documented in dev/doc/structure.md)

Why is there a committed generated file (the .dot)?

It's not entirely generated, in particular the compat subcomponent doesn't actually depend on everything (according to coqdep), but we want to declare it as possibly depending from everything, because any future compat file could add a dependency on virtually anything.