GNU logs - #73237, boring messages

Message sent to guix-patches@HIDDEN:

Subject: [bug#73237] [PATCH] gnu: Add coq-ceres.
Resent-From: Antero Mejr <mail@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Fri, 13 Sep 2024 20:56:02 +0000
Resent-Message-ID: <handler.73237.B.1726260950931 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
To: 73237 <at> debbugs.gnu.org
Cc: pukkamustard@HIDDEN, julien@HIDDEN
From: Antero Mejr <mail@HIDDEN>
Date: Fri, 13 Sep 2024 20:55:28 +0000
Message-ID: <87zfob1dfj.fsf@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13)
MIME-Version: 1.0
Content-Type: text/plain
Received-SPF: pass client-ip=207.246.76.47;
 envelope-from=SRS0=0bc9=QM=antr.me=mail@HIDDEN;
 helo=smtp.forwardemail.net
X-Spam_score_int: -20
X-Spam_score: -2.1
X-Spam_bar: --
X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
 DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, SPF_HELO_PASS=-0.001,
 SPF_PASS=-0.001 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-Spam-Score: -1.4 (-)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -2.4 (--)

* gnu/packages/coq.scm (coq-ceres): New variable.

Change-Id: I366aa3ad38a25bbcbaa70874241a22fb45d41938
---
 gnu/packages/coq.scm | 54 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 31d1e8d51d..6417b3ea48 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -777,3 +777,57 @@ (define-public coq-mathcomp-bigenough
 purposes as @code{bigenough} will be subsumed by the near tactics.  The
 formalization is based on the Mathematical Components library.")
     (license license:cecill-b)))
+
+(define-public coq-ceres
+  (package
+    (name "coq-ceres")
+    (version "0.4.1")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/Lysxia/coq-ceres")
+                    (commit version)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "080nldsxmrxdan6gd0dvdgswn3gkwpy5hdqwra6wlmh8zzrs9z7n"))))
+    (build-system gnu-build-system)
+    (arguments
+     (list #:test-target "test"
+           #:make-flags #~(list "-f" "Makefile.coq"
+                                (string-append "COQLIBINSTALL=" #$output
+                                               "/lib/coq/user-contrib")
+                                "NO_TEST=1"
+                                "COQTOP=coqtop")
+           #:phases #~(modify-phases %standard-phases
+                        ;; Need to generate Makefile.coq
+                        (replace 'configure
+                          (lambda _
+                            (invoke "coq_makefile" "-f" "_CoqProject.classic"
+                                    "-o" "Makefile.coq")))
+                        (add-after 'build 'build-doc
+                          (lambda* (#:key make-flags #:allow-other-keys)
+                            (apply invoke "make" "html" make-flags)))
+                        (replace 'check
+                          (lambda* (#:key tests? test-target parallel-build?
+                                    make-flags #:allow-other-keys)
+                            (when tests?
+                              (apply invoke "make"
+                                     "-j" (number->string
+                                           (if parallel-build?
+                                               (parallel-job-count)
+                                               1))
+                                     test-target make-flags))))
+                        (add-after 'install 'install-doc
+                          (lambda _
+                            (let ((doc (string-append #$output
+                                                      "/share/doc/ceres")))
+                              (mkdir-p doc)
+                              (copy-recursively "html" doc)))))))
+    (propagated-inputs (list coq))
+    (home-page "https://gitlab.mpi-sws.org/iris/actris")
+    (synopsis "Coq library for serialization to S-expressions")
+    (description
+     "This package provides a Coq library that allows for serialization and
+deserialization of S-expression data.")
+    (license license:bsd-3)))

base-commit: 0e0d9bc91f20ac6dda439ab09330f0163eb9bf42
-- 
2.46.0

Message sent:

Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable
MIME-Version: 1.0
X-Mailer: MIME-tools 5.505 (Entity 5.505)
Content-Type: text/plain; charset=utf-8
X-Loop: help-debbugs@HIDDEN
From: help-debbugs@HIDDEN (GNU bug Tracking System)
To: Antero Mejr <mail@HIDDEN>
Subject: bug#73237: Acknowledgement ([PATCH] gnu: Add coq-ceres.)
Message-ID: <handler.73237.B.1726260950931.ack <at> debbugs.gnu.org>
References: <87zfob1dfj.fsf@HIDDEN>
X-Gnu-PR-Message: ack 73237
X-Gnu-PR-Package: guix-patches
X-Gnu-PR-Keywords: patch
Reply-To: 73237 <at> debbugs.gnu.org
Date: Fri, 13 Sep 2024 20:56:02 +0000

