From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp0 ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms11 with LMTPS id 4Ja3K6gABF86KAAA0tVLHw (envelope-from ) for ; Tue, 07 Jul 2020 04:57:12 +0000 Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp0 with LMTPS id YMaTJ6gABF8DewAA1q6Kng (envelope-from ) for ; Tue, 07 Jul 2020 04:57:12 +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 3018C9408E6 for ; Tue, 7 Jul 2020 04:57:10 +0000 (UTC) Received: from localhost ([::1]:53008 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1jsffI-00034e-Ls for larch@yhetil.org; Tue, 07 Jul 2020 00:57:08 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:51240) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1jsffC-00030h-Aj for guix-patches@gnu.org; Tue, 07 Jul 2020 00:57:02 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:52009) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1jsffC-000120-1M for guix-patches@gnu.org; Tue, 07 Jul 2020 00:57:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1jsffB-0004Xc-Vv for guix-patches@gnu.org; Tue, 07 Jul 2020 00:57:01 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#42238] gnu: metamath: Update to 0.183. Resent-From: elaexuotee@wilsonb.com Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Tue, 07 Jul 2020 04:57:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 42238 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: To: 42238@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.159409781817444 (code B ref -1); Tue, 07 Jul 2020 04:57:01 +0000 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 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-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-Spam-Score: -2.3 (--) 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" Reply-to: elaexuotee@wilsonb.com, elaexuotee--- via Guix-patches From: elaexuotee--- via Guix-patches via X-Scanner: scn0 Authentication-Results: aspmx1.migadu.com; dkim=fail (rsa verify failed) header.d=mg.wilsonb.com header.s=krs header.b=ps8urMSJ; dkim=fail (rsa verify failed) header.d=wilsonb.com header.s=201703 header.b=Cq4orkPy; dmarc=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-Spam-Score: -2.11 X-TUID: 2avBPqCyxWMK 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_=_--