ryan77627/guix
1
0
Fork 0
mirror of https://git.in.rschanz.org/ryan77627/guix.git synced 2025-01-12 14:16:55 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

gnu: coq: Propagate ocaml-zarith.

Browse source 
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>
This commit is contained in:
Jean-Pierre De Jesus DIAZ 2024-08-20 12:31:18 +02:00 committed by Zheng Junjie
parent 0b17ad1e8b
commit 114a77e55d
No known key found for this signature in database
GPG key ID: 3B5AA993E1A2DFF0
1 changed files with 7 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
gnu/packages/coq.scm
View file

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