From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <guix-patches-bounces+larch=yhetil.org@gnu.org>
Received: from mp1 ([2001:41d0:2:4a6f::])
	(using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits))
	by ms11 with LMTPS
	id gEBSFWmp8l4WJgAA0tVLHw
	(envelope-from <guix-patches-bounces+larch=yhetil.org@gnu.org>)
	for <larch@yhetil.org>; Wed, 24 Jun 2020 01:16:25 +0000
Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::])
	(using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits))
	by mp1 with LMTPS
	id MDMiEWmp8l7MNQAAbx9fmQ
	(envelope-from <guix-patches-bounces+larch=yhetil.org@gnu.org>)
	for <larch@yhetil.org>; Wed, 24 Jun 2020 01:16:25 +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 7B8459403D3
	for <larch@yhetil.org>; Wed, 24 Jun 2020 01:16:24 +0000 (UTC)
Received: from localhost ([::1]:37044 helo=lists1p.gnu.org)
	by lists.gnu.org with esmtp (Exim 4.90_1)
	(envelope-from <guix-patches-bounces+larch=yhetil.org@gnu.org>)
	id 1jnu1V-0002NS-TO
	for larch@yhetil.org; Tue, 23 Jun 2020 21:16:21 -0400
Received: from eggs.gnu.org ([2001:470:142:3::10]:48726)
 by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
 (Exim 4.90_1) (envelope-from <Debian-debbugs@debbugs.gnu.org>)
 id 1jnu1C-0002N4-4p
 for guix-patches@gnu.org; Tue, 23 Jun 2020 21:16:02 -0400
Received: from debbugs.gnu.org ([209.51.188.43]:54143)
 by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
 (Exim 4.90_1) (envelope-from <Debian-debbugs@debbugs.gnu.org>)
 id 1jnu1B-0005MR-SP
 for guix-patches@gnu.org; Tue, 23 Jun 2020 21:16:01 -0400
Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2)
 (envelope-from <Debian-debbugs@debbugs.gnu.org>) id 1jnu1B-00063I-NH
 for guix-patches@gnu.org; Tue, 23 Jun 2020 21:16:01 -0400
X-Loop: help-debbugs@gnu.org
Subject: [bug#40815] gnu: Add metamath
Resent-From: elaexuotee@wilsonb.com
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces@debbugs.gnu.org>
Resent-CC: guix-patches@gnu.org
Resent-Date: Wed, 24 Jun 2020 01:16:01 +0000
Resent-Message-ID: <handler.40815.B40815.159296131323203@debbugs.gnu.org>
Resent-Sender: help-debbugs@gnu.org
X-GNU-PR-Message: followup 40815
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: 
To: Nicolas Goaziou <mail@nicolasgoaziou.fr>
Cc: Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= <kuba@kadziolka.net>,
 40815@debbugs.gnu.org
Received: via spool by 40815-submit@debbugs.gnu.org id=B40815.159296131323203
 (code B ref 40815); Wed, 24 Jun 2020 01:16:01 +0000
Received: (at 40815) by debbugs.gnu.org; 24 Jun 2020 01:15:13 +0000
Received: from localhost ([127.0.0.1]:37456 helo=debbugs.gnu.org)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <debbugs-submit-bounces@debbugs.gnu.org>)
 id 1jnu0I-000624-OL
 for submit@debbugs.gnu.org; Tue, 23 Jun 2020 21:15:13 -0400
Received: from m42-5.mailgun.net ([69.72.42.5]:58556)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <bounce+ca63a8.08547a-40815=debbugs.gnu.org@mg.wilsonb.com>)
 id 1jnu0C-000618-EE
 for 40815@debbugs.gnu.org; Tue, 23 Jun 2020 21:15:04 -0400
