> On May 10, 2025, at 3:25 AM, Yozo TODA <y...@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.
>
