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

[proux01]

We could also check that a package named rocq-* does not depend on any coq-*

[silene]

That seems counterproductive. It would prevent people from switching to Rocq until dependencies out of their control have done so.

[silene]

Adding two dependency lines is ok I guess, it's exactly the kind of freedom a separated stdlib gives us.

Yes. It is not different from having an explicit dependency on ocaml in standard Opam packages, despite the compiler always being available.

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 (?).

I think none of the above constraints are useful. The lower bound is redundant; the upper bound is 20 years into the future; and the disabling of 9.0.dev is just annoying.

The exception, as you mentioned, is rocq-core < 9.1 for packages providing plugins.

[palmskog]

I agree that we should allow rocq-* depending on some coq-* for the time being.

But generally I'm a bit puzzled what the actual proposal is, could you give some small concrete examples of what we might recommend @mattam82? I think our users would need this in any case.

[proux01]

That seems counterproductive. It would prevent people from switching to Rocq until dependencies out of their control have done so.

Well then, then they can't claim they switched to rocq (I mean, they can do it locally but the package manager doesn't provide any way to check it, except maybe with build-only dependencies in the dependencies?).

[silene]

Well then, then they can't claim they switched to rocq

I am confused. What is your definition of switching to Rocq? If a project is using rocq makefile and the like, it would certainly look to me like it has switched to Rocq.

[proux01]

We agree on that. But in practice, to be able to actually fully build without the coq compat shim, you need all your dependencies to also do so. Sure you could build the dependency with the compat shim, then remove it, but that seems tricky to check. Except maybe if we require the dependency to list the compat shim as a build-only dep? And even then I'm not sure how CI could actually enforce that. And we all know anything not enforced in CI is bound to be rapidly broken.

[silene]

Again, if the build section of a package is rocq makefile ; make and yet the package is somehow using the compatibility shim, then the bug is not in the package, it is in Rocq!

[proux01]

Sure but your assumption is not trivially checkable in the CI. We could have a rule like "don't depend on coq-* except if your build statement is just rocq makefile; make" but that seems overly complicated.

[SkySkimmer]

The rule should just be "if your package is named rocq- then don't depend on the compat only packages"
where compat only packages are coq-core, coq-stdlib, coq, and maybe any package coq-foo where rocq-foo also exists