DKIM-Signature: a=rsa-sha256; v=1; c=relaxed/relaxed; d=mg.wilsonb.com;
 q=dns/txt; 
 s=krs; t=1592961301; h=Content-Type: MIME-Version: Message-Id:
 In-Reply-To: References: Subject: From: Cc: To: Date: Sender;
 bh=5xWv9A+n1/p/KuIw5CR6hefmq8fmrfTDM1WS4I0VnNg=;
 b=PBq+mVsIMvpuBnor5YpmZm+nwSGocYMX/Ib8gVkmupVppEMGFjyVU9Vd7XnxTDc+ZiUpQ/+m
 3Y3wokbSDU9gOJ0w/HRguofAcY2ryqy1EsI7+jdXmKbHMRHV9wK63Tak7JrCQUlweDv19NFE
 StC6ib9PBkx7RcjmkSdVsDWLskQkbaWmTSa3yORQDBzYC4Bk0iuvKLp1VH/E08JP39DF7EfR
 ET/JullMT8NdGCNHZwipSGYETJnQdPq3btX7BItEw7Bfgx1vHVjWK5NYlPjyFsoNsEcMNkPI
 l381gq2iJUtmKFkgH708VtyEhK+SgJuXY23inKFUxh9AwvzZL0ErBQ==
X-Mailgun-Sending-Ip: 69.72.42.5
X-Mailgun-Sid: WyIxOGZjZiIsICI0MDgxNUBkZWJidWdzLmdudS5vcmciLCAiMDg1NDdhIl0=
Received: from wilsonb.com (wilsonb.com [104.199.203.42]) by
 smtp-out-n13.prod.us-east-1.postgun.com with SMTP id
 5ef2a906a3d8a44743275490 (version=TLS1.3, cipher=TLS_AES_128_GCM_SHA256);
 Wed, 24 Jun 2020 01:14:46 GMT
Received: from localhost (KD111239204110.au-net.ne.jp [111.239.204.110])
 by wilsonb.com (Postfix) with ESMTPSA id 8AE98A2C1E;
 Wed, 24 Jun 2020 01:14:43 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wilsonb.com;
 s=201703; t=1592961283;
 bh=5xWv9A+n1/p/KuIw5CR6hefmq8fmrfTDM1WS4I0VnNg=;
 h=Date:To:Cc:From:Subject:References:In-Reply-To:From;
 b=J7TITzrLrOPvFOOjMdcdwEGdu1HT5xbL+awrvUzJsTDbI/M6c4sFGNoQiDtqe56qL
 YB1CQapi4Zw1Z+EicBBmeohHLYhZCvMJS1RzG6ipWdR550nanonaGZKaChjX7AAuIX
 zyqwu7YjZROBZmaEiL4NSsjrhsa5rRRkTKCVK4nwDfPmzojIUXOBhNYTLneFviPg0t
 g6RItWdErQITI8UTCtKuKk0A51YNQOoN2B11mx1MW0DzTfWnuwF6EGVa/iDpeVaqk/
 ULHpGOdhjYaFArQxuxm5aMamMuZGuFZKX2qd9zq5Q8s59UEYQgoiazm8/f4edcRX9/
 LSLqJR8BUG5HBa5EIwXGSiyKzj3tvH9zuLp91k8zsedNcWNCaXUgH7gqFFGV/1idZj
 EpEK96qD2YML2RzDHsE8yeZuplhRK5n4pOLUiS3cG8CMwQ7LqhCGCHJUmtzVCVSHj3
 zckxPLXFbyTessr3wqin4lTWMBrSH2uN8pq+Uq+y2D0x+PDqTD0PxFj9yoTv3hJglo
 6/pXLgatUxMMmviBU0JCHr2JgvS+mbqrMjUA7XeW0pUvWsMxdW2Y4cMLsVBFzdfUuq
 rNQlId0ia+JEcY8/u7cYT0Q7s70ssehF4fOj88DxzLqsl0UL5ZODAAkz1XD1OoKrZ3
 +1lGwmWitqbSZyErN8k4HUNc=
