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

Previous Next

Package: guix-patches;

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

Date: Mon, 16 Sep 2024 15:29:02 UTC

Severity: normal

Tags: patch

Done: Ludovic Courtès <ludo <at> gnu.org>

Bug is archived. No further changes may be made.

Full log


View this message in rfc822 format

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>, Julien Lepiller <julien <at> lepiller.eu>, pukkamustard <pukkamustard <at> posteo.net>
Subject: [bug#73298] [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





This bug report was last modified 183 days ago.

Previous Next


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