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

From: Antero Mejr <[email-masked]>
Date: Mon, 16 Sep 2024 15:14:45 +0000

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.