> Here is an update of rocq to 8.20.1 which I was able to use to compile 
> latest compcert and was built on your 8.19.1 diff..
>
> It removes coqide and disables TESTs which can be fixed later.

OK from me, with two small comments.

(1) regarding "...removes coqide ...",

the targets do-build and do-install still have (dune target) "coqide-server".

> +		dune build -j ${MAKE_JOBS} -p coq-core,coq-stdlib,coqide-server,coq
> +
> +do-install:
> +	cd ${WRKSRC} && \
> +		dune install -j ${MAKE_JOBS} coq-core coq-stdlib coqide-server coq

Though I don't confirm but, at this stage, I believe we can omit this dune target
and PLIST and PFRAG files can be reduced a little.
But I'm thinking that future updates should make coqide available, and
we can say that this current update includes some preparation for future updates.

(2) regarding pkg/DESCR,

it is valuable to mention the relation on the new name "Rocq" and the old name "Coq".
Referring to the current phrase on rocq-prover.org,
how about this?

The Rocq Prover, formerly known as the Coq Proof Assistant, is an interactive
theorem prover, or proof assistant. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with
an environment for semi-interactive development of machine-checked proofs.

-- yozo.