[coq] 1.0 version coq language version meta-issue

[ejgallego]

Here is a list of missing items toward a (using coq 1.0) beta and stable release.

I separated issues on two kinds: issues that need to be resolved before we can do a wide call for testing / porting in the Coq community, and issues that are required for 1.0 but not for the beta.

Beta-blocking issues:

• inter-scope composition of theories, including support for installed theories (so people can port opam packages to Dune)
  c.f feature(coq): support for interproject composition of theories #5784 and maybe some extra PR
• Better coq native support ([coq] Improve support for Coq's native compiler #5831)

With the above in place, quite a lot of packages could be permanently ported to Dune and release in opam this way.

For 1.0, it'd be nice to have too:

• Add a %{coq_version} variable so people can have conditional copy rules for those that need compat with older Coq feature(coq): coq macro #6049
• coqchk support
• check that our coqdoc system is OK for usres
• sharing of (include_subdirs ...) between Coq and OCaml is quite inconvenient for a few users c.f. Decouple qualified/unqualified from including subdirectories #3314 Mixing coq and ml files in the same directory #2857
• Allow to have a coq.extraction and coq.theory in the same directory #4158
• resolve [coq] -R flag by default #2585

[ejgallego]

Also #3486 , a more general question is how different Coq build modes (for example quick) are going to be supported in Dune. It seems that this is something really needed for 1.0, so we may need to figure out how to better integrate them into Dune profiles or a similar mechanism.

[ejgallego]

Updated to reflect current status of affairs.