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 <didick...@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 <y...@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

Reply via email to