Before (coq lang 1.0) we need to ensure that we are testing all possible configurations of Coq Dune projects.

It seems there are quite a few, let's study the variables:

• composition: single theory, multiple same-scope ones, multiple theories in multiple workspaces
• Coq: not present, in workspace, installed
• stdlib present: no, in workspace, installed
• user-contrib: no, installed
• coqpath: yes / no
• stdlib flag: yes / no
• theories visibility: public and private, can depend in 3 different ways x 2 different configurations (same / different scope)
• native: enabled / disabled in config, manually overriden.
• plugins: no / yes single module / yes depending on other libs
• plugins: living in coqpath without findlib registration / with findlib registration
• transitive deps: both in worksspace and in user-contrib
• Coq versions: maybe 8.13 / 8.16 / 8.17 ?
• library names: different kind of overlappings

That's a lot of combos to test, but can be reduced with a bit of care.

Another point to consider is how to have a naming scheme that help us identify what part of the test matrix the test is covering.