[rocq] Initial support for the Rocq Prover build language

[ejgallego]

We introduce (lang rocq), a build mode for the Rocq Prover, previously known as "Coq".

The build mode is an exact copy of the (lang coq) mode, renaming the modules, data, and some global declarations. Also, the default implicit lib is now named Corelib.

(lang coq) should be considered deprecated / frozen, and eventually removed.

There are many cleanups and improvements possible, in particular we have done, in separate commits:

• removed support for older legacy coq modes
• removed support for legacy plugin handling
• removed the need for coq-* shims

All of the tests have been ported and manually verified to work (a time consuming process) As of today, all test pass.

Future work:

• support new extraction option (-output-directory)
• improve composition with local rocq as in (lang coq), as of today the rocqworker is not injected as a dependency
• nix CI + develop
• forward port _RocqProject generation
• forward port rocqdoc headers work
• forward port per_module fixes
• cosmetic, turn rocq into rocq compile for --display=short
• [CI] Remove dependency on rocq-stdlib, only extraction tests need that

Closes #11572

Joint work with Li-yao Xia.

[rlepigre-skylabs-ai]

I just learned that you are working on this @ejgallego, that's great news!

There are several points that are IMO worth discussing before merging this PR:

• Should we integrate the _CoqProject generation PR (Generate "_CoqProject" files for Coq theories #11752)?
• To more easily support the above, should we remove per-module flags? (IMO they are kind of useless.)
• Similarly, should we enforce at most one theory stanza per directory? (I personally always do that, can't imagine this breaking too much stuff.)
• Should we sort out the .vos / .vok mess?
• Should we integrate Add "coqdoc_header" and "coqdoc_footer" fields. #11131?

Also, I'm happy to play a part in this if you want help.

[rlepigre-skylabs-ai]

Another candidate is going back to calling rocq dep on all files, instead of per-theory.

[ejgallego]

Hey @rlepigre-skylabs-ai !

I just learned that you are working on this @ejgallego, that's great news!

Indeed! Thanks a lot for your message. We got side-tracked by other stuff, but the idea is to merge this and #11945

There are several points that are IMO worth discussing before merging this PR:

• Should we integrate the _CoqProject generation PR (Generate "_CoqProject" files for Coq theories #11752)?

Yes, we will forward port this in a separate PR.

• To more easily support the above, should we remove per-module flags? (IMO they are kind of useless.)

IMHO we can just say that both can't work together, there are some folks trying to use this feature, so I'd like to keep it.

• Similarly, should we enforce at most one theory stanza per directory? (I personally always do that, can't imagine this breaking too much stuff.)

This would certainly break a lot of stuff tho, what would we gain?

• Should we sort out the .vos / .vok mess?

Happy to work on this but IMHO we can do in a separate PR.

• Should we integrate Add "coqdoc_header" and "coqdoc_footer" fields. #11131?

Yes, we will also forward port this.

Also, I'm happy to play a part in this if you want help.

Absolutely, @Lysxia and I will send a mail soon to coordiante.

Another candidate is going back to calling rocq dep on all files, instead of per-theory.

This should be easy to do if we want, tho for some users it would mean a large performance regression. But IMHO unrelated to this PR which is to enable Rocq users no to have to depend on the coq-* compatibility wrappers.

[rlepigre-skylabs-ai]

This should be easy to do if we want, tho for some users it would mean a large performance regression. But IMHO unrelated to this PR which is to enable Rocq users no to have to depend on the coq-* compatibility wrappers.

I think this was originally due to performance issues in coqdep that have now kind of been fixed, but I could be wrong. For us, at this point, this would be a performance improvement I believe.

[ejgallego]

I think this was originally due to performance issues in coqdep that have now kind of been fixed, but I could be wrong.

Do you have pointer? The original performance problem is that in one rocqdep call per file, rocqdep will still scan the whole user-contrib tree. This has a huge impact in practice, even in fast systems like Linux.

For us, at this point, this would be a performance improvement I believe.

I'd be happy to make this configurable, the original Coq mode used this system so it is easy just to look at the commit and add back that code with a flag.

Once we have that we could test for numbers, but my original experiments showed a large overhead of repeated rocqdep calls.

[rlepigre-skylabs-ai]

Do you have pointer? The original performance problem is that in one rocqdep call per file, rocqdep will still scan the whole user-contrib tree. This has a huge impact in practice, even in fast systems like Linux.

I can't find anything, but I thought I had seen something in that line.

If that wasn't the case, then perhaps coqdep should be fixed to scan it more lazily, or we should try to push for getting rid of user-contrib entirely.

[SkySkimmer]

coqdep called by dune (ie with -boot) should not be scanning all user-contrib but only the parts which are mapped to a declared dependency

[rlepigre-skylabs-ai]

Are we actually certain that duplicating everything is the right option to support rocq? It seems to me like we could keep the same language but allow for an alias, and make the change more gradual? That being said, it looks like a lot of work went into this PR already. I'm just worried that it's gonna be supper hard to get this in.

[ejgallego]

Are we actually certain that duplicating everything is the right option to support rocq?

I am.

It seems to me like we could keep the same language but allow for an alias, and make the change more gradual?

I tried that, but it is actually quite complex, a lot of cases to handle, a lot of different tests, conditional arguments. The breakage is far from trivial.

That being said, it looks like a lot of work went into this PR already. I'm just worried that it's gonna be supper hard to get this in.

What is your worry?

[rlepigre-skylabs-ai]

What is your worry?

My main worry is asking everyone to move to a new language, for what appears to me to be not a good reason. We'll basically ask people to modify every single of their dune / dune-project files, which seems annoying.

[ejgallego]

My main worry is asking everyone to move to a new language, for what appears to me to be not a good reason. We'll basically ask people to modify every single of their dune / dune-project files, which seems annoying.

They'll have to do that anyways due to the several improvements in Rocq mode, we would have introduced a new (lang coq ) version anyways, so IMHO bumping (lang coq 0.10) to (lang coq 0.11) is not too far from changing it to (lang rocq 0.11).