04/09: gnu: coq: Propagate ocaml-zarith.

[guix-commits]

z572 pushed a commit to branch master
in repository guix.

commit 114a77e55db43c5507ed25eb47543f2c8e9199df
Author: Jean-Pierre De Jesus DIAZ <jean@foundation.xyz>
AuthorDate: Tue Aug 20 12:31:18 2024 +0200

    gnu: coq: Propagate ocaml-zarith.
    
    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
    Signed-off-by: Zheng Junjie <zhengjunjie@iscas.ac.cn>
---
 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 @@
                      (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 @@ It is developed using Objective Caml and Camlp5.")
      `(#:tests? #f
        #:package "coqide-server"))
     (inputs
-     (list coq gmp ocaml-zarith))))
+     (list coq gmp))))
 
 (define-public coq-ide
   (package
@@ -319,7 +321,7 @@ inside Coq.")
            bison
            flex))
     (inputs
-     (list gmp mpfr ocaml-zarith boost))
+     (list gmp mpfr boost))
     (propagated-inputs
      (list coq-flocq))
     (arguments
@@ -457,7 +459,7 @@ theorems between the two libraries.")
     (native-inputs
      (list ocaml coq))
     (inputs
-     (list camlp5 ocaml-zarith))
+     (list camlp5))
     (arguments
      `(#:tests? #f ; No test target.
        #:make-flags
@@ -495,8 +497,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq 
standard library.")
      `(("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 @@ uses Ltac to synthesize the substitution operation.")
     (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="