Rocq support in dune

[mattam82]

Desired Behavior

We would like dune's Coq support to be able to call the new rocq binary instead of coqc.
Currently we need to use compatibility shims (opam package coq-core) on top of the rocq-core package to compile Rocq projects.
Ideally we want a solution that's compatible with both coqc and rocq usage.

Example

Dune coq support just fails if coqc is not installed right now.

Discussion

We are currently discussing the various design decisions regarding Rocq <-> dune integration here, and plan to contribute a solution. This issue hence for letting you know we're working on it and soliciting feedback if you have any:

https://rocq-prover.zulipchat.com/#narrow/channel/240550-Dune-devs-.26-users/topic/Dune.20support.20for.20rocq.20binary/with/508283855

[SkySkimmer]

We would like dune's Coq support to be able to call the new rocq binary instead of coqc.

(and also instead of coqdep)

[ejgallego]

Thanks for opening the issue @mattam82 , a couple of comments:

• we can just check Rocq/Coq version and replace coqc by rocq
• version detection code is in src/dune_rules/coq/coq_config.ml, we need to figure out a stable set of rules to properly detect the version, I guess we can first query to see if rocq binary is in scope, then call rocqc --version, other than that we fallback to coqc --version, then if not found we complain about "no Rocq"
  We need to be careful to consider the cases where:
  • rocq / coqc are in the same workspace
  • one of the two is in the local workspace, the other is globally installed
  • of course the simple cases where only one is in the local or global workspace
  • beware of strange cases like rocqworker and rocq for some reason not living in the same space

Note about rocq vs rocqworker

After Rocq 9.0, the public entry point to Rocq is the rocq binary, however this binary is just a shell and it depends on the rocqworker binary, which is private. This means we cannot just replace coqc by rocq, but we need to add an extra dependency to rocqworker.

It seems Rocq devs added a patch to coqdep so it outputs a dependency on rocqworker by itself, I'm unsure how this can work on composed builds, needs some analysis to see what is going on.

In any case, using rocq compile would imply that each .vo file now depends on two binaries instead of one, which the consequent overhead in the build graph. I'd be good to measure the overhead at some point just to be sure it is not a problem in large-scale developments.

An easy trick is just to have dune find rocqworker directly and skip the shim, but that may not be acceptable to Rocq upstream.

[ejgallego]

Another idea I just had while cooking, maybe we could just use the Rocq language versioning to implement this, thus:

• We declare (lang coq 0.9) to be the last version, and we introduce (lang rocq 0.1)
• Patch is now trivial (modulo the possible build graph perf issue)

I think I like this idea, thoughts? cc @Alizter @rlepigre @palmskog

Main drawback is that it would prevent dune packages from having a common source build for Coq / Rocq projects

[palmskog]

I think a solution with (lang rocq 0.1) is reasonable. But then I currently try to only use Dune builds in CI, not in packaging in the opam archive and so on.

[nojb]

From a distance, I think coq and rocq should be considered synonyms inside Dune (with rocq preferred by default and in the documentation). Semantically, Dune should always try to locate rocq first and use that if found. Otherwise, try coq as today.

Is there any situation for which the above strategy would not be enough?

This means we cannot just replace coqc by rocq, but we need to add an extra dependency to rocqworker.

I am not sure I follow: how is this different from the relation between gcc and cc1? We don't declare a dependency on cc1...

[ejgallego]

Is there any situation for which the above strategy would not be enough?

That was the original plan, but it is quite a bit more work than this second idea. But indeed, I agree with you, if we can find the cycles to implement the better auto-detection plan, we should do it.

I am not sure I follow: how is this different from the relation between gcc and cc1? We don't declare a dependency on cc1...

In the Rocq would is very common to vendor Rocq itself.

Rocq 9.0 moved from coqc to a "shim" rocq which then calls rocqworker for compilation needs.

rocqworker interface is private, and the rocq binary doesn't depend on rocqworker, thus we need to add an extra dep graph as now the compilation of .vo files requires these two binaries to be up to date.

[SkySkimmer]

Note that coqc in 9.0 is also a shim calling rocqworker.
Also in <9 running coqc could call coqtacticworker even though dune wasn't aware of the dep

Another idea I just had while cooking, maybe we could just use the Rocq language versioning to implement this, thus:

People who keep using older versions of coq because of the transitive dep behaviour would probably not be too happy about this.