Re: reimport math/coq as math/rocq

It needs a quirks $stem_extensions entry to cover the renaming, and compcert BDEP needs changing.

-- 

  Sent from a phone, apologies for poor formatting.

On 8 May 2025 00:23:55 Daniel Dickman <didickman@gmail.com> wrote:

The coq project has been renamed to rocq. I'd like to reimport it as 

math/rocq before doing more updates.

See the proposed diff below for with the minimal update.

ok?

diff -Nur -x CVS coq/Makefile rocq/Makefile

--- coq/Makefile Wed Apr 24 13:10:22 2024

+++ rocq/Makefile Wed May  7 18:59:21 2025

@@ -1,13 +1,13 @@

 COMMENT= proof assistant based on a typed lambda calculus

 

 V= 8.13.2

-GH_ACCOUNT = coq

-GH_PROJECT = coq

+GH_ACCOUNT = rocq-prover

+GH_PROJECT = rocq

 GH_TAGNAME = V${V}

-REVISION = 6

+REVISION = 7

 

 CATEGORIES= math

-HOMEPAGE= https://coq.inria.fr/

+HOMEPAGE= https://rocq-prover.org/

 

 MAINTAINER= Yozo Toda <yozo@v007.vaio.ne.jp>

 

diff -Nur -x CVS coq/distinfo rocq/distinfo

--- coq/distinfo Fri Dec  3 23:33:45 2021

+++ rocq/distinfo Wed May  7 19:01:01 2025

@@ -1,2 +1,2 @@

-SHA256 (coq-8.13.2.tar.gz) = HneT2Eg/HpOfYt9nSfhD35Z6FdhDpKWssCSQS3biWhQ=

-SIZE (coq-8.13.2.tar.gz) = 6952855

+SHA256 (rocq-8.13.2.tar.gz) = 5ucx3gPDudWnJS0DJbgv6AGmr39R+loSMae8aq4/bZk=

+SIZE (rocq-8.13.2.tar.gz) = 6952061

diff -Nur -x CVS coq/pkg/PLIST rocq/pkg/PLIST

--- coq/pkg/PLIST Fri Mar 11 14:36:13 2022

+++ rocq/pkg/PLIST Wed May  7 19:20:24 2025

@@ -1,3 +1,5 @@

+@conflict coq-*

+@pkgpath math/coq

 %%native%%

 !%%native%%

 bin/coqpp