@@ -1040,7 +1040,6 @@ dist_patch_DATA = \
%D%/packages/patches/converseen-hide-non-free-pointers.patch \
%D%/packages/patches/cool-retro-term-wctype.patch \
%D%/packages/patches/coreutils-gnulib-tests.patch \
- %D%/packages/patches/coq-fix-envvars.patch \
%D%/packages/patches/cppcheck-disable-char-signedness-test.patch \
%D%/packages/patches/cpuinfo-system-libraries.patch \
%D%/packages/patches/cpulimit-with-glib-2.32.patch \
@@ -31,6 +31,7 @@ (define-module (gnu packages coq)
#:use-module (gnu packages base)
#:use-module (gnu packages bison)
#:use-module (gnu packages boost)
+ #:use-module (gnu packages compression)
#:use-module (gnu packages emacs)
#:use-module (gnu packages flex)
#:use-module (gnu packages gawk)
@@ -50,10 +51,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,28 +64,35 @@ (define-public coq-core
(file-name (git-file-name name version))
(sha256
(base32
- "0ljpqhh5lfsim29fcfp2xfcvm3j84pf1mb0gnpdr8vcqqw7mqwpf"))
- (patches (search-patches "coq-fix-envvars.patch"))))
+ "0gg6hizq0i08lk741b579cbswhy6qvkh6inc3d3i5a2af98psq63"))))
(native-search-paths
(list (search-path-specification
(variable "COQPATH")
- (files (list "lib/ocaml/site-lib/coq/user-contrib"
- "lib/coq/user-contrib")))
- (search-path-specification
- (variable "COQLIBPATH")
- (files (list "lib/ocaml/site-lib/coq")))
- (search-path-specification
- (variable "COQCORELIB")
- (files (list "lib/ocaml/site-lib/coq-core"))
- (separator #f))))
+ (files (list "lib/coq/user-contrib")))))
(build-system dune-build-system)
+ (arguments
+ (list
+ #: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"))
+ (coqlib (string-append out "/lib/ocaml/site-lib/coq/")))
+ (invoke "./configure" "-prefix" out
+ "-libdir" coqlib))))
+ (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" "coq-core" "coq-stdlib")))))))
(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 +104,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)
@@ -147,7 +122,7 @@ (define-public coq-ide
`(#:tests? #f
#:package "coqide"))
(propagated-inputs
- (list coq coq-ide-server))
+ (list coq coq-ide-server zlib))
(inputs
(list lablgtk3 ocaml-lablgtk3-sourceview3))))
@@ -555,16 +530,16 @@ (define-public coq-autosubst
(define-public coq-equations
(package
(name "coq-equations")
- (version "1.3")
+ (version "1.3-8.17")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/mattam82/Coq-Equations")
- (commit (string-append "v" version "-8.16"))))
+ (commit (string-append "v" version))))
(file-name (git-file-name name version))
(sha256
(base32
- "08f756vgdd1wklkarg0b93j4n5mhkqm5ixxrhyb23dcv2dwhc8yg"))))
+ "0g68h4c1ijpphixvl9wkd7sibds38v4236dpvvh194j5ii42vnn8"))))
(build-system gnu-build-system)
(native-inputs
(list ocaml coq camlp5))
@@ -716,7 +691,7 @@ (define-public coq-mathcomp-finmap
"/lib/coq/user-contrib"))
#:phases (modify-phases %standard-phases
(delete 'configure))))
- (inputs (list coq coq-stdlib coq-mathcomp which))
+ (inputs (list coq coq coq-mathcomp which))
(synopsis "Finite sets and finite types for coq-mathcomp")
(description
"This library is an extension of coq-mathcomp which supports finite sets
@@ -747,7 +722,7 @@ (define-public coq-mathcomp-bigenough
;; by the packaged project in the future.
#:tests? #f
#:make-flags ,#~(list (string-append "COQBIN="
- #$(this-package-input "coq-core")
+ #$(this-package-input "coq")
"/bin/")
(string-append "COQMF_COQLIB="
(assoc-ref %outputs "out")
@@ -757,7 +732,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
deleted file mode 100644
@@ -1,53 +0,0 @@
-From 0e76cda958a4d3e4bcbb96e171c26b6b3478c6c2 Mon Sep 17 00:00:00 2001
-From: Julien Lepiller <julien@lepiller.eu>
-Date: Thu, 10 Feb 2022 16:44:10 +0100
-Subject: [PATCH] Fix environment variable usage.
-
----
- boot/env.ml | 26 +++++++++++++++++++-------
- 1 file changed, 19 insertions(+), 7 deletions(-)
-
-diff --git a/boot/env.ml b/boot/env.ml
-index e8521e7..d834a3a 100644
---- a/boot/env.ml
-+++ b/boot/env.ml
-@@ -32,17 +32,29 @@ let fail_msg =
-
- let fail s = Format.eprintf "%s@\n%!" fail_msg; exit 1
-
-+let path_to_list p =
-+ let sep = if String.equal Sys.os_type "Win32" then ';' else ':' in
-+ String.split_on_char sep p
-+
- (* This code needs to be refactored, for now it is just what used to be in envvars *)
- let guess_coqlib () =
- Util.getenv_else "COQLIB" (fun () ->
- let prelude = "theories/Init/Prelude.vo" in
-- Util.check_file_else
-- ~dir:Coq_config.coqlibsuffix
-- ~file:prelude
-- (fun () ->
-- if Sys.file_exists (Filename.concat Coq_config.coqlib prelude)
-- then Coq_config.coqlib
-- else fail ()))
-+ let coqlibpath = Util.getenv_else "COQLIBPATH" (fun () -> Coq_config.coqlibsuffix) in
-+ let paths = path_to_list coqlibpath in
-+ let valid_paths =
-+ List.filter
-+ (fun dir -> (Util.check_file_else ~dir:dir ~file:prelude (fun () -> "")) <> "")
-+ paths in
-+ match valid_paths with
-+ | [] ->
-+ if Sys.file_exists (Filename.concat Coq_config.coqlib prelude)
-+ then Coq_config.coqlib
-+ else
-+ fail "cannot guess a path for Coq libraries; please use -coqlib option \
-+ or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) \
-+ If you intend to use Coq without a standard library, the -boot -noinit options must be used."
-+ | p::_ -> p)
-
- (* Build layout uses coqlib = coqcorelib *)
- let guess_coqcorelib lib =
-2.34.0
-