GNU bug report logs - #73237
[PATCH] gnu: Add coq-ceres.

Previous Next

Full log

Message #14 received at 73237 <at> debbugs.gnu.org (full text, mbox):

From: Jean-Pierre De Jesus Diaz <jean <at> foundation.xyz>
To: Antero Mejr <mail <at> antr.me>
Cc: 73237 <at> debbugs.gnu.org
Subject: Re: [PATCH] gnu: Add coq-ceres.
Date: Mon, 16 Sep 2024 15:19:31 +0000

>Yes. For some reason, the coq-mathcomp-bigenough package propagates coq,
>and coq-stdpp has it in inputs, so I was unsure where to put it. I think
>those packages should be updated to have coq as a native-input as well.

That's odd, it also propagates `which' when it shouldn't, only coq-mathcomp
should be propagated.

On Mon, Sep 16, 2024 at 3:14 PM Antero Mejr <mail <at> antr.me> wrote:
>
> Jean-Pierre De Jesus Diaz <jean <at> foundation.xyz> writes:
>
> > I've also recently packaged coq-ceres for Guix in my personal channel,
> > it is a shorter version:
>
> There's a lot of useful stuff there, it would be great to get it
> upstreamed. Unfortunately I do not have commit access.
>
> > I'd also adapt the install-doc to use the install-doc target of the generated
> > Makefile like this:
>
> That sounds good, I will update the patch.
>
> > Coq does not need to be propagated, only needs to be a native-input.
>
> Yes. For some reason, the coq-mathcomp-bigenough package propagates coq,
> and coq-stdpp has it in inputs, so I was unsure where to put it. I think
> those packages should be updated to have coq as a native-input as well.

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.