Thank you for filing a new bug report with debbugs.gnu.org.

This is an automatically generated reply to let you know your message
has been received.

Your message is being forwarded to the package maintainers and other
interested parties for their attention; they will reply in due course.

Your message has been sent to the package maintainer(s):
 guix-patches@HIDDEN

If you wish to submit further information on this problem, please
send it to 73237 <at> debbugs.gnu.org.

Please do not send mail to help-debbugs@HIDDEN unless you wish
to report a problem with the Bug-tracking system.

--=20
73237: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D73237
GNU Bug Tracking System
Contact help-debbugs@HIDDEN with problems

Message sent to guix-patches@HIDDEN:

Subject: [bug#73237] [PATCH] gnu: Add coq-ceres.
References: <87zfob1dfj.fsf@HIDDEN>
In-Reply-To: <87zfob1dfj.fsf@HIDDEN>
Resent-From: Jean-Pierre De Jesus Diaz <jean@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Mon, 16 Sep 2024 14:56:01 +0000
Resent-Message-ID: <handler.73237.B73237.172649853918618 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
To: 73237 <at> debbugs.gnu.org
Cc: mail@HIDDEN
MIME-Version: 1.0
From: Jean-Pierre De Jesus Diaz <jean@HIDDEN>
Date: Mon, 16 Sep 2024 14:54:07 +0000
Message-ID: <CAG1gdUpqdcc7Q1jMoHnCYEcZVw=V9WWB3RFZ2bJFgd3tPUcx=w@HIDDEN>
Content-Type: text/plain; charset="UTF-8"
Precedence: list
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>

Hello,

I've also recently packaged coq-ceres for Guix in my personal channel,
it is a shorter version:

<https://github.com/jeandudey/guix-formal-verification/blob/25e9444861229f8345b7baea0a2251f5fd2c7fa8/formal-verification/packages/coq.scm#L46-L73>

I'd also adapt the install-doc to use the install-doc target of the generated
Makefile like this:

(arguments
 (list #:test-target "test"
       #:make-flags
       #~(list (string-append "COQLIBINSTALL=" #$output
                              "/lib/coq/user-contrib")
               (string-append "COQDOCINSTALL=" #$output
                              "/share/doc/" #$name "-" #$version))
       #:phases
       #~(modify-phases %standard-phases
           (delete 'configure)
           (add-after 'install 'install-documentation
             (lambda* (#:key make-flags #:allow-other-keys)
               (apply invoke "make" "install-doc" make-flags))))))

The license of the channel is GPL-3.0-or-later so feel free to take
inspiration from it to contribute to Guix.

>+ (propagated-inputs (list coq))

Coq does not need to be propagated, only needs to be a native-input.

Message sent to guix-patches@HIDDEN:

Subject: [bug#73237] [PATCH] gnu: Add coq-ceres.
Resent-From: Antero Mejr <mail@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Mon, 16 Sep 2024 15:16:01 +0000
Resent-Message-ID: <handler.73237.B73237.172649971422731 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
To: Jean-Pierre De Jesus Diaz <jean@HIDDEN>
Cc: 73237 <at> debbugs.gnu.org
From: Antero Mejr <mail@HIDDEN>
In-Reply-To: <CAG1gdUpqdcc7Q1jMoHnCYEcZVw=V9WWB3RFZ2bJFgd3tPUcx=w@HIDDEN>
 (Jean-Pierre De Jesus Diaz's message of "Mon, 16 Sep 2024 14:54:07
 +0000")
References: <CAG1gdUpqdcc7Q1jMoHnCYEcZVw=V9WWB3RFZ2bJFgd3tPUcx=w@HIDDEN>
Date: Mon, 16 Sep 2024 15:14:45 +0000
Message-ID: <87o74nr5p6.fsf@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13)
MIME-Version: 1.0
Content-Type: text/plain
Precedence: list
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>

Jean-Pierre De Jesus Diaz <jean@HIDDEN> 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.

Message sent to guix-patches@HIDDEN:

X-Loop: help-debbugs@HIDDEN
Subject: [bug#73237] [PATCH] gnu: Add coq-ceres.
Resent-From: Jean-Pierre De Jesus Diaz <jean@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Mon, 16 Sep 2024 15:22:02 +0000
Resent-Message-ID: <handler.73237.B73237.172650006424419 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 73237
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: Antero Mejr <mail@HIDDEN>
Cc: 73237 <at> debbugs.gnu.org
Received: via spool by 73237-submit <at> debbugs.gnu.org id=B73237.172650006424419
          (code B ref 73237); Mon, 16 Sep 2024 15:22:02 +0000
Received: (at 73237) by debbugs.gnu.org; 16 Sep 2024 15:21:04 +0000
Received: from localhost ([127.0.0.1]:53048 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1sqDXE-0006Ll-FH
	for submit <at> debbugs.gnu.org; Mon, 16 Sep 2024 11:21:04 -0400
Received: from mail-ot1-f52.google.com ([209.85.210.52]:61634)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <jean@HIDDEN>) id 1sqDXA-0006L6-UB
 for 73237 <at> debbugs.gnu.org; Mon, 16 Sep 2024 11:21:03 -0400
Received: by mail-ot1-f52.google.com with SMTP id
 46e09a7af769-710e910dd7dso2779027a34.2
 for <73237 <at> debbugs.gnu.org>; Mon, 16 Sep 2024 08:20:47 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=foundation.xyz; s=google; t=1726499982; x=1727104782; darn=debbugs.gnu.org; 
 h=content-transfer-encoding:cc:to:subject:message-id:date:from
 :in-reply-to:references:mime-version:from:to:cc:subject:date
 :message-id:reply-to;
 bh=g7W0y6q76+r9IeJoh8fBK0gBkZQ6JoaEvTqhSK8fc1M=;
 b=tIGrmV1KOAA5M8UgAJsmGXbpftZw7E3gfpSR3gow5a4EmWTxP7I2zGqCo0z9OTW479
 0WRtNp1bBBeSYOTYfbG6Df9HvD3XqPE7ty+cRs54lSrcSYn2AUM0fCKuAo3CMZi+cSZP
 UGhF6bpD233oJWCQiOEpeKzxjR/AI+1lOUWvRf5d7OJ4WsgSFPXohsf+xiw8w7BCbwHu
 T9o2rX+nYVXId39oeQ8GRd+Pgb9BjBBfcwqAsMX4nL44z6ql5yV1MF4nBqb0un6lFPr+
 ukdY99ocWZVrMFLqzOcSVkkJUqBBo7YXypb3ywBSgtDEdYOQreIx9PmCOmbbQjQpZK//
 6XwQ==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20230601; t=1726499982; x=1727104782;
 h=content-transfer-encoding:cc:to:subject:message-id:date:from
 :in-reply-to:references:mime-version:x-gm-message-state:from:to:cc
 :subject:date:message-id:reply-to;
 bh=g7W0y6q76+r9IeJoh8fBK0gBkZQ6JoaEvTqhSK8fc1M=;
 b=BwRoWFIzQ9iaBC0I/5IM9Ob8nT6h/W2+totR3Lf5XknE8EZrfs3YxU5Hgh4R4jtlzu
 GHxjEIKtpEGyGvxo0Uo3xATR/06JsndAmGLPcpp1RDH6O8+5JkvmbG6WHoXfKTp0pKNz
 gycspQmlSuweGZ/D1CCBHHmgdUVV8EAFm+p5qqVT2ggj07Jyp8A/UmrKvKtqeDgxZk0q
 WYpim+r60ynp2tQ9KRCIm+PeVBc5tiNRH3qIYRL5/YjPgEKdUTGmYhJ94yqSo5BScmgp
 nh39l9rBwSH406Xvud+FTXwuyuHHtxGhX/ztTUt7PS6y9SgIeTeT3fkyd4e7Y6EDmn/G
 njkg==
X-Gm-Message-State: AOJu0Yx5359+LVKIQzIj4rnzfxzxxCJNAqZ4P+TB4R9LQEPITB8WMaVy
 vrdBNauKqVqEaDsZjAg3YB25gezHBPaUNF8K98OKgpegzNfSZLcXDlZeRjF1tk6lnDjc8F+d5CY
 BSsQVPBiZRd/wHcSdW0yhPhYuA7Vd4lfcgC4rTw==
X-Google-Smtp-Source: AGHT+IFsMAMu7C9RhWzZvsrItmCr3S10EYeQL/y+gFRRNfrCxJdIj7uPf00oG6sG4GlgEBF+G+w5693tfVU7741K9vI=
X-Received: by 2002:a05:6808:17a9:b0:3e0:51f9:996b with SMTP id
 5614622812f47-3e071a7a6bamr11016998b6e.9.1726499981745; Mon, 16 Sep 2024
 08:19:41 -0700 (PDT)
MIME-Version: 1.0
References: <CAG1gdUpqdcc7Q1jMoHnCYEcZVw=V9WWB3RFZ2bJFgd3tPUcx=w@HIDDEN>
 <87o74nr5p6.fsf@HIDDEN>
In-Reply-To: <87o74nr5p6.fsf@HIDDEN>
From: Jean-Pierre De Jesus Diaz <jean@HIDDEN>
Date: Mon, 16 Sep 2024 15:19:31 +0000
Message-ID: <CAG1gdUqp6u=2kuVBhCFsdFSODYR7+XjVdWatq8AUXgVNC3MnnA@HIDDEN>
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: -0.0 (/)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

>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=E2=80=AFPM Antero Mejr <mail@HIDDEN> wrote:
>
> Jean-Pierre De Jesus Diaz <jean@HIDDEN> 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 gen=
erated
> > 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.

Message sent to guix-patches@HIDDEN:

X-Loop: help-debbugs@HIDDEN
Subject: [bug#73237] [PATCH] gnu: Add coq-ceres.
Resent-From: Jean-Pierre De Jesus Diaz <jean@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Mon, 16 Sep 2024 15:32:02 +0000
Resent-Message-ID: <handler.73237.B73237.172650071926777 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 73237
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: Antero Mejr <mail@HIDDEN>
Cc: 73237 <at> debbugs.gnu.org
Received: via spool by 73237-submit <at> debbugs.gnu.org id=B73237.172650071926777
          (code B ref 73237); Mon, 16 Sep 2024 15:32:02 +0000
Received: (at 73237) by debbugs.gnu.org; 16 Sep 2024 15:31:59 +0000
Received: from localhost ([127.0.0.1]:53076 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1sqDhm-0006xo-Hh
	for submit <at> debbugs.gnu.org; Mon, 16 Sep 2024 11:31:58 -0400
Received: from mail-ot1-f50.google.com ([209.85.210.50]:58434)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <jean@HIDDEN>) id 1sqDhk-0006xa-L7
 for 73237 <at> debbugs.gnu.org; Mon, 16 Sep 2024 11:31:57 -0400
Received: by mail-ot1-f50.google.com with SMTP id
 46e09a7af769-710e14e2134so2202329a34.0
 for <73237 <at> debbugs.gnu.org>; Mon, 16 Sep 2024 08:31:43 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=foundation.xyz; s=google; t=1726500638; x=1727105438; darn=debbugs.gnu.org; 
 h=content-transfer-encoding:cc:to:subject:message-id:date:from
 :in-reply-to:references:mime-version:from:to:cc:subject:date
 :message-id:reply-to;
 bh=PnwbGDI89gJpQpf9AC38REpI3qUvfdK48QsMaVplArM=;
 b=tTU3RF7ytvsqQlQtDC59k/0knEP+daDMjwMOCgsLACTjYkSR4nDP1rlS2LR4LVik+d
 bBP7O3KOyPoQ1oOvGhjAuYKBJLMgV8nXrhI3W7ujlJCNx5HYkxCHh/p3izgsQOSrJAWp
 zceEKv6bJGNVKgDwRdrjaxajpSSF7ZcvpN6gelEFY7ytgdcjzl9ALgPKxFWp/XOvuUxw
 1c8XguUVyXUALwrWcwAsliqcWdD9RzcodJRZpxHZoNlg3gPWYgiEaqzs/qzgpGwHu3lZ
 EkD7DMqT44jTUPVAUTxf+XiBQP1W69VfqbOipQSakntu+cHvRaSidlqo/H69PnwK8iXs
 BHpA==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20230601; t=1726500638; x=1727105438;
 h=content-transfer-encoding:cc:to:subject:message-id:date:from
 :in-reply-to:references:mime-version:x-gm-message-state:from:to:cc
 :subject:date:message-id:reply-to;
 bh=PnwbGDI89gJpQpf9AC38REpI3qUvfdK48QsMaVplArM=;
 b=b3sQ+NQOC4Y9UleDIMpPukyifyJ6MSKu8oIN3xg0knBOBzSYLs6FwNxj1gZsP6uPD4
 0ck1AeEXwBWz7w/TWsm9UsqQDbw9X2yUAuIj7iErfAfVIb5/S09eR+yqVCwVOnR37VDd
 hbPV7R/Luf52xmCYnkW+ettLZ1AgPMn/cZtEB5JZYIog5MTnWDHcwtAhdqJlfwF+MfDN
 tYtopAo5eo5Vx/QthUMh7mir4bJ2HQyIE3k2L25OWXjkmDGPmUxvaIwIdl6MdXMVvcdC
 oMOtrW2fBJS7scUQyqmYtlPwfdfBL9hnOczndwZA/+rRnx71W/E2pqkSCRBgw6VYI0yl
 5d/g==
X-Gm-Message-State: AOJu0Yzb87244BMfLiSkDqVYr2U6aFXmvtaeNZgAeYHcX6iL3GiJk/yW
 EyLUv3aaTGBwmeeZpCf78SlX5Pa03o+ef/B0WF9qW5ZiS0BZRMJL1HeninZ/16ZL7AWD1oOdocD
 zQY/dNyUBYo/7iRW4uu6NkGozE/hU6u11D21QvHCluXLEtIez
X-Google-Smtp-Source: AGHT+IHG2PnRzFlTbYJMzigugC+RAH3nNrCaaFdAgCXL9RCPk4/gmJ0s2NZGqf3nfIkNcgpcTwpZE2fWEpYZVkJKCNg=
X-Received: by 2002:a05:6830:270e:b0:710:dec2:df70 with SMTP id
 46e09a7af769-711094baecamr10486984a34.24.1726500637656; Mon, 16 Sep 2024
 08:30:37 -0700 (PDT)
MIME-Version: 1.0
References: <CAG1gdUpqdcc7Q1jMoHnCYEcZVw=V9WWB3RFZ2bJFgd3tPUcx=w@HIDDEN>
 <87o74nr5p6.fsf@HIDDEN>
 <CAG1gdUqp6u=2kuVBhCFsdFSODYR7+XjVdWatq8AUXgVNC3MnnA@HIDDEN>
In-Reply-To: <CAG1gdUqp6u=2kuVBhCFsdFSODYR7+XjVdWatq8AUXgVNC3MnnA@HIDDEN>
From: Jean-Pierre De Jesus Diaz <jean@HIDDEN>
Date: Mon, 16 Sep 2024 15:30:27 +0000
Message-ID: <CAG1gdUrRDfpsDgqSEtkAU1+sYkdEJUHaSeLiZZDA-UmT=ikZRA@HIDDEN>
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: -0.0 (/)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

>That's odd, it also propagates `which' when it shouldn't, only coq-mathcom=
p
>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=E2=80=AFPM Jean-Pierre De Jesus Diaz
<jean@HIDDEN> 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-mathco=
mp
> should be propagated.
>
> On Mon, Sep 16, 2024 at 3:14=E2=80=AFPM Antero Mejr <mail@HIDDEN> wrote:
> >
> > Jean-Pierre De Jesus Diaz <jean@HIDDEN> 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 g=
enerated
> > > 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 thin=
k
> > those packages should be updated to have coq as a native-input as well.

Last modified: Sun, 12 Jan 2025 05:45:02 UTC

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