GNU bug report logs - #73298
[PATCH 0/2] gnu: coq-mathcomp-bigenough: Use native-inputs.

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 73298 in the body.
You can then email your comments to 73298 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

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

From: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
To: guix-patches <at> gnu.org
Cc: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Subject: [PATCH 0/2] gnu: coq-mathcomp-bigenough: Use native-inputs.
Date: Mon, 16 Sep 2024 17:28:12 +0200

This simplifies the coq-mathcomp-bigenough package by removing uneeded
make flags and also moves coq and which from propagated-inputs to
native-inputs.

Jean-Pierre De Jesus DIAZ (2):
  gnu: coq-mathcomp-bigenough: Use new style.
  gnu: coq-mathcomp-bigenough: Use native-inputs.

 gnu/packages/coq.scm | 28 ++++++++++++----------------
 1 file changed, 12 insertions(+), 16 deletions(-)


base-commit: ee64bcfb796ef36db4b63f79540627fb25f3320a
-- 
2.46.0

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

From: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
To: 73298 <at> debbugs.gnu.org
Cc: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Subject: [PATCH 1/2] gnu: coq-mathcomp-bigenough: Use new style.
Date: Mon, 16 Sep 2024 17:29:09 +0200

* gnu/packages/coq.scm (coq-mathcomp-bigenough) [arguments]: Use new
style and remove uneeded make flags.

Change-Id: I11a6350a10cedd682cf598ecb8660b63a12aa00d
---
 gnu/packages/coq.scm | 25 ++++++++++---------------
 1 file changed, 10 insertions(+), 15 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 31d1e8d51d..166657fdd1 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -753,21 +753,16 @@ (define-public coq-mathcomp-bigenough
                 "02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw"))))
     (build-system gnu-build-system)
     (arguments
-     `(;; No references to tests in Makefile.common.
-       ;; It doesn't appear as though tests will be included
-       ;; by the packaged project in the future.
-       #:tests? #f
-       #:make-flags ,#~(list (string-append "COQBIN="
-                                            #$(this-package-input "coq")
-                                            "/bin/")
-                             (string-append "COQMF_COQLIB="
-                                            (assoc-ref %outputs "out")
-                                            "/lib/ocaml/site-lib/coq")
-                             (string-append "COQLIBINSTALL="
-                                            (assoc-ref %outputs "out")
-                                            "/lib/coq/user-contrib"))
-       #:phases (modify-phases %standard-phases
-                  (delete 'configure))))
+     (list ;; No references to tests in Makefile.common.
+           ;; It doesn't appear as though tests will be included
+           ;; by the packaged project in the future.
+           #:tests? #f
+           #:make-flags
+           #~(list (string-append "COQLIBINSTALL=" #$output
+                                  "/lib/coq/user-contrib"))
+           #:phases
+           #~(modify-phases %standard-phases
+               (delete 'configure))))
     (propagated-inputs (list coq coq-mathcomp which))
     (home-page "https://math-comp.github.io/")
     (synopsis "Small library to do epsilon - N reasoning")
-- 
2.46.0

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

From: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
To: 73298 <at> debbugs.gnu.org
Cc: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Subject: [PATCH 2/2] gnu: coq-mathcomp-bigenough: Use native-inputs.
Date: Mon, 16 Sep 2024 17:29:10 +0200

* gnu/packages/coq.scm (coq-mathcomp-bigenough) [propagated-inputs]:
Move coq and which from here...
[native-inputs]: ... to here.

Change-Id: I1a57175b69f6b4a5eba308bf60c9e74437563f58
---
 gnu/packages/coq.scm | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 166657fdd1..ea0868f226 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -763,7 +763,8 @@ (define-public coq-mathcomp-bigenough
            #:phases
            #~(modify-phases %standard-phases
                (delete 'configure))))
-    (propagated-inputs (list coq coq-mathcomp which))
+    (native-inputs (list coq which))
+    (propagated-inputs (list coq-mathcomp))
     (home-page "https://math-comp.github.io/")
     (synopsis "Small library to do epsilon - N reasoning")
     (description
-- 
2.46.0

Message #16 received at 73298-done <at> debbugs.gnu.org (full text, mbox):

From: Ludovic Courtès <ludo <at> gnu.org>
To: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Cc: pukkamustard <pukkamustard <at> posteo.net>,
 Julien Lepiller <julien <at> lepiller.eu>, 73298-done <at> debbugs.gnu.org
Subject: Re: [bug#73298] [PATCH 0/2] gnu: coq-mathcomp-bigenough: Use
 native-inputs.
Date: Sun, 17 Nov 2024 23:02:38 +0100

Hi,

Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz> skribis:

> This simplifies the coq-mathcomp-bigenough package by removing uneeded
> make flags and also moves coq and which from propagated-inputs to
> native-inputs.
>
> Jean-Pierre De Jesus DIAZ (2):
>   gnu: coq-mathcomp-bigenough: Use new style.
>   gnu: coq-mathcomp-bigenough: Use native-inputs.

I went ahead and applied both, even though I’m not on the Coq/OCaml
team.

I think you should consider joining that team (Julien, pukkamustard,
perhaps you could use some help?) and probably applying for commit
rights as well.

Thanks,
Ludo’.

Previous Next

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