[coq] [coq-lang-1.0] Ensure test suite is comprehensive.

[ejgallego]

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.

[Alizter]

Regarding the naming, if we separate tests by directories then that won't be too much of a problem.

[ejgallego]

Regarding the naming, if we separate tests by directories then that won't be too much of a problem.

How would such directories be named? What I mean by naming scheme is a directory / test name that allows us to understand what variables on the matrix are covered.

[palmskog]

Some use cases we have in Coq-community and I have myself:

• Coq library / extraction / plugin: a Coq theory is used as the basis for code extracted to OCaml, and the OCaml code is used inside a Coq plugin (that has Coq theories). Exemplified by Stalmarck
• Monorepo Coq library: multiple Coq theories with different logical path prefixes live in the same codebase but in different packages, where some packages depend on other packages. Exemplified by Hydras & Co.
• Coq library / extraction / OCaml tool: a Coq theory is used as the basis for code extracted to OCaml, and the OCaml code is linked with other OCaml libraries to produce an executable

[palmskog]

I think we can add the use case where I discovered #8042:

• Coq library / multiple extracted modules / multiple executables

Specifically, in Chapar, there are three different key-value store executables produced from three different Coq modules. However, those executables share the same OCaml infrastructure/libraries, so it makes sense for them to be defined in the same dune file.

[ejgallego]

Yes @palmskog , we would like to fix #8042