From: Daniel Dickman <didickman@gmail.com>
Subject: Re: reimport math/coq as math/rocq
To: Yozo TODA <yozo@v007.vaio.ne.jp>
Cc: ports@openbsd.org, Stuart Henderson <stu@spacehopper.org>, Yozo Toda <yozo@v007.vaio.ne.jp>
Date: Sat, 10 May 2025 03:55:53 -0400



> On May 10, 2025, at 3:25 AM, Yozo TODA <yozo@v007.vaio.ne.jp> wrote:
> 
> 
>> 
>> It needs a quirks $stem_extensions entry to cover the renaming, and
>> compcert BDEP needs changing.
> ........
>>> The coq project has been renamed to rocq. I'd like to reimport it as
>>> math/rocq before doing more updates.
> 
> thanks Daniel and stu!
> 
> I understand now that access to github.com/coq/coq is redirected
> to github.com/rocq-prover/rocq.
> 

Yes. Coq is no more due to the project’s decision to rename themselves.

> As far as I remember, when rocq repository was created,
> it was an independent repository different from coq.
> That made me thinking about adding math/rocq with the newer version and
> keeping math/coq for a while until lang/compcert being updated to depend on math/rocq.

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.

> 
> -- yozo.
>