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