GNU bug report logs - #72730
[PATCH 0/2] coq: Update to 8.18.0.

Previous Next

Full log

View this message in rfc822 format

From: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
To: 72730 <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#72730] [PATCH 1/2] gnu: coq: Propagate ocaml-zarith.
Date: Tue, 20 Aug 2024 12:31:18 +0200

Otherwise each Coq plugin needs to specify it.

* gnu/packages/coq.scm (coq) <inputs>: Move ocaml-zarith from here...
<propagated-inptus>: ... to here.
(coq-gappa) <inputs>: Remove ocaml-zarith.
(coq-bignums) <inputs>: Likewise.
(coq-interval) <inputs>: Likewise.
(coq-equations) <inputs>: Likewise.

Change-Id: I63cab11032cc6d4673efc9fdcf14be2929bda05e
---
 gnu/packages/coq.scm | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 4857426613..be95d16991 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -91,8 +91,10 @@ (define-public coq
                      (libdir (string-append out "/lib/ocaml/site-lib")))
                 (invoke "dune" "install" "--prefix" out
                         "--libdir" libdir "coq" "coq-core" "coq-stdlib")))))))
+    (propagated-inputs
+     (list ocaml-zarith))
     (inputs
-     (list gmp ocaml-zarith))
+     (list gmp))
     (native-inputs
      (list ocaml-ounit2 which))
     (properties '((upstream-name . "coq"))) ; also for inherited packages
@@ -114,7 +116,7 @@ (define-public coq-ide-server
      `(#:tests? #f
        #:package "coqide-server"))
     (inputs
-     (list coq gmp ocaml-zarith))))
+     (list coq gmp))))
 
 (define-public coq-ide
   (package
@@ -319,7 +321,7 @@ (define-public coq-gappa
            bison
            flex))
     (inputs
-     (list gmp mpfr ocaml-zarith boost))
+     (list gmp mpfr boost))
     (propagated-inputs
      (list coq-flocq))
     (arguments
@@ -457,7 +459,7 @@ (define-public coq-bignums
     (native-inputs
      (list ocaml coq))
     (inputs
-     (list camlp5 ocaml-zarith))
+     (list camlp5))
     (arguments
      `(#:tests? #f ; No test target.
        #:make-flags
@@ -495,8 +497,7 @@ (define-public coq-interval
      `(("flocq" ,coq-flocq)
        ("bignums" ,coq-bignums)
        ("coquelicot" ,coq-coquelicot)
-       ("mathcomp" ,coq-mathcomp)
-       ("ocaml-zarith" ,ocaml-zarith)))
+       ("mathcomp" ,coq-mathcomp)))
     (arguments
      `(#:configure-flags
        (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out")
@@ -579,8 +580,6 @@ (define-public coq-equations
     (build-system gnu-build-system)
     (native-inputs
      (list ocaml coq camlp5))
-    (inputs
-     (list ocaml-zarith))
     (arguments
      `(#:test-target "test-suite"
        #:make-flags (list (string-append "COQLIBINSTALL="
-- 
2.45.2

Previous Next

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