Switch from [coq.theory] to [rocq.theory].

[rlepigre-skylabs-ai]

Following the removal of the coq.theory support in dune (see here), something like that will soon be required. Not sure how important it is for you to keep supporting older Rocq @gares.

[gares]

Are the docker images going to be updated (CC @Justme0606)?

[SkySkimmer]

Do not merge before rocq-prover/rocq#21660

[gares]

maybe regenerating rocq-elpi.opam is sufficient to have the docker CI work, but at the cost of recompiling rocq which makes docker useless.

[rlepigre-skylabs-ai]

Not sure I understand what needs to happen for CI, but I pushed a commit that enables project-file generation in the rocq.theory stanzas, which makes the static _CoqProject file obsolete. This also means that in a composed build the flags are adapted according to the workspace (this is the setup we are now using at SkyLabs).

[rlepigre-skylabs-ai]

Note also that after this PR, it should be possible to port most tests to "output tests" (supported in (using rocq 0.12)), which could be pretty nice (much better than cram tests, although I see you removed most of those already).

[yannl35133]

With the release of dune 3.24, (coq.theory 0.8) is not supported anymore, so you can't install rocq-elpi without manually constraining dune. I don't know whether you'd rather do the switch or add a constraint to the dune dependency, but please fix.

[gares]

@rlepigre-skylabs-ai can you rebase so that we re-run ci and merge?

[rlepigre-skylabs-ai]

Seems like there are still some nix issues, but I'm not sure how to fix those.

[gares]

Docker jobs also fail, the problem is that the docker images come with an outdated dune version.
I bumped the dependency in the opam file, maybe it will result in a reinstallation of dune (and rocq, defeating the purpose of docker...).

I think the docker images should be re-generated choosing a version of dune that has both coq and rocq theory stanzas. CC @Justme0606 @Zimmi48

[rlepigre-skylabs-ai]

I tried updating the opam files, and at the same time removed the dummy packages for tests. I don't get the point of them: are they load-bearing an any way?