Date: Wed, 24 Jun 2020 10:14:39 +0900
References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com>
 <20200426172945.7ez6i2fl3pjcoexd@gravity>
 <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com>
 <20200427121248.cga7p43flnusf7zo@gravity>
 <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com>
 <25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com> <87d06eraaf.fsf@nicolasgoaziou.fr>
In-Reply-To: <87d06eraaf.fsf@nicolasgoaziou.fr>
Message-Id: <31H3GR8EOYWGZ.2EEY2GE3LMLRZ@wilsonb.com>
User-Agent: mblaze/0.7
MIME-Version: 1.0
Content-Type: multipart/signed; micalg="pgp-sha1";
 protocol="application/pgp-signature";
 boundary="----_=_23e6165e77eb4ce4043f1aa2_=_"
X-Spam-Score: 2.0 (++)
X-BeenThere: debbugs-submit@debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
X-Spam-Score: 1.0 (+)
X-BeenThere: guix-patches@gnu.org
List-Id: <guix-patches.gnu.org>
List-Unsubscribe: <https://lists.gnu.org/mailman/options/guix-patches>,
 <mailto:guix-patches-request@gnu.org?subject=unsubscribe>
List-Archive: <https://lists.gnu.org/archive/html/guix-patches>
List-Post: <mailto:guix-patches@gnu.org>
List-Help: <mailto:guix-patches-request@gnu.org?subject=help>
List-Subscribe: <https://lists.gnu.org/mailman/listinfo/guix-patches>,
 <mailto:guix-patches-request@gnu.org?subject=subscribe>
Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org
Sender: "Guix-patches" <guix-patches-bounces+larch=yhetil.org@gnu.org>
Reply-to: elaexuotee@wilsonb.com, elaexuotee--- via Guix-patches <guix-patches@gnu.org>
From: elaexuotee--- via Guix-patches via <guix-patches@gnu.org>
X-Scanner: scn0
Authentication-Results: aspmx1.migadu.com;
	dkim=fail (rsa verify failed) header.d=mg.wilsonb.com header.s=krs header.b=PBq+mVsI;
	dkim=fail (rsa verify failed) header.d=wilsonb.com header.s=201703 header.b=J7TITzrL;
	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: YB58JfkmcIpj

This is a multipart message in MIME format.

------_=_23e6165e77eb4ce4043f1aa2_=_
MIME-Version: 1.0
Content-Type: multipart/mixed; boundary="----_=_398bc6d86f3b7154107c411f_=_"

This is a multipart message in MIME format.

------_=_398bc6d86f3b7154107c411f_=_
Content-Type: text/plain; charset=UTF-8
Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable

Oops. Looks like my previous emais's patch was for the version that *didn't=
*
comment out the "doc" output. The one included here should be correct.


------_=_398bc6d86f3b7154107c411f_=_
Content-Disposition: attachment; filename=0001-gnu-Add-metamath.patch
Content-Type: text/x-patch
Content-Transfer-Encoding: quoted-printable

