Download raw body.
reimport math/coq as math/rocq
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
reimport math/coq as math/rocq