mirror/guix
1
0
Fork 0
mirror of https://git.savannah.gnu.org/git/guix.git synced 2025-01-20 06:37:08 +01:00
Code Issues Projects Releases Packages Wiki Activity Actions

gnu: coq: Update to 8.14.0.

Browse source 
* 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.
This commit is contained in:
Julien Lepiller 2021-11-28 16:42:56 +01:00
parent 189501bf3b
commit d95a982cdd
No known key found for this signature in database
GPG key ID: 53D457B2D636EE82
3 changed files with 187 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
gnu/local.mk
View file

@ -951,6 +951,7 @@ dist_patch_DATA = \
%D%/packages/patches/collectd-5.11.0-noinstallvar.patch \
%D%/packages/patches/combinatorial-blas-awpm.patch \
%D%/packages/patches/combinatorial-blas-io-fix.patch \
%D%/packages/patches/coq-fix-envvars.patch \
%D%/packages/patches/coreutils-ls.patch \
%D%/packages/patches/cpuinfo-system-libraries.patch \
%D%/packages/patches/crawl-upgrade-saves.patch \

63
gnu/packages/coq.scm
View file

@ -49,10 +49,10 @@ (define-module (gnu packages coq)
#: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 @@ (define-public coq
(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 @@ (define-public coq
;; 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 @@ (define-public coq-coquelicot
(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 @@ (define-public coq-bignums
(file-name (git-file-name name version))
(sha256
(base32
"1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y"))))
"0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06"))))
(build-system gnu-build-system)
(native-inputs
`(("ocaml" ,ocaml)
@ -537,16 +568,16 @@ (define-public coq-autosubst
(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)

139
gnu/packages/patches/coq-fix-envvars.patch Normal file
View file

@ -0,0 +1,139 @@
From ebe09fcac72b21d17c4e8fe6edc1b6076a4ae97c Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Sun, 21 Nov 2021 00:38:03 +0100
Subject: [PATCH] Fix environment variable usage.
---
checker/checker.ml | 2 ++
lib/envars.ml | 26 ++++++++++++++++----------
sysinit/coqargs.ml | 3 ++-
sysinit/coqloadpath.ml | 3 ++-
sysinit/coqloadpath.mli | 2 +-
tools/coqdep.ml | 2 +-
6 files changed, 24 insertions(+), 14 deletions(-)
diff --git a/checker/checker.ml b/checker/checker.ml
index f55ed9e8d6..3b797729ed 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -104,6 +104,7 @@ let set_include d p =
(* Initializes the LoadPath *)
let init_load_path () =
let coqlib = Envars.coqlib () in
+ let coqcorelib = Envars.coqcorelib () in
let user_contrib = coqlib/"user-contrib" in
let xdg_dirs = Envars.xdg_dirs in
let coqpath = Envars.coqpath in
@@ -111,6 +112,7 @@ let init_load_path () =
CPath.choose_existing
[ CPath.make [ coqlib ; "plugins" ]
; CPath.make [ coqlib ; ".."; "coq-core"; "plugins" ]
+ ; CPath.make [ coqcorelib ; "plugins" ]
] |> function
| None ->
CErrors.user_err (Pp.str "Cannot find plugins directory")
diff --git a/lib/envars.ml b/lib/envars.ml
index 750bd60e71..c7affbd437 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -127,15 +127,21 @@ let check_file_else ~dir ~file oth =
let guess_coqlib fail =
getenv_else "COQLIB" (fun () ->
let prelude = "theories/Init/Prelude.vo" in
- check_file_else ~dir:Coq_config.coqlibsuffix ~file:prelude
- (fun () ->
- if Sys.file_exists (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.")
- )
+ let coqlibpath = getenv_else "COQLIBPATH" (fun () -> Coq_config.coqlibsuffix) in
+ let paths = path_to_list coqlibpath in
+ let valid_paths =
+ List.filter
+ (fun dir -> (check_file_else ~dir:dir ~file:prelude (fun () -> "")) <> "")
+ paths in
+ match valid_paths with
+ | [] ->
+ if Sys.file_exists (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)
let coqlib_ref : string option ref = ref None
let set_user_coqlib path = coqlib_ref := Some path
@@ -208,7 +214,7 @@ let xdg_dirs ~warn =
let print_config ?(prefix_var_name="") f coq_src_subdirs =
let open Printf in
fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ());
- fprintf f "%sCOQCORELIB=%s/\n" prefix_var_name (coqlib () / "../coq-core/");
+ fprintf f "%sCOQCORELIB=%s/\n" prefix_var_name (coqcorelib ());
fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ());
fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ());
fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags;
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index 00f70a5fea..8325623a63 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -453,7 +453,8 @@ let build_load_path opts =
if opts.pre.boot then [],[]
else
let coqlib = Envars.coqlib () in
- Coqloadpath.init_load_path ~coqlib in
+ let coqcorelib = Envars.coqcorelib () in
+ Coqloadpath.init_load_path ~coqlib ~coqcorelib in
ml_path @ opts.pre.ml_includes ,
vo_path @ opts.pre.vo_includes
diff --git a/sysinit/coqloadpath.ml b/sysinit/coqloadpath.ml
index 95ae5da3de..a58cfe6928 100644
--- a/sysinit/coqloadpath.ml
+++ b/sysinit/coqloadpath.ml
@@ -35,7 +35,7 @@ let build_userlib_path ~unix_path =
else [], []
(* LoadPath for Coq user libraries *)
-let init_load_path ~coqlib =
+let init_load_path ~coqlib ~coqcorelib =
let open Loadpath in
let user_contrib = coqlib/"user-contrib" in
@@ -50,6 +50,7 @@ let init_load_path ~coqlib =
CPath.choose_existing
[ CPath.make [ coqlib ; "plugins" ]
; CPath.make [ coqlib ; ".."; "coq-core"; "plugins" ]
+ ; CPath.make [ coqcorelib ; "plugins" ]
] |> function
| None ->
CErrors.user_err (Pp.str "Cannot find plugins directory")
diff --git a/sysinit/coqloadpath.mli b/sysinit/coqloadpath.mli
index d853e9ea54..43c6dfa134 100644
--- a/sysinit/coqloadpath.mli
+++ b/sysinit/coqloadpath.mli
@@ -12,5 +12,5 @@
includes (in-order) Coq's standard library, Coq's [user-contrib]
folder, and directories specified in [COQPATH] and [XDG_DIRS] *)
val init_load_path
- : coqlib:CUnix.physical_path
+ : coqlib:CUnix.physical_path -> coqcorelib:CUnix.physical_path
-> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index c1c87993e1..6c78e10866 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -33,7 +33,7 @@ let coqdep () =
let coqlib = Envars.coqlib () in
let coq_plugins_dir = Filename.concat (Envars.coqcorelib ()) "plugins" in
if not (Sys.file_exists coq_plugins_dir) then
- CErrors.user_err Pp.(str "coqdep: cannot find plugins directory for coqlib: " ++ str coqlib ++ fnl ());
+ CErrors.user_err Pp.(str "coqdep: cannot find plugins directory " ++ str coq_plugins_dir ++ str " for coqlib: " ++ str coqlib ++ fnl ());
CD.add_rec_dir_import CD.add_coqlib_known (coqlib//"theories") ["Coq"];
CD.add_rec_dir_import CD.add_coqlib_known (coq_plugins_dir) ["Coq"];
let user = coqlib//"user-contrib" in
--
2.33.1