From: Daniel Dickman <didickman@gmail.com>
Subject: Re: reimport math/coq as math/rocq
To: Yozo TODA <yozo@v007.vaio.ne.jp>
Cc: Daniel Dickman <didickman@gmail.com>, ports@openbsd.org,  Stuart Henderson <stu@spacehopper.org>
Date: Mon, 12 May 2025 18:48:00 -0400



On Sun, 11 May 2025, Yozo TODA wrote:

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

Would you mind sending out what's needed for the update? 8.19 sounds good 
to me. I think ocaml 4.14 compat was only added in coq 8.17 so that 
version or newer is probably best.

Please correct me if I'm wrong, but from a quick look I think the steps 
might be:
1. update dune
2. import ocaml-camlp-streams
3. update lablgtk3 (even if coqide can't be built)
4. update coq to 8.19

Once this update is in I can take care of compcert.

Thank you