[DO NOT MERGE] Port to Rocq master

[mattam82]

This PR adapts the proof scripts to latest Rocq / mathcomp master. I propose it because I would like to put CertiRocq in the CI, which has a Wasm backend relying on WasmCert. That would hence mean putting WasmCert in the CI as well. Are you ok/interested in that? The usual setup for Rocq projects in Rocq's CI is to have the master branch follow Rocq master, with potentially different branches like 9.0, 9.1 etc if code needs to be version specific. One can also use a specific e.g. rocq-master branch solely used for the Rocq CI, and periodically update it from one's master branch that rather depends on a released Rocq (easier for contributors). For these particular changes (due to SsrOldRewriteOrder changing in mathcomp master and the upcoming mathcomp release), I think it should be backwards compat (although the rewrite change in contexts.v seems a bit more subtle).

[raoxiaojia]

I'd be happy to put WasmCert in the CI. IMO having a separate rocq-master is better in the long term, and I presume it will also make our GitHub CI for master easier, unless the rocq-community docker CI has a dev version.

There's currently a small blocker on the parser combinators library (Parseque) which has yet been upgraded to 9.1 (merely an opam release issue). I guess that means Parseque needs to brought into the CI as well (@womeier ).

[womeier]

the current release of rocq-parseque (version 0.3.0) is already compatible with Rocq 9.1, just need to wait for rocq-prover/opam#3690 to be merged.

is there anything else I should do?

[mattam82]

@womeier is parseque#master also compatible with Rocq master?

[mattam82]

If so, could you add rocq-parseque.dev to Rocq's opam/extra-dev ? We can then push a coq-wasm.dev package depending on it.

[womeier]

@womeier is parseque#master also compatible with Rocq master?

yes! The PR is ready I think: rocq-prover/opam#3691
@mattam82

[mattam82]

I'd be happy to put WasmCert in the CI. IMO having a separate rocq-master is better in the long term, and I presume it will also make our GitHub CI for master easier, unless the rocq-community docker CI has a dev version.

It does have an image tagged 'dev' following Rocq's master. There seems to be only a limited amount of ML code here, and nothing relying on Rocq's API, right? If so I think you can expect little breakage from working directly on Rocq's master (in the CI at least), but having a separate rocq-master branch also has its advantages if anything not backward compatible is done on Rocq's master. Do as you prefer, just tell me which branch I should point to for the coq-wasm.dev package :)

[mattam82]

We can then undraft rocq-prover/opam#3693

[raoxiaojia]

Thanks -- I'll make a rocq-master branch based on your branch here. Should I change anything in the opam files (I presume I need to bump the version of some dependencies)?

Upd: made a rocq-master branch that directly mirrors the current state of this branch.

[mattam82]

Coming back to this. Thanks for the changes, I'll try to merge the dev package now.

[mattam82]

@raoxiaojia sorry to bother you, but it seems some changes in rocq#master broke the rocq-master branch: https://gitlab.inria.fr/coq/opam-repositories/-/jobs/7465369

[raoxiaojia]

@raoxiaojia sorry to bother you, but it seems some changes in rocq#master broke the rocq-master branch: https://gitlab.inria.fr/coq/opam-repositories/-/jobs/7465369

Thanks for the message! I'll take a look when I get home later today.

[raoxiaojia]

File "./Interpreter.v", line 177, characters 0-622:
Warning: This interactive proof is not started by the "Proof" command.
[missing-proof-command,fragile,default]
File "./Interpreter.v", line 194, characters 0-6:
Error: "Proof" must be the first command in an interactive proof.

This is quite weird, we don't even have any interpreter.v file in the current codebase (iirc that file was retired back in 2023 or so). I'm checking the build log to understand what it is actually trying to compile.

[raoxiaojia]

=== ERROR while compiling coq-menhirlib.20250912 =============================#
context 2.1.2 | linux/x86_64 | ocaml-base-compiler.4.14.2 | file:///builds/coq/opam-repositories/released
path ~/opam-root-4.14.2-2.1.2-sandbox/4.14.2/.opam-switch/build/coq-menhirlib.20250912
command /usr/bin/make -C coq-menhirlib -j2
exit-code 2
env-file ~/opam-root-4.14.2-2.1.2-sandbox/log/coq-menhirlib-5291-c2d36e.env
output-file ~/opam-root-4.14.2-2.1.2-sandbox/log/coq-menhirlib-5291-c2d36e.out

Oh, hmm, the actual issue was menhir.20250912 no longer compiling under Rocq.dev -- it is coq-menhirlib not compiling.

That probably means I'll need to merge #93 into master (and then into rocq-master) first, because menhir had a conflict with compcert. #93 drops the dependency on compcert (since we only need the numeric files which they release under a more permissive license), so I can then remove the cap on menhir's version. compcert also used to block ocaml 5 (unsure about its current status), so dropping the dependency seems like a good move.

[raoxiaojia]

@mattam82 #93 is merged and also into Rocq-master; dependency on menhir is now uncapped. The pipeline should hopefully work now.

[raoxiaojia]

Hmm I noticed that the CI fails on that branch. I'm not sure how meaningful/accurate it is given that it's on Rocq-dev, but the errors seem believable. I'll take a look later today.

[mattam82]

Ah right, my bad, I could have catched it was menhir indeed!

[raoxiaojia]

@mattam82 Rocq-master now compiles on CI (with rocq-dev). This should mean that the opam merge should work as well (the opam dependencies might need an update due to the changes).

Let me know if there's anything I can do to unblock further. I might not have much time to look at this until early July (popl deadline), but will keep track in case there's something simple I can fix.