From patchwork Sun Nov 28 17:27:09 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Julien Lepiller X-Patchwork-Id: 34863 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id B515527BBE9; Sun, 28 Nov 2021 17:28:14 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-3.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,MAILING_LIST_MULTI,RCVD_IN_MSPIKE_H2,SPF_HELO_PASS, URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id F16E627BBEA for ; Sun, 28 Nov 2021 17:28:13 +0000 (GMT) Received: from localhost ([::1]:43410 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1mrNyH-0007lJ-0J for patchwork@mira.cbaines.net; Sun, 28 Nov 2021 12:28:13 -0500 Received: from eggs.gnu.org ([209.51.188.92]:32938) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1mrNy6-0007kA-Tj for guix-patches@gnu.org; Sun, 28 Nov 2021 12:28:02 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:52995) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1mrNy6-0005sW-LV for guix-patches@gnu.org; Sun, 28 Nov 2021 12:28:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1mrNy6-0007Mw-A4 for guix-patches@gnu.org; Sun, 28 Nov 2021 12:28:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#52164] [PATCH 1/3] gnu: ocaml-semantics: 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:02 +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.163812044428259 (code B ref 52164); Sun, 28 Nov 2021 17:28:02 +0000 Received: (at 52164) by debbugs.gnu.org; 28 Nov 2021 17:27:24 +0000 Received: from localhost ([127.0.0.1]:36304 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrNxU-0007Lj-4B for submit@debbugs.gnu.org; Sun, 28 Nov 2021 12:27:24 -0500 Received: from lepiller.eu ([89.234.186.109]:38862) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrNxP-0007LS-8i for 52164@debbugs.gnu.org; Sun, 28 Nov 2021 12:27:22 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 81c079cc for <52164@debbugs.gnu.org>; Sun, 28 Nov 2021 17:27:17 +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=LmiuDsE7ZXPdLCtp5qIvI5THL Abx6j6fmlrYKnuTOlg=; b=QUGOkat3IYgnVVn+yKIv2NxvpMGyslC9ONj+9LADk tieJwO4Pwv44dYYbIenUsQuH9AlRmobf/iKU/NLXGu9gzXc/ctwT4fyYw+1NC1cr 8al3NTwW2v5r+r+N0tH+jfUsZji7uUw+A5uETEdu9DH6ULXDCQqdbVr7ftd1sxvc 8SwT1m8PwFeSA4/30uVjghTPjvNFvmn0ch9WrjQ++3eCTDENwSw4DZtOqz+diVHN GEotS/TZZ6K2Zs0BCv61YKqWwH4SZokLq5GVN/Uh7m0jYWJgOstaS6Ywod9XMfL2 09HHhXzhjkwxXlQ47Rfu2kZX5svgWAzg3cjuLly7JCO0A== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id ac92b9c5 (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO) for <52164@debbugs.gnu.org>; Sun, 28 Nov 2021 17:27:17 +0000 (UTC) From: Julien Lepiller Date: Sun, 28 Nov 2021 18:27:09 +0100 Message-Id: <854d751e7d512c66acb72225120168e5ee16d6a2.1638120398.git.julien@lepiller.eu> 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 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+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches --- gnu/packages/coq.scm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 @@ (define-public coq-equations (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 @@ (define-public coq-semantics (file-name (git-file-name name version)) (sha256 (base32 - "0m5si9dsv96z92gy4xaqz8mzyz8zp7j1sp542l0wzsp5xgyfpc7i")))) + "0ldrp86bfcjpzsb08p45sgs3aczjzr1gksy5dsf7pxapg05pc7ac")))) (build-system gnu-build-system) (native-inputs `(("coq" ,coq) From patchwork Sun Nov 28 17:27:10 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Julien Lepiller X-Patchwork-Id: 34862 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 418F127BBEB; Sun, 28 Nov 2021 17:28:14 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-3.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,MAILING_LIST_MULTI,RCVD_IN_MSPIKE_H2,SPF_HELO_PASS, URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id F031327BBE9 for ; Sun, 28 Nov 2021 17:28:13 +0000 (GMT) Received: from localhost ([::1]:43416 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1mrNyH-0007lf-10 for patchwork@mira.cbaines.net; Sun, 28 Nov 2021 12:28:13 -0500 Received: from eggs.gnu.org ([209.51.188.92]:32940) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1mrNy7-0007kF-1s for guix-patches@gnu.org; Sun, 28 Nov 2021 12:28:03 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:52996) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1mrNy6-0005sa-Pd for guix-patches@gnu.org; Sun, 28 Nov 2021 12:28:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1mrNy6-0007N4-N7 for guix-patches@gnu.org; Sun, 28 Nov 2021 12:28:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#52164] [PATCH 2/3] gnu: proof-general: Update to latest commit. Resent-From: Julien Lepiller Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 28 Nov 2021 17:28:02 +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.163812044728275 (code B ref 52164); Sun, 28 Nov 2021 17:28:02 +0000 Received: (at 52164) by debbugs.gnu.org; 28 Nov 2021 17:27:27 +0000 Received: from localhost ([127.0.0.1]:36306 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrNxX-0007Ly-DS for submit@debbugs.gnu.org; Sun, 28 Nov 2021 12:27:27 -0500 Received: from lepiller.eu ([89.234.186.109]:38862) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrNxS-0007LS-IQ for 52164@debbugs.gnu.org; Sun, 28 Nov 2021 12:27:23 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 7c811c7d 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=c/Tr1jMIU4f18LwqyCQMkA0rP WcB0puNrW1dvR+26xc=; b=P85/C/x1kzGK9CBiLwVgkDygsxikOvOBH6ggwDeCH TzCatwUT0LLoFrDFzXiY4BHsLWu2kG5nGRmxtN0dWAaivMFgrZRQXRybOTJmWRzZ CtwtK2u7WLGVyN7jr+O7vYY5mM1dDIaQuaFgjZfCDmY4WNpS/uCtObkATMa7RKe+ qdEHlsn2wCw1DW/Uxe6D5G+kH5CHzZvZ60ydW7npgHTGzYFXGo0thPrA/zZ7K+zv Tluk/sjpfJQTeyVpkhmVKunHe6yfewWxpSOaWTfRCGxI7lDWGY5P933LMecwN0u9 27O7NOVWwBuNCGUMAPQ/wf2YHLhp4oSduivWn3z1/arcQ== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 8577d61a (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO) for <52164@debbugs.gnu.org>; Sun, 28 Nov 2021 17:27:17 +0000 (UTC) From: Julien Lepiller Date: Sun, 28 Nov 2021 18:27:10 +0100 Message-Id: <2e3b3fe2ed163577a854f10b9a1c8531eabcadf6.1638120398.git.julien@lepiller.eu> 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 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+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches * gnu/packages/coq.scm (proof-general): Update to latest commit. --- gnu/packages/coq.scm | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index e3c4190ac3..2045901aed 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -119,9 +119,9 @@ (define-public coq-ide (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 @@ (define-public proof-general (file-name (git-file-name name version)) (sha256 (base32 - "00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa")))) + "1pnysczhscapgwmvf6ix7f31lf3hnh8h977bfll1m7jlxl9b9c0j")))) (build-system gnu-build-system) (native-inputs `(("emacs" ,emacs-minimal) From patchwork Sun Nov 28 17:27:11 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Julien Lepiller X-Patchwork-Id: 34864 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 97C4627BBEA; Sun, 28 Nov 2021 17:28:16 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-3.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,MAILING_LIST_MULTI,RCVD_IN_MSPIKE_H2,SPF_HELO_PASS, URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 8115727BBE9 for ; Sun, 28 Nov 2021 17:28:15 +0000 (GMT) Received: from localhost ([::1]:43474 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1mrNyI-0007oN-NN for patchwork@mira.cbaines.net; Sun, 28 Nov 2021 12:28:14 -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 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+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches * 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