From: Stuart Henderson <stu@spacehopper.org>
Subject: Re: reimport math/coq as math/rocq
To: Daniel Dickman <didickman@gmail.com>, Yozo Toda <yozo@v007.vaio.ne.jp>
Cc: <ports@openbsd.org>
Date: Thu, 08 May 2025 09:06:59 +0100

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