diff options
| author | Jean-Pierre De Jesus DIAZ <jean@foundation.xyz> | 2024-08-20 12:31:18 +0200 |
|---|---|---|
| committer | Zheng Junjie <zhengjunjie@iscas.ac.cn> | 2024-09-12 13:20:40 +0800 |
| commit | 114a77e55db43c5507ed25eb47543f2c8e9199df (patch) | |
| tree | 0555dda9b3f2eaf6da0a8fbd4ec7532aab6805d9 /gnu/packages | |
| parent | 0b17ad1e8b9056a0af621ebb8c5faf4b029ad34d (diff) | |
| download | guix-114a77e55db43c5507ed25eb47543f2c8e9199df.tar guix-114a77e55db43c5507ed25eb47543f2c8e9199df.tar.gz | |
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>
Diffstat (limited to 'gnu/packages')
| -rw-r--r-- | gnu/packages/coq.scm | 15 |
1 files 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=" |