[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[bug#64249] [PATCH ocaml-team v4 5/9] gnu: coq: Update to 8.17.1.
From: |
pukkamustard |
Subject: |
[bug#64249] [PATCH ocaml-team v4 5/9] gnu: coq: Update to 8.17.1. |
Date: |
Fri, 28 Jul 2023 11:08:27 +0000 |
* gnu/packages/coq.scm (coq): Update to 8.17.1 and merge with coq-core and
coq-stdlib.
[arguments] Merge with coq-core and coq-stdlib. Add pre-build phases and
add a custom install phase. Remove unnecessary test-target
(coq-core): Remove variable.
(coq-stdlib): Remove variable.
(coq-mathcomp-bigenough)[propagated-inputs] Remove coq-core.
---
gnu/packages/coq.scm | 65 ++++++++++++++++----------------------------
1 file changed, 24 insertions(+), 41 deletions(-)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index cc914422d4..6f9205cfb0 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -50,10 +50,10 @@ (define-module (gnu packages coq)
#:use-module (guix utils)
#:use-module ((srfi srfi-1) #:hide (zip)))
-(define-public coq-core
+(define-public coq
(package
- (name "coq-core")
- (version "8.16.1")
+ (name "coq")
+ (version "8.17.1")
(source
(origin
(method git-fetch)
@@ -63,7 +63,7 @@ (define-public coq-core
(file-name (git-file-name name version))
(sha256
(base32
- "0ljpqhh5lfsim29fcfp2xfcvm3j84pf1mb0gnpdr8vcqqw7mqwpf"))
+ "0gg6hizq0i08lk741b579cbswhy6qvkh6inc3d3i5a2af98psq63"))
(patches (search-patches "coq-fix-envvars.patch"))))
(native-search-paths
(list (search-path-specification
@@ -78,13 +78,29 @@ (define-public coq-core
(files (list "lib/ocaml/site-lib/coq-core"))
(separator #f))))
(build-system dune-build-system)
+ (arguments
+ `(#:package "coq-core,coq-stdlib,coq"
+ #:phases
+ (modify-phases %standard-phases
+ (add-before 'build 'configure
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (libdir (string-append out "/lib/ocaml/site-lib")))
+ (invoke "./configure" "-prefix" out
+ "-libdir" libdir))))
+ (add-before 'build 'make-dunestrap
+ (lambda _ (invoke "make" "dunestrap")))
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (libdir (string-append out "/lib/ocaml/site-lib")))
+ (invoke "dune" "install" "--prefix" out
+ "--libdir" libdir
+ "coq-core" "coq-stdlib" "coq")))))))
(inputs
(list gmp ocaml-zarith))
(native-inputs
(list ocaml-ounit2 which))
- (arguments
- `(#:package "coq-core"
- #:test-target "."))
(properties '((upstream-name . "coq"))) ; also for inherited packages
(home-page "https://coq.inria.fr")
(synopsis "Proof assistant for higher-order logic")
@@ -96,39 +112,6 @@ (define-public coq-core
;; Some of the documentation is distributed under opl1.0+.
(license (list license:lgpl2.1 license:opl1.0+))))
-(define-public coq-stdlib
- (package
- (inherit coq-core)
- (name "coq-stdlib")
- (arguments
- `(#:package "coq-stdlib"
- #:test-target "."
- #:phases
- (modify-phases %standard-phases
- (add-before 'build 'fix-dune
- (lambda _
- (substitute* "user-contrib/Ltac2/dune"
- (("coq-core.plugins.ltac2")
- (string-join
- (map (lambda (plugin) (string-append "coq-core.plugins."
plugin))
- '("ltac2" "number_string_notation" "tauto" "cc"
- "firstorder"))
- " "))))))))
- (inputs
- (list coq-core gmp ocaml-zarith))
- (native-inputs '())))
-
-(define-public coq
- (package
- (inherit coq-core)
- (name "coq")
- (arguments
- `(#:package "coq"
- #:test-target "."))
- (propagated-inputs
- (list coq-core coq-stdlib))
- (native-inputs '())))
-
(define-public coq-ide-server
(package
(inherit coq)
@@ -761,7 +744,7 @@ (define-public coq-mathcomp-bigenough
"/lib/coq/user-contrib"))
#:phases (modify-phases %standard-phases
(delete 'configure))))
- (propagated-inputs (list coq coq-core coq-mathcomp which))
+ (propagated-inputs (list coq coq-mathcomp which))
(home-page "https://math-comp.github.io/")
(synopsis "Small library to do epsilon - N reasoning")
(description
--
2.40.1
- [bug#64249] [PATCH ocaml-team v4 0/9], pukkamustard, 2023/07/28
- [bug#64249] [PATCH ocaml-team v4 1/9] gnu: ocaml: Update to 4.14.1., pukkamustard, 2023/07/28
- [bug#64249] [PATCH ocaml-team v4 2/9] gnu: Update coq-flocq to 4.1.1., pukkamustard, 2023/07/28
- [bug#64249] [PATCH ocaml-team v4 3/9] gnu: Update coq-gappa to 1.5.3., pukkamustard, 2023/07/28
- [bug#64249] [PATCH ocaml-team v4 5/9] gnu: coq: Update to 8.17.1.,
pukkamustard <=
- [bug#64249] [PATCH ocaml-team v4 8/9] gnu: Add opam-installer., pukkamustard, 2023/07/28
- [bug#64249] [PATCH ocaml-team v4 7/9] gnu: opam: Split build into smaller sub-packages., pukkamustard, 2023/07/28
- [bug#64249] [PATCH ocaml-team v4 6/9] gnu: dune-bootstrap: Update to 3.9.1., pukkamustard, 2023/07/28
- [bug#64249] [PATCH ocaml-team v4 9/9] FIXME: gnu: opam: Update to 2.1.5., pukkamustard, 2023/07/28
- [bug#64249] [PATCH ocaml-team v4 4/9] gnu: Update coq-mathcomp to 1.17.0., pukkamustard, 2023/07/28
- [bug#64249] [PATCH ocaml-team v4 0/9], Julien Lepiller, 2023/07/30