From: Yozo TODA <yozo@v007.vaio.ne.jp>
Subject: Re: reimport math/coq as math/rocq
To: Daniel Dickman <didickman@gmail.com>
Cc: ports@openbsd.org, Stuart Henderson <stu@spacehopper.org>, Yozo Toda <yozo@v007.vaio.ne.jp>
Date: Sun, 11 May 2025 04:21:09 +0900

(hmm... my email doesn't go to the list? anyway...)

> Are you able to update coq/rocq soon? Compcert now needs coq 8.15+ so
> the ancient version of coq in our tree is now a blocker for compcert updates.

I was playing with 8.19.1 around March and it can be packaged without coqide.
(I didn't try building compcert yet.)
see https://github.com/yozot/OpenBSD-ports-mystuff/tree/master/math/coq

-- yozo.