Clarify and check the dependency policy for packages depending on new Rocq packages

[mattam82]

It seems there is an agreement we should check that nothing depends on the rocq-prover package but rather on rocq-runtime/rocq-stdilb and optionally the compatibility coq packages. Is there such an agreement?

If so, we should write as part of linting a check that we don't intoduce such dependencies.

[SkySkimmer]

There are also packages depending on rocq-core.
For packages depending on rocq-stdlib I guess they may also want to depend on one of rocq-runtime and rocq-core to fix the version, IDK if one or the other should be preferred.

[mattam82]

Yep, there is definitely some leeway.

[mattam82]

Adding two dependency lines is ok I guess, it's exactly the kind of freedom a separated stdlib gives us. Should we advise to use rocq-core + rocq-stdlib at >= "9.0~" & != "9.0.dev & < "10" with the != 9.0.dev constraint core-dev compat. I'm not sure we need the upper bound (?).

[mattam82]

Maybe rocq-core < 9.1 even if there's some ML code involved?

[mattam82]

@silene @palmskog @gares what do you think? I can write some guidelines in the README based on what we decide here, and link from Rocq 9.0's changelog to give advice to users about porting coq/coq#20168