From unknown Thu Jun 19 14:04:47 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#42238 <42238@debbugs.gnu.org> To: bug#42238 <42238@debbugs.gnu.org> Subject: Status: gnu: metamath: Update to 0.183. Reply-To: bug#42238 <42238@debbugs.gnu.org> Date: Thu, 19 Jun 2025 21:04:47 +0000 retitle 42238 gnu: metamath: Update to 0.183. reassign 42238 guix-patches submitter 42238 elaexuotee@wilsonb.com severity 42238 normal thanks From debbugs-submit-bounces@debbugs.gnu.org Tue Jul 07 00:56:58 2020 Received: (at submit) by debbugs.gnu.org; 7 Jul 2020 04:56:58 +0000 Received: from localhost ([127.0.0.1]:35322 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jsff3-0004XD-FD for submit@debbugs.gnu.org; Tue, 07 Jul 2020 00:56:58 -0400 Received: from lists.gnu.org ([209.51.188.17]:51698) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jsff0-0004X5-QZ for submit@debbugs.gnu.org; Tue, 07 Jul 2020 00:56:52 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:51234) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1jsff0-0002cO-HD for guix-patches@gnu.org; Tue, 07 Jul 2020 00:56:50 -0400 Received: from m42-5.mailgun.net ([69.72.42.5]:44869) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1jsfey-00011P-6A for guix-patches@gnu.org; Tue, 07 Jul 2020 00:56:50 -0400 DKIM-Signature: a=rsa-sha256; v=1; c=relaxed/relaxed; d=mg.wilsonb.com; q=dns/txt; s=krs; t=1594097806; h=Content-Type: MIME-Version: Message-Id: Subject: From: To: Date: Sender; bh=0oUzFdp8+huszmKGDlnNKR4ZchPQiis1j7cjpUOkZgI=; b=ps8urMSJZs0M5SNglFQTE48jcG1HtHOeg/UPsXPam+BGIEA70udS9v8Gclw1UO1MFMrlEBlS vgOI2Sv2tNQSStg35JpTO8z1j2h5oIC1WVEhD5M5eTZEN9n4xUwJRpOzZhS4r/5z9aIEUimP zgryWSqxVuNm70mPx7OHcR96kYnkQO9F0NWVzrOtxDtkWoi+6r1ibl6gf/FkS28xf0ceHz/d VBKFVyCE7i+B2a/pATnbNMnCrEuALLGQFrIt0ABCySy8vX94FQoACKAEOkBFELL1feaGKqqv J8X9NREJKsZ/14mVwQvhDnph1U9ACdbt2bxpJvHAv4ZkO+HSBKd32A== X-Mailgun-Sending-Ip: 69.72.42.5 X-Mailgun-Sid: WyI5MmEzMyIsICJndWl4LXBhdGNoZXNAZ251Lm9yZyIsICIwODU0N2EiXQ== Received: from wilsonb.com (wilsonb.com [104.199.203.42]) by smtp-out-n01.prod.us-east-1.postgun.com with SMTP id 5f04008dbca1ed3155a7c4ec (version=TLS1.3, cipher=TLS_AES_128_GCM_SHA256); Tue, 07 Jul 2020 04:56:45 GMT Received: from localhost (KD111239204107.au-net.ne.jp [111.239.204.107]) by wilsonb.com (Postfix) with ESMTPSA id 050F3A2C46 for ; Tue, 7 Jul 2020 04:56:41 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wilsonb.com; s=201703; t=1594097802; bh=0oUzFdp8+huszmKGDlnNKR4ZchPQiis1j7cjpUOkZgI=; h=Date:To:From:Subject:From; b=Cq4orkPynpAbW5fZgcnSOyaV8U93OSs4rXTFk123SA1sU4kKXfp8uOLapJY9AN7QN 7D1wb/aGBj0pegiyF1YhJ3aK3+nC1MJq2ugxd1fuxQD4RWTNH2HSWyblV70IqdwQiY Azl+f3iwMYtWJDGtYHWjWqIbkHulZ6nF45A6c/ZlOUQd5QErHcaaQYmGrBGCi3g+or HYmDZQvW5gZrFysdCrXlULOYCvVFmSI7/cnbIIpEsEb8gK8Mz2+EHN0LpEg+LaEGEm 61IWM/G/6p7UEfEbLo81d1gsB+kyaRr6eZ/p2nrWVNjqgYKw6LXle0uNFI3CLnCPOg DOX8/baoGLDw8C/tWagJx50s5dJQ28TSqaPrVq3lgm87E55M0H791nq6hvGzTrIUQ3 vRhaGCvVFrRjq40efyNfKD/qhl0hFYu+aC6Y6GWEFk5Yz2jvRUxzvrSBEOs/mNniUF Y3b2Aly1caiy7SqMMTuO25TVvbBp5oz+xR2sO85hWtwyG83f+klKtHMMOkNaFFw1OP L5GlPpAdQ6jRna380KiBHpBSqL6pTjGhUqo9/NMIwesiALFFugPstZN7TFlQ41SGhv RgWdYAXXKNc7Ud0ewnpWarFtPinR203TSUHmLg+f9Godm6qkjNe+En7YrXIIKciIlS nGBG2grd85vEKB3hN5KW9r48= Date: Tue, 07 Jul 2020 13:56:38 +0900 To: guix-patches@gnu.org From: elaexuotee@wilsonb.com Subject: gnu: metamath: Update to 0.183. Message-Id: <3AF495BDV48J8.3UR1ZZRM1QMF8@wilsonb.com> User-Agent: mblaze/0.7 MIME-Version: 1.0 Content-Type: multipart/signed; micalg="pgp-sha1"; protocol="application/pgp-signature"; boundary="----_=_649e61c2028577580a347666_=_" Received-SPF: pass client-ip=69.72.42.5; envelope-from=bounce+686de0.08547a-guix-patches=gnu.org@mg.wilsonb.com; helo=m42-5.mailgun.net X-detected-operating-system: by eggs.gnu.org: First seen = 2020/07/07 00:56:45 X-ACL-Warn: Detected OS = Linux 2.2.x-3.x [generic] [fuzzy] X-Spam_score_int: -30 X-Spam_score: -3.1 X-Spam_bar: --- X-Spam_report: (-3.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, RCVD_IN_DNSWL_NONE=-0.0001, RCVD_IN_MSPIKE_H2=-1, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, URIBL_BLOCKED=0.001 autolearn=_AUTOLEARN X-Spam_action: no action X-Spam-Score: -1.3 (-) X-Debbugs-Envelope-To: submit 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 (--) This is a multipart message in MIME format. ------_=_649e61c2028577580a347666_=_ MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----_=_27939d0d4e256cef2b478ff9_=_" This is a multipart message in MIME format. ------_=_27939d0d4e256cef2b478ff9_=_ Content-Type: text/plain; charset=UTF-8 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Upstream updated to 0.183 about a week ago. ------_=_27939d0d4e256cef2b478ff9_=_ Content-Disposition: attachment; filename*0*=UTF-8''0001-gnu-metamath-Update-to-0.183.patch Content-Type: text/x-patch Content-Transfer-Encoding: quoted-printable =46rom 5e7232c2a90ad302c0177bf008b6dd61b59f542e Mon Sep 17 00:00:00 2001 =46rom: "B. Wilson" =44ate: Tue, 7 Jul 2020 13:52:30 +0900 =53ubject: [PATCH] gnu: metamath: Update to 0.183. =54o: guix-patches@gnu.org =0A* gnu/packages/maths.scm (metamath): Update to 0.183. =2D-- =20gnu/packages/maths.scm | 48 ++++++++++++++++++------------------------ =201 file changed, 21 insertions(+), 27 deletions(-) =0Adiff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm =69ndex 5ea505764a..dbc670178a 100644 =2D-- a/gnu/packages/maths.scm =2B++ b/gnu/packages/maths.scm =40@ -2411,32 +2411,26 @@ bindings to almost all functions of SLEPc.") =20 (license license:bsd-3))) =20= =20(define-public metamath =2D ;; Upstream pushed a commit on top of v0.182 that fixes a bug in Makef= =69le.am. =2D ;; Using this commit lets us avoid directly including the patch here. = =20In the =2D ;; next version bump, we should be able to replace this and directly u= =73e the =2D ;; version tag. =2D (let ((commit "5df616efe4119ff88daf77e7041d45b6fa39c578") =2D (revision "0")) =2D (package =2D (name "metamath") =2D (version (git-version "0.182" revision commit)) =2D (source =2D (origin =2D (method git-fetch) =2D (uri (git-reference =2D (url "https://github.com/metamath/metamath-exe.git") =2D (commit commit))) =2D (file-name (git-file-name name version)) =2D (sha256 =2D (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"= =29))) =2D (build-system gnu-build-system) =2D (native-inputs =2D `(("autoconf" ,autoconf) =2D ("automake" ,automake))) =2D (home-page "http://us.metamath.org/") =2D (synopsis "Proof verifier based on a minimalistic formalism") =2D (description =2D "Metamath is a tiny formal language and that can express theorems= =20in =2B (package =2B (name "metamath") =2B (version "0.183") =2B (source =2B (origin =2B (method git-fetch) =2B (uri (git-reference =2B (url "https://github.com/metamath/metamath-exe.git") =2B (commit (string-append "v" version)))) =2B (file-name (git-file-name name version)) =2B (sha256 =2B (base32 "1jjf4fy6j53i40dh0yv0f9sngnw4gs24cig99vsg3q0303pwrhg7"))= =29) =2B (build-system gnu-build-system) =2B (native-inputs =2B `(("autoconf" ,autoconf) =2B ("automake" ,automake))) =2B (home-page "http://us.metamath.org/") =2B (synopsis "Proof verifier based on a minimalistic formalism") =2B (description =2B "Metamath is a tiny formal language and that can express theorems i= =6E =20abstract mathematics, with an accompyaning @command{metamath} executable= =20that =20verifies databases of these proofs. There is a public database, =20@url{https://github.com/metamath/set.mm, set.mm}, implementing first-ord= =65r =40@ -2444,7 +2438,7 @@ logic and Zermelo-Frenkel set theory with Choice, a= =6Cong with a large swath of =20associated, high-level theorems, e.g.@: the fundamental theorem of arith= =6Detic, =20the Cauchy-Schwarz inequality, Stirling's formula, etc. See the Metamat= =68 =20book.") =2D (license license:gpl2+)))) =2B (license license:gpl2+))) =20= =20(define-public mumps =20 (package =2D-=20 =32.27.0 =0A= ------_=_27939d0d4e256cef2b478ff9_=_-- ------_=_649e61c2028577580a347666_=_ Content-Disposition: attachment; filename=signature.asc Content-Type: application/pgp-signature Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- iI0EABYIADUWIQQ7FdZn/PDWvxE6cmR2pStZ7i7CgQUCXwQAghccZWxhZXh1b3Rl ZUB3aWxzb25iLmNvbQAKCRB2pStZ7i7CgXYnAP0UZsXpF/V6eRBb5HGSg9hfK9Hv TZKcHWtkqx0UW2pNwQD/UIJj7pl2WY/jBr7AIok0+W2DWvMuq6pIGPvlVcJPmwY= =Bpxp -----END PGP SIGNATURE----- ------_=_649e61c2028577580a347666_=_-- From debbugs-submit-bounces@debbugs.gnu.org Tue Jul 07 08:04:26 2020 Received: (at submit) by debbugs.gnu.org; 7 Jul 2020 12:04:26 +0000 Received: from localhost ([127.0.0.1]:35631 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jsmKo-00033m-9T for submit@debbugs.gnu.org; Tue, 07 Jul 2020 08:04:26 -0400 Received: from lists.gnu.org ([209.51.188.17]:48952) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jsmKl-00033X-L0 for submit@debbugs.gnu.org; Tue, 07 Jul 2020 08:04:24 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:54326) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1jsmKl-0001l8-9F for guix-patches@gnu.org; Tue, 07 Jul 2020 08:04:23 -0400 Received: from relay9-d.mail.gandi.net ([217.70.183.199]:50577) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1jsmKi-0004WJ-4H for guix-patches@gnu.org; Tue, 07 Jul 2020 08:04:23 -0400 X-Originating-IP: 185.131.40.67 Received: from localhost (40-67.ipv4.commingeshautdebit.fr [185.131.40.67]) (Authenticated sender: admin@nicolasgoaziou.fr) by relay9-d.mail.gandi.net (Postfix) with ESMTPSA id 964C8FF809; Tue, 7 Jul 2020 12:04:15 +0000 (UTC) From: Nicolas Goaziou To: elaexuotee--- via Guix-patches via Subject: Re: [bug#42238] gnu: metamath: Update to 0.183. References: <3AF495BDV48J8.3UR1ZZRM1QMF8@wilsonb.com> Date: Tue, 07 Jul 2020 14:04:14 +0200 In-Reply-To: <3AF495BDV48J8.3UR1ZZRM1QMF8@wilsonb.com> (elaexuotee's message of "Tue, 07 Jul 2020 13:56:38 +0900") Message-ID: <8736638rb5.fsf@nicolasgoaziou.fr> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain Received-SPF: pass client-ip=217.70.183.199; envelope-from=mail@nicolasgoaziou.fr; helo=relay9-d.mail.gandi.net X-detected-operating-system: by eggs.gnu.org: First seen = 2020/07/07 08:04:16 X-ACL-Warn: Detected OS = Linux 3.11 and newer X-Spam_score_int: -35 X-Spam_score: -3.6 X-Spam_bar: --- X-Spam_report: (-3.6 / 5.0 requ) BAYES_00=-1.9, RCVD_IN_DNSWL_LOW=-0.7, RCVD_IN_MSPIKE_H2=-1, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=_AUTOLEARN X-Spam_action: no action X-Spam-Score: -1.6 (-) X-Debbugs-Envelope-To: submit Cc: elaexuotee@wilsonb.com, 42238@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: -2.6 (--) Hello, elaexuotee--- via Guix-patches via writes: > * gnu/packages/maths.scm (metamath): Update to 0.183. Applied. Thank you. Regards, -- Nicolas Goaziou From debbugs-submit-bounces@debbugs.gnu.org Tue Jul 07 08:04:46 2020 Received: (at 42238-done) by debbugs.gnu.org; 7 Jul 2020 12:04:46 +0000 Received: from localhost ([127.0.0.1]:35634 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jsmL8-00034L-Lt for submit@debbugs.gnu.org; Tue, 07 Jul 2020 08:04:46 -0400 Received: from relay3-d.mail.gandi.net ([217.70.183.195]:42569) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jsmL6-000345-DZ for 42238-done@debbugs.gnu.org; Tue, 07 Jul 2020 08:04:45 -0400 X-Originating-IP: 185.131.40.67 Received: from localhost (40-67.ipv4.commingeshautdebit.fr [185.131.40.67]) (Authenticated sender: admin@nicolasgoaziou.fr) by relay3-d.mail.gandi.net (Postfix) with ESMTPSA id E6FBB60009 for <42238-done@debbugs.gnu.org>; Tue, 7 Jul 2020 12:04:37 +0000 (UTC) From: Nicolas Goaziou To: 42238-done@debbugs.gnu.org Subject: Re: [bug#42238] gnu: metamath: Update to 0.183. References: <3AF495BDV48J8.3UR1ZZRM1QMF8@wilsonb.com> Date: Tue, 07 Jul 2020 14:04:36 +0200 In-Reply-To: <3AF495BDV48J8.3UR1ZZRM1QMF8@wilsonb.com> (elaexuotee's message of "Tue, 07 Jul 2020 13:56:38 +0900") Message-ID: <87y2nv7cq3.fsf@nicolasgoaziou.fr> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: -0.7 (/) X-Debbugs-Envelope-To: 42238-done 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.7 (-) Applied. Closing. From unknown Thu Jun 19 14:04:47 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Wed, 05 Aug 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