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

Previous Next

Full log

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

From: Z572 <zhengjunjie <at> iscas.ac.cn>
To: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Cc: 72730 <at> debbugs.gnu.org, pukkamustard <pukkamustard <at> posteo.net>,
 Julien Lepiller <julien <at> lepiller.eu>
Subject: Re: [bug#72730] [PATCH 1/2] gnu: coq: Propagate ocaml-zarith.
Date: Thu, 12 Sep 2024 14:34:09 +0800

[Message part 1 (text/plain, inline)]

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

> 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.

adjust to

* 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="

[signature.asc (application/pgp-signature, inline)]

Previous Next

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