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 6ByGJAOhu14mawAA0tVLHw (envelope-from ) for ; Wed, 13 May 2020 07:25:55 +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 aDNqDhKhu17GTgAA1q6Kng (envelope-from ) for ; Wed, 13 May 2020 07:26:10 +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 441FA94050C for ; Wed, 13 May 2020 07:26:07 +0000 (UTC) Received: from localhost ([::1]:49696 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1jYlmI-0007Eo-Vk for larch@yhetil.org; Wed, 13 May 2020 03:26:07 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:53488) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1jYlmE-0007C0-LH for guix-patches@gnu.org; Wed, 13 May 2020 03:26:02 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:45709) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1jYlmE-0002mC-Cn for guix-patches@gnu.org; Wed, 13 May 2020 03:26:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1jYlmE-0001c1-8b for guix-patches@gnu.org; Wed, 13 May 2020 03:26:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#40815] gnu: Add metamath. References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> In-Reply-To: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> Resent-From: elaexuotee@wilsonb.com Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Wed, 13 May 2020 07:26:02 +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 Received: via spool by 40815-submit@debbugs.gnu.org id=B40815.15893547446172 (code B ref 40815); Wed, 13 May 2020 07:26:02 +0000 Received: (at 40815) by debbugs.gnu.org; 13 May 2020 07:25:44 +0000 Received: from localhost ([127.0.0.1]:57255 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jYllr-0001bO-7g for submit@debbugs.gnu.org; Wed, 13 May 2020 03:25:44 -0400 Received: from m42-5.mailgun.net ([69.72.42.5]:11341) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jYlln-0001b7-46 for 40815@debbugs.gnu.org; Wed, 13 May 2020 03:25:38 -0400 DKIM-Signature: a=rsa-sha256; v=1; c=relaxed/relaxed; d=mg.wilsonb.com; q=dns/txt; s=krs; t=1589354737; h=Content-Type: MIME-Version: Message-Id: Subject: From: To: Date: Sender; bh=PKXMj1p67RsaBaj4Qb6Jzz0UUWut2IjSSaWOVGRTqSE=; b=qvESmOodrnTAkCU0X26A3kNxdSrqfYO+/A6I3Vd1CXG5ET//vAMNnprnTtokFgVukGkTF+rv vo6tzkntNxmSLnqpUrGYfTx04Q+YtqWYFRnvTUlMC/VIRF6KM+nigb/KiMouO1EZ/tPMYn6o GmxWT/cMhhUd4mfQ/sbkH9Tph7U0hrj/kUzTsW+UDaTZ7J7Hz0rEnqysBgm9xYPCU2kFkEwm yH2PaUaqwCvhG+HXEdnmOAmudg0L+o5fxWc6+n5HH/aGVOADdmLzPOZoeJ0xwY3SZ4BFwpDJ iepapd09bGw7/7Txhd1r/h6BpPRlBdhqsUIx1irSM/0f9MW6gEvArw== X-Mailgun-Sending-Ip: 69.72.42.5 X-Mailgun-Sid: WyIxOGZjZiIsICI0MDgxNUBkZWJidWdzLmdudS5vcmciLCAiMDg1NDdhIl0= Received: from wilsonb.com (wilsonb.com [104.199.203.42]) by mxa.mailgun.org with ESMTP id 5ebba0dd.7fe5efd7be40-smtp-out-n05; Wed, 13 May 2020 07:25:17 -0000 (UTC) Received: from localhost (KD111239206087.au-net.ne.jp [111.239.206.87]) by wilsonb.com (Postfix) with ESMTPSA id 716E0A137A for <40815@debbugs.gnu.org>; Wed, 13 May 2020 07:25:15 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wilsonb.com; s=201703; t=1589354715; bh=PKXMj1p67RsaBaj4Qb6Jzz0UUWut2IjSSaWOVGRTqSE=; h=Date:To:From:Subject:From; b=kfwFAVAbXyZcqN4JvNtZLceM1VgKaXncIMy6+Xws0C4ayqeot0H9LJW9Hoe3k5/aU BpotTmPH6pby36FEbAOKPzFjzNbs0EPq13S+kZMGXQarqHjd5XJKAvyuf5lLGfuvNq gs9J9uUsvZGhmedyXyefBeCqkI4TLG4DcvAu+Zgs7BQyVmWjK694M0pHNvkEXfvTnw OBKWnpCa0VsjMTtPQDIBK1JaioFyBV3VvJA3m1iMRDWDnnE7xAD0I+nnq4NnyN0gtL S2mWWFsq0u+ky9HXwOXwtAIEwqm6DC9qjoxKGHIFrusOIpDJ43WzBZq7qdJsCuhoEE 1pc+W7CWAm0o0twjppxrN0D+IWTY6wUkAQWczQ4L4+b9TExOxDgzUUCsTtlyM4Z+Iy kxmcmls7s3/LX9WTjes8vP32HCkxDvV5XF/ujHaiR8x4NRnTBUFjY/fMI9ZwilW0yc VHapqj7U4MaT9CYQpFQ4uLUf+59V9mcLarl1c1flpv2pc1NJei9AsUv5dWTFvdie9S n0xfl+iaJDTEOUo3OH9sdBlt+S5rsK2rwbr+RJybgomudH9WktdKiv87Ajk8Z7jzoJ Ah73/XF9RQYHAFV6s4g0npzSpDPMbHkfKQt0WtZe02LvCVmKV92yrRN+X0qPUVjXPf RNHL6alHOsAt+cm25QFkI4Tg= Date: Wed, 13 May 2020 16:25:11 +0900 Message-Id: <3A31ISRYFT791.2TFZ4E8NIDG43@wilsonb.com> User-Agent: mblaze/0.5.1 MIME-Version: 1.0 Content-Type: multipart/signed; micalg="pgp-sha1"; protocol="application/pgp-signature"; boundary="----_=_205eb33e5ee0479245956195_=_" X-Spam-Score: 1.8 (+) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-Spam-Score: 0.8 (/) 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 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=qvESmOod; dkim=fail (rsa verify failed) header.d=wilsonb.com header.s=201703 header.b=kfwFAVAb; 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.53966220717843]; DWL_DNSWL_BLOCKED(0.00)[209.51.188.17:from]; R_SPF_ALLOW(-0.20)[+ip4:209.51.188.0/24:c]; IP_REPUTATION_HAM(0.00)[asn: 22989(0.06), country: US(-0.00), ip: 209.51.188.17(-0.54)]; HAS_ATTACHMENT(0.00)[]; TO_DN_NONE(0.00)[]; R_DKIM_REJECT(1.00)[mg.wilsonb.com:s=krs,wilsonb.com:s=201703]; MX_GOOD(-0.50)[cached: eggs.gnu.org]; 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]; FROM_NEQ_ENVFROM(0.00)[guix-patches@gnu.org,guix-patches-bounces@gnu.org]; TAGGED_FROM(0.00)[larch=yhetil.org]; ARC_NA(0.00)[]; RECEIVED_SPAMHAUS_PBL(0.00)[111.239.206.87:received]; FROM_HAS_DN(0.00)[]; URIBL_BLOCKED(0.00)[gnu.org:email,metamath.org:url,vkten.in:email,nixo.xyz:email,wilsonb.com:email,set.mm:url]; MIME_GOOD(-0.20)[multipart/signed,multipart/mixed,text/plain,text/x-patch]; REPLYTO_DOM_NEQ_FROM_DOM(0.00)[]; PREVIOUSLY_DELIVERED(0.00)[40815@debbugs.gnu.org]; HAS_LIST_UNSUB(-0.01)[]; RCPT_COUNT_ONE(0.00)[1]; DMARC_NA(0.00)[gnu.org]; RWL_MAILSPIKE_POSSIBLE(0.00)[209.51.188.17:from]; RCVD_COUNT_SEVEN(0.00)[9]; FORGED_SENDER_MAILLIST(0.00)[] X-TUID: VTCH1AIlR/uR This is a multipart message in MIME format. ------_=_205eb33e5ee0479245956195_=_ MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----_=_673a3b405c10a00e2c730834_=_" This is a multipart message in MIME format. ------_=_673a3b405c10a00e2c730834_=_ Content-Type: text/plain; charset=UTF-8 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Just discovered the (git-file-name ...) function. This is a simple update t= o the metamath patch to use this instead of manually using string-append. ------_=_673a3b405c10a00e2c730834_=_ Content-Disposition: attachment; filename=0001-gnu-Add-metamath.patch Content-Type: text/x-patch Content-Transfer-Encoding: quoted-printable =46rom 0e9facf67f5af44bb8e605631a0be6c90ce23000 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 d60c033dbc..5a7230cb53 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@ -5635,3 +5636,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 (git-file-name name version)))) =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= ------_=_673a3b405c10a00e2c730834_=_-- ------_=_205eb33e5ee0479245956195_=_ Content-Disposition: attachment; filename=signature.asc Content-Type: application/pgp-signature Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- iI0EABYIADUWIQQ7FdZn/PDWvxE6cmR2pStZ7i7CgQUCXrug1hccZWxhZXh1b3Rl ZUB3aWxzb25iLmNvbQAKCRB2pStZ7i7CgfzUAQDulEAGYH6mXFyTY0u9lTQo7QMO xztc0htALud3m9OtQQEA/2wSBD0wzWU9Z6Erd1rX3PW9EBya4y+z3ouXeSLy1Qo= =cnZ1 -----END PGP SIGNATURE----- ------_=_205eb33e5ee0479245956195_=_--