From unknown Tue Jun 17 23:59:22 2025 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.509 (Entity 5.509) Content-Type: text/plain; charset=utf-8 From: bug#43325 <43325@debbugs.gnu.org> To: bug#43325 <43325@debbugs.gnu.org> Subject: Status: [PATCH] gnu: Update coq and its dependents Reply-To: bug#43325 <43325@debbugs.gnu.org> Date: Wed, 18 Jun 2025 06:59:22 +0000 retitle 43325 [PATCH] gnu: Update coq and its dependents reassign 43325 guix-patches submitter 43325 Robin Green severity 43325 normal tag 43325 patch thanks From debbugs-submit-bounces@debbugs.gnu.org Fri Sep 11 03:30:53 2020 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 From debbugs-submit-bounces@debbugs.gnu.org Sun Sep 13 10:43:37 2020 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) To: 43325@debbugs.gnu.org From: Robin Green Subject: Re: [PATCH] gnu: Update coq and its dependents 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-Debbugs-Envelope-To: 43325 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 debbugs-submit-bounces@debbugs.gnu.org Sun Sep 13 20:30:04 2020 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! From unknown Tue Jun 17 23:59:22 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Mon, 12 Oct 2020 11:24:05 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator