From unknown Sat Jun 14 14:26:25 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#43325] [PATCH] gnu: Update coq and its dependents Resent-From: Robin Green Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Fri, 11 Sep 2020 07:31:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 43325 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 43325@debbugs.gnu.org Cc: Robin Green X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.15998094532433 (code B ref -1); Fri, 11 Sep 2020 07:31:01 +0000 Received: (at submit) by debbugs.gnu.org; 11 Sep 2020 07:30:53 +0000 Received: from localhost ([127.0.0.1]:42194 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kGdWG-0000dB-Ks for submit@debbugs.gnu.org; Fri, 11 Sep 2020 03:30:53 -0400 Received: from lists.gnu.org ([209.51.188.17]:38742) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kGdWE-0000d2-8Z for submit@debbugs.gnu.org; Fri, 11 Sep 2020 03:30:50 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:47708) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1kGdWB-0007Xk-2a for guix-patches@gnu.org; Fri, 11 Sep 2020 03:30:50 -0400 Received: from [67.214.171.71] (port=51918 helo=mail.dnsexit.com) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1kGdW9-00024G-6s for guix-patches@gnu.org; Fri, 11 Sep 2020 03:30:46 -0400 Received: from localhost (localhost.localdomain [127.0.0.1]) by mail.dnsexit.com (Postfix) with ESMTP id 3B4EA3C0816 for ; Fri, 11 Sep 2020 03:30:42 -0400 (EDT) X-Virus-Scanned: amavisd-new at dnsexit.com Received: from mail.dnsexit.com ([127.0.0.1]) by localhost (box2.dnsexit.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id H0tVMJ9javdj; Fri, 11 Sep 2020 03:30:42 -0400 (EDT) Received: from localhost.localdomain (greenrd.plus.com [212.159.116.150]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by mail.dnsexit.com (Postfix) with ESMTPSA id 999453C083B; Fri, 11 Sep 2020 03:30:40 -0400 (EDT) From: Robin Green Date: Fri, 11 Sep 2020 08:30:27 +0100 Message-Id: <20200911073027.6485-1-greenrd@greenrd.org> X-Mailer: git-send-email 2.28.0 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Host-Lookup-Failed: Reverse DNS lookup failed for 67.214.171.71 (failed) Received-SPF: pass client-ip=67.214.171.71; envelope-from=greenrd@greenrd.org; helo=mail.dnsexit.com X-detected-operating-system: by eggs.gnu.org: First seen = 2020/09/11 03:30:43 X-ACL-Warn: Detected OS = Linux 3.1-3.10 [fuzzy] X-Spam_score_int: -10 X-Spam_score: -1.1 X-Spam_bar: - X-Spam_report: (-1.1 / 5.0 requ) BAYES_00=-1.9, RDNS_NONE=0.793, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=no autolearn_force=no X-Spam_action: no action X-Spam-Score: -1.3 (-) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -2.3 (--) * gnu/packages/coq.scm (coq): Update to 8.11.2 (coq-flocq): Update to 3.3.1 (coq-gappa): Update to 1.4.4 (coq-mathcomp): Update to 1.11.0 (coq-coquelicot): Update to 3.1.0 (coq-bignums): Update to 8.11.0 (coq-interval): Update to 4.0.0 (coq-equations): Update to 1.2.3 --- gnu/packages/coq.scm | 45 +++++++++++++++++++++++--------------------- 1 file changed, 24 insertions(+), 21 deletions(-) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 3573518763..2d8dca8d46 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -34,6 +34,7 @@ #:use-module (gnu packages ocaml) #:use-module (gnu packages perl) #:use-module (gnu packages python) + #:use-module (gnu packages rsync) #:use-module (gnu packages texinfo) #:use-module (guix build-system gnu) #:use-module (guix build-system ocaml) @@ -47,7 +48,7 @@ (define-public coq (package (name "coq") - (version "8.10.2") + (version "8.11.2") (source (origin (method git-fetch) @@ -57,7 +58,7 @@ (file-name (git-file-name name version)) (sha256 (base32 - "0ji2rzd70b3hcwfw97qk7rv3m2977ylqnq82l1555dp3njr8nm3q")))) + "1gia82dkmzqspw2w3s4gjyh39ghbmw4i41i4hyzc91g7mza17nbz")))) (native-search-paths (list (search-path-specification (variable "COQPATH") @@ -70,7 +71,8 @@ ("camlp5" ,camlp5) ("ocaml-num" ,ocaml-num))) (native-inputs - `(("ocaml-ounit" ,ocaml-ounit))) + `(("ocaml-ounit" ,ocaml-ounit) + ("rsync" ,rsync))) (arguments `(#:phases (modify-phases %standard-phases @@ -121,11 +123,12 @@ (add-after 'install 'check (lambda _ (with-directory-excursion "test-suite" - ;; These two tests fail. + ;; These three tests fail. ;; Fails because the output is not formatted as expected. (delete-file-recursively "coq-makefile/timing") - ;; Fails because we didn't build coqtop.byte. - (delete-file-recursively "coq-makefile/findlib-package") + ;; Fail because we didn't build coqtop.byte. + (delete-file-recursively "coq-makefile/findlib-package-unpacked") + (delete-file "misc/printers.sh") (invoke "make"))))))) (home-page "https://coq.inria.fr") (synopsis "Proof assistant for higher-order logic") @@ -215,7 +218,7 @@ provers.") (define-public coq-flocq (package (name "coq-flocq") - (version "3.2.0") + (version "3.3.1") (source (origin (method git-fetch) @@ -225,7 +228,7 @@ provers.") (file-name (git-file-name name version)) (sha256 (base32 - "15bi36x7zj0glsb3s2gwqd4wswhfzh36rbp7imbyff53a7nna95l")))) + "01gdykva0lcw6y3dm8j0djxayb87szfg9vn0mxd6z3pks644misl")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -272,7 +275,7 @@ inside Coq.") (define-public coq-gappa (package (name "coq-gappa") - (version "1.4.2") + (version "1.4.4") (source (origin (method git-fetch) @@ -282,7 +285,7 @@ inside Coq.") (file-name (git-file-name name version)) (sha256 (base32 - "0r7jwp5xssdfzivs2flp7mzrscqhgl63mryhhf1cvndpgzqwfk2f")))) + "0f3g3wjkvfkm961l4jpckhsqd43jnvm7f5qqk78qc32zh1fg339n")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -332,7 +335,7 @@ assistant.") (define-public coq-mathcomp (package (name "coq-mathcomp") - (version "1.10.0") + (version "1.11.0") (source (origin (method git-fetch) @@ -341,7 +344,7 @@ assistant.") (commit (string-append "mathcomp-" version)))) (file-name (git-file-name name version)) (sha256 - (base32 "1h5h1c2025r1ms5qryvwy6pikxmpmmjav6yl127xpzmqdi6w732d")))) + (base32 "1axywpa1jcpnidd86irpd1gdbbg2sfbwc652675xisq5wnmfmf6f")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) @@ -374,7 +377,7 @@ part of the distribution.") (define-public coq-coquelicot (package (name "coq-coquelicot") - (version "3.0.3") + (version "3.1.0") (source (origin (method git-fetch) @@ -384,7 +387,7 @@ part of the distribution.") (file-name (git-file-name name version)) (sha256 (base32 - "0m5wbr2s8lnf8b7cfwv15hyzsmbcaz6hgdn7aazcrkxnwr87vgkp")))) + "0mz3pxan1237fr5fi79c66y7b9z7bmi0sc45kwrmkczsjm5462jm")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -427,7 +430,7 @@ theorems between the two libraries.") (define-public coq-bignums (package (name "coq-bignums") - (version "8.10.0") + (version "8.11.0") (source (origin (method git-fetch) (uri (git-reference @@ -436,7 +439,7 @@ theorems between the two libraries.") (file-name (git-file-name name version)) (sha256 (base32 - "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5")))) + "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) @@ -460,7 +463,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.") (define-public coq-interval (package (name "coq-interval") - (version "3.4.1") + (version "4.0.0") (source (origin (method git-fetch) @@ -470,7 +473,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.") (file-name (git-file-name name version)) (sha256 (base32 - "03q3dfqi3r3f7aji5s06ig4aav9ajcwswwdzi5lrgr69z0m487k4")))) + "01iz6qmnsm6b9s1vmdjs79vjx9xgwzn5rwyjp6bvs8hg3zlmhpip")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -556,16 +559,16 @@ uses Ltac to synthesize the substitution operation.") (define-public coq-equations (package (name "coq-equations") - (version "1.2.1") + (version "1.2.3") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/mattam82/Coq-Equations") - (commit (string-append "v" version "-8.10-2")))) + (commit (string-append "v" version "-8.11")))) (file-name (git-file-name name version)) (sha256 (base32 - "0j3z4l5nrbyi9zbbyqkc6kassjanwld2188mwmrbqspaypm2ys68")))) + "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) -- 2.28.0 From unknown Sat Jun 14 14:26:25 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#43325] [PATCH] gnu: Update coq and its dependents References: <20200911073027.6485-1-greenrd@greenrd.org> In-Reply-To: <20200911073027.6485-1-greenrd@greenrd.org> Resent-From: Robin Green Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 13 Sep 2020 14:44:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 43325 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 43325@debbugs.gnu.org Received: via spool by 43325-submit@debbugs.gnu.org id=B43325.160000821716799 (code B ref 43325); Sun, 13 Sep 2020 14:44:01 +0000 Received: (at 43325) by debbugs.gnu.org; 13 Sep 2020 14:43:37 +0000 Received: from localhost ([127.0.0.1]:51297 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kHTE8-0004Mt-Q1 for submit@debbugs.gnu.org; Sun, 13 Sep 2020 10:43:37 -0400 Received: from [67.214.171.71] (port=50793 helo=mail.dnsexit.com) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kHTE6-0004Mi-Nt for 43325@debbugs.gnu.org; Sun, 13 Sep 2020 10:43:35 -0400 Received: from [10.137.0.6] (greenrd.plus.com [212.159.116.150]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by mail.dnsexit.com (Postfix) with ESMTPSA id 699C43C101E for <43325@debbugs.gnu.org>; Sun, 13 Sep 2020 10:43:28 -0400 (EDT) From: Robin Green Message-ID: <347d318b-8b4c-4207-a080-e0a216a7448a@greenrd.org> Date: Sun, 13 Sep 2020 15:43:28 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.11.0 MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="------------5E05156E34112582443CE76A" Content-Language: en-US X-Spam-Score: 1.3 (+) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: Updated patch, fixing a test that I mistakenly removed in the previous version. From a435d45d5777e0a9d0350bc4871d700190cd817b Mon Sep 17 00:00:00 2001 From: Robin Green Date: Sun, 13 Sep 2020 15:12:18 +0100 Subject: [PATCH] gnu: Update coq and its dependents Content analysis details: (1.3 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- -0.0 SPF_PASS SPF: sender matches SPF record 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record 1.3 RDNS_NONE Delivered to internal network by a host with no rDNS X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 0.3 (/) This is a multi-part message in MIME format. --------------5E05156E34112582443CE76A Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Updated patch, fixing a test that I mistakenly removed in the previous version. --------------5E05156E34112582443CE76A Content-Type: text/x-patch; charset=UTF-8; name="0001-gnu-Update-coq-and-its-dependents.patch" Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename="0001-gnu-Update-coq-and-its-dependents.patch" >From a435d45d5777e0a9d0350bc4871d700190cd817b Mon Sep 17 00:00:00 2001 From: Robin Green Date: Sun, 13 Sep 2020 15:12:18 +0100 Subject: [PATCH] gnu: Update coq and its dependents * gnu/packages/coq.scm (coq): Update to 8.11.2 (coq-flocq): Update to 3.3.1 (coq-gappa): Update to 1.4.4 (coq-mathcomp): Update to 1.11.0 (coq-coquelicot): Update to 3.1.0 (coq-bignums): Update to 8.11.0 (coq-interval): Update to 4.0.0 (coq-equations): Update to 1.2.3 --- gnu/packages/coq.scm | 41 ++++++++++++++++++++++------------------- 1 file changed, 22 insertions(+), 19 deletions(-) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 3573518763..44317efd1c 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -34,6 +34,7 @@ #:use-module (gnu packages ocaml) #:use-module (gnu packages perl) #:use-module (gnu packages python) + #:use-module (gnu packages rsync) #:use-module (gnu packages texinfo) #:use-module (guix build-system gnu) #:use-module (guix build-system ocaml) @@ -47,7 +48,7 @@ (define-public coq (package (name "coq") - (version "8.10.2") + (version "8.11.2") (source (origin (method git-fetch) @@ -57,7 +58,7 @@ (file-name (git-file-name name version)) (sha256 (base32 - "0ji2rzd70b3hcwfw97qk7rv3m2977ylqnq82l1555dp3njr8nm3q")))) + "1gia82dkmzqspw2w3s4gjyh39ghbmw4i41i4hyzc91g7mza17nbz")))) (native-search-paths (list (search-path-specification (variable "COQPATH") @@ -70,7 +71,9 @@ ("camlp5" ,camlp5) ("ocaml-num" ,ocaml-num))) (native-inputs - `(("ocaml-ounit" ,ocaml-ounit))) + `(("ocaml-ounit" ,ocaml-ounit) + ("rsync" ,rsync) + ("which" ,which))) (arguments `(#:phases (modify-phases %standard-phases @@ -125,7 +128,7 @@ ;; Fails because the output is not formatted as expected. (delete-file-recursively "coq-makefile/timing") ;; Fails because we didn't build coqtop.byte. - (delete-file-recursively "coq-makefile/findlib-package") + (delete-file "misc/printers.sh") (invoke "make"))))))) (home-page "https://coq.inria.fr") (synopsis "Proof assistant for higher-order logic") @@ -215,7 +218,7 @@ provers.") (define-public coq-flocq (package (name "coq-flocq") - (version "3.2.0") + (version "3.3.1") (source (origin (method git-fetch) @@ -225,7 +228,7 @@ provers.") (file-name (git-file-name name version)) (sha256 (base32 - "15bi36x7zj0glsb3s2gwqd4wswhfzh36rbp7imbyff53a7nna95l")))) + "01gdykva0lcw6y3dm8j0djxayb87szfg9vn0mxd6z3pks644misl")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -272,7 +275,7 @@ inside Coq.") (define-public coq-gappa (package (name "coq-gappa") - (version "1.4.2") + (version "1.4.4") (source (origin (method git-fetch) @@ -282,7 +285,7 @@ inside Coq.") (file-name (git-file-name name version)) (sha256 (base32 - "0r7jwp5xssdfzivs2flp7mzrscqhgl63mryhhf1cvndpgzqwfk2f")))) + "0f3g3wjkvfkm961l4jpckhsqd43jnvm7f5qqk78qc32zh1fg339n")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -332,7 +335,7 @@ assistant.") (define-public coq-mathcomp (package (name "coq-mathcomp") - (version "1.10.0") + (version "1.11.0") (source (origin (method git-fetch) @@ -341,7 +344,7 @@ assistant.") (commit (string-append "mathcomp-" version)))) (file-name (git-file-name name version)) (sha256 - (base32 "1h5h1c2025r1ms5qryvwy6pikxmpmmjav6yl127xpzmqdi6w732d")))) + (base32 "1axywpa1jcpnidd86irpd1gdbbg2sfbwc652675xisq5wnmfmf6f")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) @@ -374,7 +377,7 @@ part of the distribution.") (define-public coq-coquelicot (package (name "coq-coquelicot") - (version "3.0.3") + (version "3.1.0") (source (origin (method git-fetch) @@ -384,7 +387,7 @@ part of the distribution.") (file-name (git-file-name name version)) (sha256 (base32 - "0m5wbr2s8lnf8b7cfwv15hyzsmbcaz6hgdn7aazcrkxnwr87vgkp")))) + "0mz3pxan1237fr5fi79c66y7b9z7bmi0sc45kwrmkczsjm5462jm")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -427,7 +430,7 @@ theorems between the two libraries.") (define-public coq-bignums (package (name "coq-bignums") - (version "8.10.0") + (version "8.11.0") (source (origin (method git-fetch) (uri (git-reference @@ -436,7 +439,7 @@ theorems between the two libraries.") (file-name (git-file-name name version)) (sha256 (base32 - "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5")))) + "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) @@ -460,7 +463,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.") (define-public coq-interval (package (name "coq-interval") - (version "3.4.1") + (version "4.0.0") (source (origin (method git-fetch) @@ -470,7 +473,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.") (file-name (git-file-name name version)) (sha256 (base32 - "03q3dfqi3r3f7aji5s06ig4aav9ajcwswwdzi5lrgr69z0m487k4")))) + "01iz6qmnsm6b9s1vmdjs79vjx9xgwzn5rwyjp6bvs8hg3zlmhpip")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -556,16 +559,16 @@ uses Ltac to synthesize the substitution operation.") (define-public coq-equations (package (name "coq-equations") - (version "1.2.1") + (version "1.2.3") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/mattam82/Coq-Equations") - (commit (string-append "v" version "-8.10-2")))) + (commit (string-append "v" version "-8.11")))) (file-name (git-file-name name version)) (sha256 (base32 - "0j3z4l5nrbyi9zbbyqkc6kassjanwld2188mwmrbqspaypm2ys68")))) + "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) -- 2.28.0 --------------5E05156E34112582443CE76A-- From unknown Sat Jun 14 14:26:25 2025 MIME-Version: 1.0 X-Mailer: MIME-tools 5.505 (Entity 5.505) X-Loop: help-debbugs@gnu.org From: help-debbugs@gnu.org (GNU bug Tracking System) To: Robin Green Subject: bug#43325: closed (Re: [bug#43325] [PATCH] gnu: Update coq and its dependents) Message-ID: References: <20200914022943.5ea8cd91@tachikoma.lepiller.eu> <20200911073027.6485-1-greenrd@greenrd.org> X-Gnu-PR-Message: they-closed 43325 X-Gnu-PR-Package: guix-patches X-Gnu-PR-Keywords: patch Reply-To: 43325@debbugs.gnu.org Date: Mon, 14 Sep 2020 00:31:06 +0000 Content-Type: multipart/mixed; boundary="----------=_1600043466-28098-1" This is a multi-part message in MIME format... ------------=_1600043466-28098-1 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Your bug report #43325: [PATCH] gnu: Update coq and its dependents which was filed against the guix-patches package, has been closed. The explanation is attached below, along with your original report. If you require more details, please reply to 43325@debbugs.gnu.org. --=20 43325: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D43325 GNU Bug Tracking System Contact help-debbugs@gnu.org with problems ------------=_1600043466-28098-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at 43325-done) by debbugs.gnu.org; 14 Sep 2020 00:30:04 +0000 Received: from localhost ([127.0.0.1]:52144 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kHcNf-0006Mx-Jq for submit@debbugs.gnu.org; Sun, 13 Sep 2020 20:30:03 -0400 Received: from lepiller.eu ([89.234.186.109]:58180) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kHcNc-0006L9-IQ for 43325-done@debbugs.gnu.org; Sun, 13 Sep 2020 20:30:01 -0400 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 8cbf5a06; Mon, 14 Sep 2020 00:29:58 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from :to:cc:subject:message-id:in-reply-to:references:mime-version :content-type:content-transfer-encoding; s=dkim; bh=8fv+/rCN7dDV C/Upkinb9848D33bkL1hlhhckpdxpjM=; b=OdSmzUX6zqmzswNhAXPX2/eJ30Jy sycj9kbl/et6LLUkU/I2xBHM+VrUH0LjwQFBD1+KcU3K5lju7Xv9QDdTpX6KvkUk 8Mt+ptAI+BhNGoqMIW9B3mBf7SkFd2wS7DiBSVV/8Er6+BTCqg3WURIypGZdEUa1 VETvwewh5W9R0FLXr19Ag6T14Y9iHnEuaDDSYKKFt5VSOrOY8ByAErWxExN3REEv 2Z32SPxEh6m5WRzOAC3WB6080SlPOCoKGysTGMNN8Bt2pFqVIwTs3yQnOragdQYN aQ5OO5g8r0Ut5upGaaeAVEnnasHbeNezgLuSPfV5vL7y1AgAfuE2V5ED/w== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 20cfe72c (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO); Mon, 14 Sep 2020 00:29:57 +0000 (UTC) Date: Mon, 14 Sep 2020 02:29:43 +0200 From: Julien Lepiller To: Robin Green Subject: Re: [bug#43325] [PATCH] gnu: Update coq and its dependents Message-ID: <20200914022943.5ea8cd91@tachikoma.lepiller.eu> In-Reply-To: <347d318b-8b4c-4207-a080-e0a216a7448a@greenrd.org> References: <20200911073027.6485-1-greenrd@greenrd.org> <347d318b-8b4c-4207-a080-e0a216a7448a@greenrd.org> X-Mailer: Claws Mail 3.17.6 (GTK+ 2.24.32; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 43325-done Cc: 43325-done@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) Le Sun, 13 Sep 2020 15:43:28 +0100, Robin Green a =C3=A9crit : > Updated patch, fixing a test that I mistakenly removed in the > previous version. >=20 >=20 Pushed as 1042d269a723360a02b19a2baafef1e24a3bfc73, thank you! ------------=_1600043466-28098-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at submit) by debbugs.gnu.org; 11 Sep 2020 07:30:53 +0000 Received: from localhost ([127.0.0.1]:42194 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kGdWG-0000dB-Ks for submit@debbugs.gnu.org; Fri, 11 Sep 2020 03:30:53 -0400 Received: from lists.gnu.org ([209.51.188.17]:38742) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kGdWE-0000d2-8Z for submit@debbugs.gnu.org; Fri, 11 Sep 2020 03:30:50 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:47708) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1kGdWB-0007Xk-2a for guix-patches@gnu.org; Fri, 11 Sep 2020 03:30:50 -0400 Received: from [67.214.171.71] (port=51918 helo=mail.dnsexit.com) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1kGdW9-00024G-6s for guix-patches@gnu.org; Fri, 11 Sep 2020 03:30:46 -0400 Received: from localhost (localhost.localdomain [127.0.0.1]) by mail.dnsexit.com (Postfix) with ESMTP id 3B4EA3C0816 for ; Fri, 11 Sep 2020 03:30:42 -0400 (EDT) X-Virus-Scanned: amavisd-new at dnsexit.com Received: from mail.dnsexit.com ([127.0.0.1]) by localhost (box2.dnsexit.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id H0tVMJ9javdj; Fri, 11 Sep 2020 03:30:42 -0400 (EDT) Received: from localhost.localdomain (greenrd.plus.com [212.159.116.150]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by mail.dnsexit.com (Postfix) with ESMTPSA id 999453C083B; Fri, 11 Sep 2020 03:30:40 -0400 (EDT) From: Robin Green To: guix-patches@gnu.org Subject: [PATCH] gnu: Update coq and its dependents Date: Fri, 11 Sep 2020 08:30:27 +0100 Message-Id: <20200911073027.6485-1-greenrd@greenrd.org> X-Mailer: git-send-email 2.28.0 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Host-Lookup-Failed: Reverse DNS lookup failed for 67.214.171.71 (failed) Received-SPF: pass client-ip=67.214.171.71; envelope-from=greenrd@greenrd.org; helo=mail.dnsexit.com X-detected-operating-system: by eggs.gnu.org: First seen = 2020/09/11 03:30:43 X-ACL-Warn: Detected OS = Linux 3.1-3.10 [fuzzy] X-Spam_score_int: -10 X-Spam_score: -1.1 X-Spam_bar: - X-Spam_report: (-1.1 / 5.0 requ) BAYES_00=-1.9, RDNS_NONE=0.793, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=no autolearn_force=no X-Spam_action: no action X-Spam-Score: -1.3 (-) X-Debbugs-Envelope-To: submit Cc: Robin Green X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -2.3 (--) * gnu/packages/coq.scm (coq): Update to 8.11.2 (coq-flocq): Update to 3.3.1 (coq-gappa): Update to 1.4.4 (coq-mathcomp): Update to 1.11.0 (coq-coquelicot): Update to 3.1.0 (coq-bignums): Update to 8.11.0 (coq-interval): Update to 4.0.0 (coq-equations): Update to 1.2.3 --- gnu/packages/coq.scm | 45 +++++++++++++++++++++++--------------------- 1 file changed, 24 insertions(+), 21 deletions(-) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 3573518763..2d8dca8d46 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -34,6 +34,7 @@ #:use-module (gnu packages ocaml) #:use-module (gnu packages perl) #:use-module (gnu packages python) + #:use-module (gnu packages rsync) #:use-module (gnu packages texinfo) #:use-module (guix build-system gnu) #:use-module (guix build-system ocaml) @@ -47,7 +48,7 @@ (define-public coq (package (name "coq") - (version "8.10.2") + (version "8.11.2") (source (origin (method git-fetch) @@ -57,7 +58,7 @@ (file-name (git-file-name name version)) (sha256 (base32 - "0ji2rzd70b3hcwfw97qk7rv3m2977ylqnq82l1555dp3njr8nm3q")))) + "1gia82dkmzqspw2w3s4gjyh39ghbmw4i41i4hyzc91g7mza17nbz")))) (native-search-paths (list (search-path-specification (variable "COQPATH") @@ -70,7 +71,8 @@ ("camlp5" ,camlp5) ("ocaml-num" ,ocaml-num))) (native-inputs - `(("ocaml-ounit" ,ocaml-ounit))) + `(("ocaml-ounit" ,ocaml-ounit) + ("rsync" ,rsync))) (arguments `(#:phases (modify-phases %standard-phases @@ -121,11 +123,12 @@ (add-after 'install 'check (lambda _ (with-directory-excursion "test-suite" - ;; These two tests fail. + ;; These three tests fail. ;; Fails because the output is not formatted as expected. (delete-file-recursively "coq-makefile/timing") - ;; Fails because we didn't build coqtop.byte. - (delete-file-recursively "coq-makefile/findlib-package") + ;; Fail because we didn't build coqtop.byte. + (delete-file-recursively "coq-makefile/findlib-package-unpacked") + (delete-file "misc/printers.sh") (invoke "make"))))))) (home-page "https://coq.inria.fr") (synopsis "Proof assistant for higher-order logic") @@ -215,7 +218,7 @@ provers.") (define-public coq-flocq (package (name "coq-flocq") - (version "3.2.0") + (version "3.3.1") (source (origin (method git-fetch) @@ -225,7 +228,7 @@ provers.") (file-name (git-file-name name version)) (sha256 (base32 - "15bi36x7zj0glsb3s2gwqd4wswhfzh36rbp7imbyff53a7nna95l")))) + "01gdykva0lcw6y3dm8j0djxayb87szfg9vn0mxd6z3pks644misl")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -272,7 +275,7 @@ inside Coq.") (define-public coq-gappa (package (name "coq-gappa") - (version "1.4.2") + (version "1.4.4") (source (origin (method git-fetch) @@ -282,7 +285,7 @@ inside Coq.") (file-name (git-file-name name version)) (sha256 (base32 - "0r7jwp5xssdfzivs2flp7mzrscqhgl63mryhhf1cvndpgzqwfk2f")))) + "0f3g3wjkvfkm961l4jpckhsqd43jnvm7f5qqk78qc32zh1fg339n")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -332,7 +335,7 @@ assistant.") (define-public coq-mathcomp (package (name "coq-mathcomp") - (version "1.10.0") + (version "1.11.0") (source (origin (method git-fetch) @@ -341,7 +344,7 @@ assistant.") (commit (string-append "mathcomp-" version)))) (file-name (git-file-name name version)) (sha256 - (base32 "1h5h1c2025r1ms5qryvwy6pikxmpmmjav6yl127xpzmqdi6w732d")))) + (base32 "1axywpa1jcpnidd86irpd1gdbbg2sfbwc652675xisq5wnmfmf6f")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) @@ -374,7 +377,7 @@ part of the distribution.") (define-public coq-coquelicot (package (name "coq-coquelicot") - (version "3.0.3") + (version "3.1.0") (source (origin (method git-fetch) @@ -384,7 +387,7 @@ part of the distribution.") (file-name (git-file-name name version)) (sha256 (base32 - "0m5wbr2s8lnf8b7cfwv15hyzsmbcaz6hgdn7aazcrkxnwr87vgkp")))) + "0mz3pxan1237fr5fi79c66y7b9z7bmi0sc45kwrmkczsjm5462jm")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -427,7 +430,7 @@ theorems between the two libraries.") (define-public coq-bignums (package (name "coq-bignums") - (version "8.10.0") + (version "8.11.0") (source (origin (method git-fetch) (uri (git-reference @@ -436,7 +439,7 @@ theorems between the two libraries.") (file-name (git-file-name name version)) (sha256 (base32 - "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5")))) + "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) @@ -460,7 +463,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.") (define-public coq-interval (package (name "coq-interval") - (version "3.4.1") + (version "4.0.0") (source (origin (method git-fetch) @@ -470,7 +473,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.") (file-name (git-file-name name version)) (sha256 (base32 - "03q3dfqi3r3f7aji5s06ig4aav9ajcwswwdzi5lrgr69z0m487k4")))) + "01iz6qmnsm6b9s1vmdjs79vjx9xgwzn5rwyjp6bvs8hg3zlmhpip")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -556,16 +559,16 @@ uses Ltac to synthesize the substitution operation.") (define-public coq-equations (package (name "coq-equations") - (version "1.2.1") + (version "1.2.3") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/mattam82/Coq-Equations") - (commit (string-append "v" version "-8.10-2")))) + (commit (string-append "v" version "-8.11")))) (file-name (git-file-name name version)) (sha256 (base32 - "0j3z4l5nrbyi9zbbyqkc6kassjanwld2188mwmrbqspaypm2ys68")))) + "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) -- 2.28.0 ------------=_1600043466-28098-1--