From: Yozo Toda Subject: Re: [update] math/rocq 8.13.2 -> 8.20.1 To: Daniel Dickman Cc: ports@openbsd.org, Yozo Toda Date: Sun, 25 May 2025 19:43:24 +0900 > 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.