Subject: [bug#73237] [PATCH] gnu: Add coq-ceres.

From: Jean-Pierre De Jesus Diaz <[email-masked]>
Date: Mon, 16 Sep 2024 15:30:27 +0000

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

I've sent a few patches to fix this:

<https://issues.guix.gnu.org/73298>

On Mon, Sep 16, 2024 at 3:19 PM Jean-Pierre De Jesus Diaz
<[email-masked]> wrote:
>
> >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 <[email-masked]> wrote:
> >
> > Jean-Pierre De Jesus Diaz <[email-masked]> 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.