summaryrefslogtreecommitdiff
path: root/gnu/packages/coq.scm
diff options
context:
space:
mode:
authorJulien Lepiller <julien@lepiller.eu>2021-11-28 16:42:56 +0100
committerJulien Lepiller <julien@lepiller.eu>2021-11-30 03:52:00 +0100
commitd95a982cdd898790d247f013440f08a448265e3f (patch)
tree9b2f1c794fca28895a2a7dcab0b00cc3992c07a6 /gnu/packages/coq.scm
parent189501bf3b8facced98f08e73b7cdb83ec7a272b (diff)
gnu: coq: Update to 8.14.0.
* gnu/packages/coq.scm (coq): Update to 8.14.0. (coq-bignums): Update to 8.14.0. (coq-equations): Update to 1.3. * gnu/packages/patches/coq-fix-envvars.patch: New file. * gnu/local.mk (dist_patch_DATA): Add it.
Diffstat (limited to 'gnu/packages/coq.scm')
-rw-r--r--gnu/packages/coq.scm63
1 files changed, 47 insertions, 16 deletions
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 8d967241f5..cf0c67f214 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -49,10 +49,10 @@
#:use-module (guix utils)
#:use-module ((srfi srfi-1) #:hide (zip)))
-(define-public coq
+(define-public coq-core
(package
- (name "coq")
- (version "8.13.2")
+ (name "coq-core")
+ (version "8.14.0")
(source
(origin
(method git-fetch)
@@ -62,25 +62,31 @@
(file-name (git-file-name name version))
(sha256
(base32
- "15r0cm3p9dlsxbg0lf05njjp1xi1y74vxvq6drxjykax67x95l8a"))))
+ "0iachapmdwvwwlvkrb2yxhqqrgzs70zyr1c9v1jdb1awx3bp68hf"))
+ (patches (search-patches "coq-fix-envvars.patch"))))
(native-search-paths
(list (search-path-specification
(variable "COQPATH")
- (files (list "lib/coq/user-contrib")))
+ (files (list "lib/ocaml/site-lib/coq/user-contrib"
+ "lib/coq/user-contrib")))
(search-path-specification
- (variable "COQLIB")
- (files (list "lib/ocaml/site-lib/coq"))
+ (variable "COQLIBPATH")
+ (files (list "lib/ocaml/site-lib/coq")))
+ (search-path-specification
+ (variable "COQCORELIB")
+ (files (list "lib/ocaml/site-lib/coq-core"))
(separator #f))))
(build-system dune-build-system)
(inputs
`(("gmp" ,gmp)
("ocaml-zarith" ,ocaml-zarith)))
(native-inputs
- `(("which" ,which)))
+ `(("ocaml-ounit2" ,ocaml-ounit2)
+ ("which" ,which)))
(arguments
- `(#:package "coq"
- #:test-target "test-suite"))
- (properties '((upstream-name . "coq"))) ; for inherited packages
+ `(#: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")
(description
@@ -91,6 +97,31 @@ It is developed using Objective Caml and Camlp5.")
;; 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 "."))
+ (inputs
+ `(("coq-core" ,coq-core)
+ ("gmp" ,gmp)
+ ("ocaml-zarith" ,ocaml-zarith)))
+ (native-inputs '())))
+
+(define-public coq
+ (package
+ (inherit coq-core)
+ (name "coq")
+ (arguments
+ `(#:package "coq"
+ #:test-target "."))
+ (propagated-inputs
+ `(("coq-core" ,coq-core)
+ ("coq-stdlib" ,coq-stdlib)))
+ (native-inputs '())))
+
(define-public coq-ide-server
(package
(inherit coq)
@@ -410,7 +441,7 @@ theorems between the two libraries.")
(define-public coq-bignums
(package
(name "coq-bignums")
- (version "8.13.0")
+ (version "8.14.0")
(source (origin
(method git-fetch)
(uri (git-reference
@@ -419,7 +450,7 @@ theorems between the two libraries.")
(file-name (git-file-name name version))
(sha256
(base32
- "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y"))))
+ "0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06"))))
(build-system gnu-build-system)
(native-inputs
`(("ocaml" ,ocaml)
@@ -537,16 +568,16 @@ uses Ltac to synthesize the substitution operation.")
(define-public coq-equations
(package
(name "coq-equations")
- (version "1.2.4")
+ (version "1.3")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/mattam82/Coq-Equations")
- (commit (string-append "v" version "-8.13"))))
+ (commit (string-append "v" version "-8.14"))))
(file-name (git-file-name name version))
(sha256
(base32
- "0i014lshsdflzw6h0qxra9d2f0q82vffxv2f29awbb9ad0p4rq4q"))))
+ "19bj9nncd1r9g4273h5qx35gs3i4bw5z9bhjni24b413hyj55hkv"))))
(build-system gnu-build-system)
(native-inputs
`(("ocaml" ,ocaml)