=46rom 74db38db11a7e107119362983e388cfb5ead3431 Mon Sep 17 00:00:00 2001
=46rom: "B. Wilson" <elaexuotee@wilsonb.com>
=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 | 97 ++++++++++++++++++++++++++++++++++++++++++
=201 file changed, 97 insertions(+)
=0Adiff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
=69ndex 45d699e39c..e6f4cbe980 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 <vkor@vkten.in>
=20;;; Copyright =C2=A9 2020 Vincent Legoll <vincent.legoll@gmail.com>
=20;;; Copyright =C2=A9 2020 Nicol=C3=B2 Balzarotti <nicolo@nixo.xyz>
=2B;;; Copyright =C2=A9 2020 B. Wilson <elaexuotee@wilsonb.com>
=20;;;
=20;;; This file is part of GNU Guix.
=20;;;
=40@ -5686,3 +5687,99 @@ 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  ;; Upstream pushed a commit on top of v0.182 that fixes a bug in Makef=
=69le.am.
=2B  ;; Using this commit lets us avoid directly including the patch here. =
=20In the
=2B  ;; next version bump, we should be able to replace this and directly u=
=73e the
=2B  ;; version tag.
=2B  (let ((commit "5df616efe4119ff88daf77e7041d45b6fa39c578")
=2B        (revision "0")
=2B        (book-name "metamath-book")
=2B        (book-version "second_edition"))
=2B    (package
=2B      (name "metamath")
=2B      (version (git-version "0.182" revision commit))
=2B      (source
=2B       (origin
=2B         (method git-fetch)
=2B         (uri (git-reference
=2B               (url "https://github.com/metamath/metamath-exe.git")
=2B               (commit commit)))
=2B         (sha256
=2B          (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"=
=29)
=2B         (file-name (git-file-name name version))))
=2B      ;; FIXME: Unfortunately, there seems to be a problem with
=2B      ;; texlive-amsfonts that prevents us from typsetting the "doc" out=
=70ut
=2B      ;; pdf.  Once fixed, this along with the commented out sections be=
=6Cow,
=2B      ;; should be enabled.
=2B      ; (outputs '("out" "doc"))
=2B      (build-system gnu-build-system)
=2B      ;; FIXME: Enable for "doc" output.  See previous comment.
=2B      ; (inputs
=2B      ;  `((,book-name
=2B      ;     ,(origin
=2B      ;        (method git-fetch)
=2B      ;        (uri (git-reference
=2B      ;              (url "https://github.com/metamath/metamath-book.git=
=22)
=2B      ;              (commit book-version)))
=2B      ;        (sha256
=2B      ;         (base32
=2B      ;          "1kk9nfhs0h8qccpxp1qh072bpfis7h05rlnz3qn1z641d9i4ryyq")=
=29
=2B      ;        (file-name (git-file-name book-name book-version))))))
=2B      (native-inputs `(("autoconf" ,autoconf)
=2B                       ("automake" ,automake)
=2B                       ;; FIXME: Required inputs to build the "doc" outp=
=75t.
=2B                       ;; See above comment.
=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                       ))
=2B      ;; FIXME: Arguments to build the "doc" output.  See above comment.=
=0A+      ; (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 (assoc-ref inputs ,book-name)))
=2B      ;              (mkdir-p book-builddir)
=2B      ;              (copy-recursively book book-builddir))))
=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=
=20"out")))
=2B      ;                   (out-doc (assoc-ref outputs "doc")))
=2B      ;              (install-file (string-append book-builddir "/metama=
=74h.pdf")
=2B      ;                            (string-append out-doc "/share/doc/" =
=70kg))
=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 expr=
=65ss
=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 T=
=68eorem
=2Bof Arithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc.  =
=53ee the
=2BMetamath book.")
=2B    ;; FIXME: The "doc" output requires license:cc0.  See above comment.=
=0A+    ; (license '(,license:gpl2+ ,license:cc0)))))
=2B    (license license:gpl2+))))
=2D-=20
=32.27.0
=0A=

------_=_398bc6d86f3b7154107c411f_=_--

------_=_23e6165e77eb4ce4043f1aa2_=_
Content-Disposition: attachment; filename=signature.asc
Content-Type: application/pgp-signature
Content-Transfer-Encoding: 7bit

-----BEGIN PGP SIGNATURE-----

iI0EABYIADUWIQQ7FdZn/PDWvxE6cmR2pStZ7i7CgQUCXvKo/hccZWxhZXh1b3Rl
ZUB3aWxzb25iLmNvbQAKCRB2pStZ7i7CgQ8aAP9XbXNroGsRIn0faF8qKaip/7hk
VkGCMYnT03pq23eziAEApzEayV7nNLR5WBY9C7rmqV4yzJTl2LvEdiyxsSbhhA0=
=MvlX
-----END PGP SIGNATURE-----

------_=_23e6165e77eb4ce4043f1aa2_=_--