From bcd4c7ae6a8e8374cc75a5daf8e8b27138dc162f Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Sun, 28 Nov 2021 17:39:01 +0100 Subject: gnu: coq-semantics: Update to 8.14.0. * gnu/packages/coq.scm (coq-semantics): Update to 8.14.0. --- gnu/packages/coq.scm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index a27ec53ecb..e3c4190ac3 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -576,7 +576,7 @@ kernel.") (define-public coq-semantics (package (name "coq-semantics") - (version "8.13.0") + (version "8.14.0") (source (origin (method git-fetch) @@ -591,7 +591,7 @@ kernel.") (file-name (git-file-name name version)) (sha256 (base32 - "0m5si9dsv96z92gy4xaqz8mzyz8zp7j1sp542l0wzsp5xgyfpc7i")))) + "0ldrp86bfcjpzsb08p45sgs3aczjzr1gksy5dsf7pxapg05pc7ac")))) (build-system gnu-build-system) (native-inputs `(("coq" ,coq) -- cgit v1.2.3 From 189501bf3b8facced98f08e73b7cdb83ec7a272b Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Sun, 28 Nov 2021 17:41:19 +0100 Subject: gnu: proof-general: Update to latest commit. * gnu/packages/coq.scm (proof-general): Update to latest commit. [license]: Change to glp3+. --- gnu/packages/coq.scm | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index e3c4190ac3..8d967241f5 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -119,9 +119,9 @@ It is developed using Objective Caml and Camlp5.") (define-public proof-general ;; The latest release is from 2016 and there has been more than 450 commits ;; since then. - ;; Commit from 2021-06-07. - (let ((commit "bc86736abb728ec0d28abc90ef0adae21d29a66a") - (revision "0")) + ;; Commit from 2021-11-25. + (let ((commit "1b1083e86e0cddc20ff2f1a6b25c7a7eee2edf02") + (revision "1")) (package (name "proof-general") (version (git-version "4.4" revision commit)) @@ -133,7 +133,7 @@ It is developed using Objective Caml and Camlp5.") (file-name (git-file-name name version)) (sha256 (base32 - "00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa")))) + "1pnysczhscapgwmvf6ix7f31lf3hnh8h977bfll1m7jlxl9b9c0j")))) (build-system gnu-build-system) (native-inputs `(("emacs" ,emacs-minimal) @@ -201,7 +201,7 @@ It is developed using Objective Caml and Camlp5.") "Proof General is a major mode to turn Emacs into an interactive proof assistant to write formal mathematical proofs using a variety of theorem provers.") - (license license:gpl2+)))) + (license license:gpl3+)))) (define-public coq-flocq (package -- cgit v1.2.3 From d95a982cdd898790d247f013440f08a448265e3f Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Sun, 28 Nov 2021 16:42:56 +0100 Subject: 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. --- gnu/local.mk | 1 + gnu/packages/coq.scm | 63 +++++++++---- gnu/packages/patches/coq-fix-envvars.patch | 139 +++++++++++++++++++++++++++++ 3 files changed, 187 insertions(+), 16 deletions(-) create mode 100644 gnu/packages/patches/coq-fix-envvars.patch (limited to 'gnu/packages/coq.scm') diff --git a/gnu/local.mk b/gnu/local.mk index b1eb41d4fc..a5c0486c94 100644 --- a/gnu/local.mk +++ b/gnu/local.mk @@ -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 \ 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) diff --git a/gnu/packages/patches/coq-fix-envvars.patch b/gnu/packages/patches/coq-fix-envvars.patch new file mode 100644 index 0000000000..deecf5ce74 --- /dev/null +++ b/gnu/packages/patches/coq-fix-envvars.patch @@ -0,0 +1,139 @@ +From ebe09fcac72b21d17c4e8fe6edc1b6076a4ae97c Mon Sep 17 00:00:00 2001 +From: Julien Lepiller +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 -- cgit v1.2.3