From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp2 ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id qGRrNzC8o2HtoQAAgWs5BA (envelope-from ) for ; Sun, 28 Nov 2021 18:28:16 +0100 Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp2 with LMTPS id 4NIAMzC8o2H9NAAAB5/wlQ (envelope-from ) for ; Sun, 28 Nov 2021 17:28:16 +0000 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id 8F7F52FFAB for ; Sun, 28 Nov 2021 18:28:16 +0100 (CET) Received: from localhost ([::1]:43474 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1mrNyJ-0007oN-P0 for larch@yhetil.org; Sun, 28 Nov 2021 12:28:15 -0500 Received: from eggs.gnu.org ([209.51.188.92]:32944) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1mrNy7-0007ka-Ej for guix-patches@gnu.org; Sun, 28 Nov 2021 12:28:03 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:52997) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1mrNy7-0005si-5n for guix-patches@gnu.org; Sun, 28 Nov 2021 12:28:03 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1mrNy7-0007NB-3N for guix-patches@gnu.org; Sun, 28 Nov 2021 12:28:03 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#52164] [PATCH 3/3] gnu: coq: Update to 8.14.0. Resent-From: Julien Lepiller Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 28 Nov 2021 17:28:03 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 52164 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 52164@debbugs.gnu.org Received: via spool by 52164-submit@debbugs.gnu.org id=B52164.163812045528291 (code B ref 52164); Sun, 28 Nov 2021 17:28:03 +0000 Received: (at 52164) by debbugs.gnu.org; 28 Nov 2021 17:27:35 +0000 Received: from localhost ([127.0.0.1]:36308 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrNxX-0007M0-PW for submit@debbugs.gnu.org; Sun, 28 Nov 2021 12:27:35 -0500 Received: from lepiller.eu ([89.234.186.109]:38862) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrNxT-0007LS-FS for 52164@debbugs.gnu.org; Sun, 28 Nov 2021 12:27:24 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id d30ff2c9 for <52164@debbugs.gnu.org>; Sun, 28 Nov 2021 17:27:18 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=from:to :subject:date:message-id:in-reply-to:references:mime-version :content-transfer-encoding; s=dkim; bh=680gNOFoHQqSlwNBKhvY2Y9hw 7SdJO0aaWHGCA98VMI=; b=cu3A/CvXYlq8+H6e4I6LoYbY61xyLV6mRqKnqhX9S bRWS3sDddXVG3ZlNCS/bKUg6zVf75OiVDr+kDw0hJOD6IbdV2AX+Vx6SKdvjZZFC M9BeAKJ2SNkgQX6yBtBDp6SP1TjTTFNw3VNPtoZwLkxIy9Ia0DpanrphmNI2pyJv eVEtxSE/elDefQCpW91cJO8uOGoTvLIAUoH4VLgIdto9CHX1Ztqp/PlUm/iOlcBo LbS1G8Bt1Y9OBSQjVf7sFxdNHuSe5NgUYy5veaV+nuLNTkVm5RKEabyxvYOObhq+ v6VJpEsgN/slNECTUnXZZVEQzY/Ias/ZSYVS8+wSkJrnQ== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id d187f1c7 (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO) for <52164@debbugs.gnu.org>; Sun, 28 Nov 2021 17:27:18 +0000 (UTC) From: Julien Lepiller Date: Sun, 28 Nov 2021 18:27:11 +0100 Message-Id: X-Mailer: git-send-email 2.34.0 In-Reply-To: <20211128174408.747bccba@tachikoma.lepiller.eu> References: <20211128174408.747bccba@tachikoma.lepiller.eu> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: "Guix-patches" X-Migadu-Flow: FLOW_IN ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1638120496; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding:resent-cc: resent-from:resent-sender:resent-message-id:in-reply-to:in-reply-to: references:references:list-id:list-help:list-unsubscribe: list-subscribe:list-post:dkim-signature; bh=7Kgs4ay9aDflGCsC6pKUSBEm9JEpA2dv/EOhFhzyJbw=; b=b4V5io+9VULMr4hs+bqkFaBOFy41MZw1DgWE2LyqkcJ8xArMuZ8yc19kVsneXhTRYSpyIb qDi9neBjDA6nyfHnsYBgFhAKn84bfI0RURuKYLTUE86wVvLStWieR7Y7GbqDRUrLy+Mbr7 AEPSu82xJPU3A1MNL5PMpZhi4/cHM4FMqUDpBbvgA2W47LiNnx3D1Bt9BzIx/i2ei3puZ7 R+M/ZdxYTH873FMDCiUBfgS6oDdjQHQ02Q98ZZ/TX4dnizxfB9Apg8SmqVwUyjrDZ39fF2 uvU78v8nXHrJk+u5MqbEAl5ma3Cb96bHKbWyg6qW7UAsECo0kN/hTI045HrmYA== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1638120496; a=rsa-sha256; cv=none; b=a9HHzAQPglOGw+rh1/Xznoo/gCECx0DsRfAYpC/jBptfDapi5eVSvBJaTG2IWJDpvzIfV3 dYc/nTZ4VzufKRfUfokLxpHfF4/oJLWTmgxlH4b1DM96TYr/R3WkdN+uENIXByv32yn2DV AWmTNkpqv0kGfQ8Mh9mBT+IV/CQY+ougKIDAx1Qp2TUUMGsQCI0Dil0s2Myvm2gQNmbecO CuGCfwIklHqWDL6t2W5sUSba45RCyoo6vWIwnvUHrdimlSVl9RYrBcVio92id0nv6etZXY bzJpo3MdHlkpETSdp9MGaVgH+VzbNKHtirZ8BItAhx/JPVZ8GIB73YloT6tHLw== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=lepiller.eu header.s=dkim header.b="cu3A/CvX"; dmarc=fail reason="SPF not aligned (relaxed)" header.from=lepiller.eu (policy=none); spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org X-Migadu-Spam-Score: 3.19 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=lepiller.eu header.s=dkim header.b="cu3A/CvX"; dmarc=fail reason="SPF not aligned (relaxed)" header.from=lepiller.eu (policy=none); spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org X-Migadu-Queue-Id: 8F7F52FFAB X-Spam-Score: 3.19 X-Migadu-Scanner: scn1.migadu.com X-TUID: MpPyqNgvpf/p * 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 | 65 +++++++--- gnu/packages/patches/coq-fix-envvars.patch | 139 +++++++++++++++++++++ 3 files changed, 188 insertions(+), 17 deletions(-) create mode 100644 gnu/packages/patches/coq-fix-envvars.patch diff --git a/gnu/local.mk b/gnu/local.mk index efe153faf2..b26907a211 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 2045901aed..b6a5ff357c 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -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) @@ -471,7 +502,7 @@ (define-public coq-interval (arguments `(#:configure-flags (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out") - "/lib/coq/user-contrib")) + "/lib/ocaml/site-lib/coq/user-contrib")) #:phases (modify-phases %standard-phases (add-before 'configure 'fix-remake @@ -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) 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 -- 2.33.1