> 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.
