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 WPgAJz1cuV64JQAA0tVLHw (envelope-from ) for ; Mon, 11 May 2020 14:07:57 +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 GH+eJEtcuV42QAAA1q6Kng (envelope-from ) for ; Mon, 11 May 2020 14:08:11 +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 1D19D940712 for ; Mon, 11 May 2020 14:08:09 +0000 (UTC) Received: from localhost ([::1]:39396 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1jY96H-0003vw-Jh for larch@yhetil.org; Mon, 11 May 2020 10:08:09 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:55104) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1jY96B-0003tk-Lq for guix-patches@gnu.org; Mon, 11 May 2020 10:08:03 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:41345) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1jY969-0002jU-RS for guix-patches@gnu.org; Mon, 11 May 2020 10:08:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1jY969-00047M-MS for guix-patches@gnu.org; Mon, 11 May 2020 10:08:01 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#40815] gnu: Add metamath Resent-From: "B. Wilson" Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 11 May 2020 14:08:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 40815 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: To: 40815@debbugs.gnu.org Cc: Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.158920605015757 (code B ref -1); Mon, 11 May 2020 14:08:01 +0000 Received: (at submit) by debbugs.gnu.org; 11 May 2020 14:07:30 +0000 Received: from localhost ([127.0.0.1]:52891 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jY95a-000461-UQ for submit@debbugs.gnu.org; Mon, 11 May 2020 10:07:30 -0400 Received: from lists.gnu.org ([209.51.188.17]:44138) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jY95Q-00045a-Mj for submit@debbugs.gnu.org; Mon, 11 May 2020 10:07:26 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:54962) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1jY95Q-0002yM-H9 for guix-patches@gnu.org; Mon, 11 May 2020 10:07:16 -0400 Received: from m42-5.mailgun.net ([69.72.42.5]:47538) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1jY958-0002Pz-MV for guix-patches@gnu.org; Mon, 11 May 2020 10:07:16 -0400 DKIM-Signature: a=rsa-sha256; v=1; c=relaxed/relaxed; d=mg.wilsonb.com; q=dns/txt; s=krs; t=1589206034; h=Content-Type: MIME-Version: Message-Id: In-Reply-To: References: From: Subject: Cc: To: Date: Sender; bh=b8A0YMDlP5an8n7MXbIeMQdhk0NKM2YTV4d3kMhdkvk=; b=Y4iv6RyOPinwj7xI/GM4kyFm4QWpwEahK4+qjNEta7jty7KieKA6g9q6W4hQBMaoDf6y6BH9 Wk1IsSIUtP7qfQOeLUDJ/c77B1lpgW8j2DqM63tuY6N0Qx73/M/ohZHmlHNKDDRA5M95ecU6 J1XOIRH5RQZonJwLBnFHxJUqvkcdSNmJMWL0gWcQUgATIhJ3ev+bNefJ/a8Y0wsoiotr4cWp 0gAwg8MRAf2FhwcE/7vPdZwcdQCjG/NwCOWpx2ruIURsPx8HTi2/qPjwzi9HygFT1i5tgugQ DD6X5AsRfOGJ7UAOc9COJ66iCkWWLgbGtPHdYlmqJR7KODKXj2aNSA== X-Mailgun-Sending-Ip: 69.72.42.5 X-Mailgun-Sid: WyI5MmEzMyIsICJndWl4LXBhdGNoZXNAZ251Lm9yZyIsICIwODU0N2EiXQ== Received: from wilsonb.com (wilsonb.com [104.199.203.42]) by mxa.mailgun.org with ESMTP id 5eb95bc8.7fd1c9000f60-smtp-out-n05; Mon, 11 May 2020 14:06:00 -0000 (UTC) Received: from localhost (KD111239199242.au-net.ne.jp [111.239.199.242]) by wilsonb.com (Postfix) with ESMTPSA id 55FAAA00C8; Mon, 11 May 2020 14:05:57 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wilsonb.com; s=201703; t=1589205957; bh=b8A0YMDlP5an8n7MXbIeMQdhk0NKM2YTV4d3kMhdkvk=; h=Date:To:Cc:Subject:From:References:In-Reply-To:From; b=G8yUP+Ks9UiczJpcENjKokLO2+ZBbo1/JfJax7LUvMvNiyzwHiuYxGan1Dk8Vw3jg vYuvkBhU8t9REmvC4JU4z1WtoXvpezh8F4RCWU/vhvq0NfbyQBan2MTI7+ibNdjSN/ psim5a+SrLKdOs2l1lzUhkG0wd1z3qNntUB69CE3Kh/O081TPeJ9WUgFBcMpMjjis0 jQXSjeiqlI3+k+z6pQpMhZ8BLiEsjK4QBrmJSCFd3mSZ/ADzQPr3hTqaHrNDltWuQq 2lzNEb4rkI5CQy/PNNUpS8t4W3+AipNig0tcjTN/HYtmbdD70TZIRXhNtbztCqWkFg YlZSRoxE0bakZTyowqMpT0buX6qx1mGlB8UUdEJqJtDjTpm2AhZGxgAnvSD1W/agko 3MWpQNjt2vk+g/ZPBDH5mCtygw3TuDHfDu7GdEEwLEIUAGeda1qlL9ya/2k0qQUliy WDis9WbetcRZcyIw8McWp8sKWr8Cq+IcPzWuHhR5RYAZkGc9B++MziX6pz3X7gyZNM s4BKFOr9h8Al7H1TIuWaRtYzVnHsgUOdUNXz2Fbyaz/khKcS27aT6ksdQdsiRFSAUj LcxnJs4p3eCRIEheC4JnLsaN9hde8U3seT4Ovnh+S7zx8SWl64O+YD2pncxpSB1QLE bGn6NKWTSR9IhWC/imjusDY4= Date: Mon, 11 May 2020 23:05:48 +0900 References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> <20200426172945.7ez6i2fl3pjcoexd@gravity> <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com> <20200427121248.cga7p43flnusf7zo@gravity> <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com> In-Reply-To: <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com> Message-Id: <25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com> User-Agent: mblaze/0.5.1 MIME-Version: 1.0 Content-Type: multipart/signed; micalg="pgp-sha1"; protocol="application/pgp-signature"; boundary="----_=_273a89163ec2adca5de5ddad_=_" 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/05/11 10:06:57 X-ACL-Warn: Detected OS = Linux 2.2.x-3.x [generic] X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.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_H3=0.001, RCVD_IN_MSPIKE_WL=0.001, SPF_PASS=-0.001, URIBL_BLOCKED=0.001 autolearn=_AUTOLEARN X-Spam_action: no action X-Spam-Score: 2.8 (++) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-Spam-Score: -0.5 (/) 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: "B. Wilson" , "B. Wilson via Guix-patches" From: "B. Wilson via Guix-patches" via X-Scanner: scn0 X-Spam-Score: -2.11 Authentication-Results: aspmx1.migadu.com; dkim=fail (rsa verify failed) header.d=mg.wilsonb.com header.s=krs header.b=Y4iv6RyO; dkim=fail (rsa verify failed) header.d=wilsonb.com header.s=201703 header.b=G8yUP+Ks; 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-Scan-Result: default: False [-2.11 / 13.00]; HAS_REPLYTO(0.00)[elaexuotee@wilsonb.com]; RCVD_VIA_SMTP_AUTH(0.00)[]; GENERIC_REPUTATION(0.00)[-0.54013025548374]; TO_DN_SOME(0.00)[]; R_SPF_ALLOW(-0.20)[+ip4:209.51.188.0/24:c]; IP_REPUTATION_HAM(0.00)[asn: 22989(0.07), country: US(-0.00), ip: 209.51.188.17(-0.54)]; HAS_ATTACHMENT(0.00)[]; R_DKIM_REJECT(1.00)[mg.wilsonb.com:s=krs,wilsonb.com:s=201703]; DWL_DNSWL_FAIL(0.00)[209.51.188.17:server fail]; MX_GOOD(-0.50)[cached: eggs.gnu.org]; RCPT_COUNT_TWO(0.00)[2]; DKIM_TRACE(0.00)[mg.wilsonb.com:-,wilsonb.com:-]; MAILLIST(-0.20)[mailman]; SIGNED_PGP(-2.00)[]; FORGED_RECIPIENTS_MAILLIST(0.00)[]; RCVD_IN_DNSWL_FAIL(0.00)[209.51.188.17:server fail]; MIME_TRACE(0.00)[0:+,1:+,2:+,3:+,4:~]; RCVD_TLS_LAST(0.00)[]; ASN(0.00)[asn:22989, ipnet:209.51.188.0/24, country:US]; TAGGED_FROM(0.00)[larch=yhetil.org]; FROM_NEQ_ENVFROM(0.00)[guix-patches@gnu.org,guix-patches-bounces@gnu.org]; ARC_NA(0.00)[]; RECEIVED_SPAMHAUS_PBL(0.00)[111.239.199.242:received]; FROM_HAS_DN(0.00)[]; URIBL_BLOCKED(0.00)[vkten.in:email,set.mm:url,wilsonb.com:email,metamath.org:url,nixo.xyz:email,gnu.org:email]; MIME_GOOD(-0.20)[multipart/signed,multipart/mixed,text/plain,text/x-patch]; REPLYTO_DOM_NEQ_FROM_DOM(0.00)[]; DMARC_NA(0.00)[gnu.org]; HAS_LIST_UNSUB(-0.01)[]; RWL_MAILSPIKE_POSSIBLE(0.00)[209.51.188.17:from]; RCVD_COUNT_SEVEN(0.00)[11]; FORGED_SENDER_MAILLIST(0.00)[] X-TUID: mBsNFfSOMTQ1 This is a multipart message in MIME format. ------_=_273a89163ec2adca5de5ddad_=_ MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----_=_0956a90551bf04152c547a44_=_" This is a multipart message in MIME format. ------_=_0956a90551bf04152c547a44_=_ Content-Type: text/plain; charset=UTF-8 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Updated patch for metamath, containing two fixes: * Rename source repo checkout to match package name (fixes lint warning), a= nd * Consolidate pdf under share/doc/- with LICENSE.TXT. ------_=_0956a90551bf04152c547a44_=_ Content-Disposition: attachment; filename=0001-gnu-Add-metamath.patch Content-Type: text/x-patch Content-Transfer-Encoding: quoted-printable =46rom f7c803351c483ff0efe0e65604fec3de001f7282 Mon Sep 17 00:00:00 2001 =46rom: "B. Wilson" =44ate: Mon, 11 May 2020 20:10:48 +0900 =53ubject: [PATCH] gnu: Add metamath. =54o: guix-patches@gnu.org =0A* gnu/packages/maths.scm (metamath): New variable. =2D-- =20gnu/packages/maths.scm | 75 ++++++++++++++++++++++++++++++++++++++++++ =201 file changed, 75 insertions(+) =0Adiff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm =69ndex 8fbce15418..5dc600ccb5 100644 =2D-- a/gnu/packages/maths.scm =2B++ b/gnu/packages/maths.scm =40@ -38,6 +38,7 @@ =20;;; Copyright =C2=A9 2020 R Veera Kumar =20;;; Copyright =C2=A9 2020 Vincent Legoll =20;;; Copyright =C2=A9 2020 Nicol=C3=B2 Balzarotti =2B;;; Copyright =C2=A9 2020 B. Wilson =20;;; =20;;; This file is part of GNU Guix. =20;;; =40@ -5615,3 +5616,77 @@ and conversions, physical constants, symbolic calc= =75lations (including =20integrals and equations), arbitrary precision, uncertainity propagation,= =0A interval arithmetic, plotting.") =20 (license license:gpl2+))) =2B =2B(define-public metamath =2B (package =2B (name "metamath") =2B (version "0.182") =2B (source =2B (origin =2B (method git-fetch) =2B (uri (git-reference =2B (url "https://github.com/metamath/metamath-exe.git") =2B (commit "5df616efe4119ff88daf77e7041d45b6fa39c578"))) =2B (sha256 =2B (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"))= =0A+ (file-name (string-append name "-" version "-checkout")))) =2B (build-system gnu-build-system) =2B (inputs =2B `(("book" =2B ,(origin =2B (method url-fetch) =2B (uri (string-append "https://github.com/metamath/" =2B "metamath-book/archive/second_edition.tar= =2Egz")) =2B (sha256 =2B (base32 =2B "1kbgajik9dn870db1zslqyvhn2j8g7shb8d6dm6njwqfkygiliir")))))= =29 =2B (native-inputs `(("autoconf" ,autoconf) =2B ("automake" ,automake) =2B ("texlive" ,(texlive-union =2B (list texlive-amsfonts =2B texlive-bibtex =2B texlive-breqn =2B texlive-makecell =2B texlive-microtype =2B texlive-tabu =2B texlive-latex-anysize =2B texlive-latex-hyperref =2B texlive-latex-needspace =2B texlive-latex-tools))))) =2B (outputs '("out" "doc")) =2B (arguments =2B `(#:phases =2B (let ((book-builddir "metamath-book-second_edition")) =2B (modify-phases %standard-phases =2B (add-after 'unpack 'unpack-doc =2B (lambda* (#:key inputs #:allow-other-keys) =2B (let ((book-tar (assoc-ref inputs "book"))) =2B (invoke "tar" "xzf" book-tar)))) =2B (add-after 'build 'build-doc =2B (lambda _ =2B (with-directory-excursion book-builddir =2B (invoke "touch" "metamath.ind") =2B (invoke "pdflatex" "metamath") =2B (invoke "pdflatex" "metamath") =2B (invoke "bibtex" "metamath") =2B (invoke "makeindex" "metamath") =2B (invoke "pdflatex" "metamath") =2B (invoke "pdflatex" "metamath")))) =2B (add-after 'build-doc 'install-doc =2B (lambda* (#:key outputs #:allow-other-keys) =2B (let* ((pkg (strip-store-file-name (assoc-ref outputs "ou= =74"))) =2B (out-doc (assoc-ref outputs "doc"))) =2B (install-file (string-append book-builddir "/metamath.p= =64f") =2B (string-append out-doc "/share/doc/" pkg)= =29 =2B #t))))))) =2B (home-page "http://us.metamath.org/") =2B (synopsis "Proof verifier based on a minimalistic formalism") =2B (description "Metamath is a tiny formal language and that can expres= =73 =2Btheorems in abstract mathematics, with an accompyaning @code{metamath} =2Bexecutable that verifies databases of these proofs. There is a public =2Bdatabase, @url{https://github.com/metamath/set.mm, set.mm}, implementing= =0A+first-order logic and Zermelo-Frenkel set theory with Choice, along wit= =68 a =2Blarge swath of associated, high-level theorems, e.g. the Fundamental The= =6Frem of =2BArithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc. See= =20the =2BMetamath book") =2B (license license:gpl2+))) =2D-=20 =32.26.2 =0A= ------_=_0956a90551bf04152c547a44_=_-- ------_=_273a89163ec2adca5de5ddad_=_ Content-Disposition: attachment; filename=signature.asc Content-Type: application/pgp-signature Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- iI0EABYIADUWIQQ7FdZn/PDWvxE6cmR2pStZ7i7CgQUCXrlbuhccZWxhZXh1b3Rl ZUB3aWxzb25iLmNvbQAKCRB2pStZ7i7CgXKJAP9sukjdMRBDlRrDFz0pYqT5VKeX 5fvlKGDfibjWAs6vpAEA3CFPgyuHawPX1KY7gsLLFg1h0jtnoM/D305fsDpe8ws= =pFWs -----END PGP SIGNATURE----- ------_=_273a89163ec2adca5de5ddad_=_--