From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <guix-patches-bounces+larch=yhetil.org@gnu.org>
Received: from mp2 ([2001:41d0:2:4a6f::])
	(using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits))
	by ms11 with LMTPS
	id YOT1AXno8V6+EgAA0tVLHw
	(envelope-from <guix-patches-bounces+larch=yhetil.org@gnu.org>)
	for <larch@yhetil.org>; Tue, 23 Jun 2020 11:33:13 +0000
Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::])
	(using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits))
	by mp2 with LMTPS
	id 4LlyOXjo8V4kXQAAB5/wlQ
	(envelope-from <guix-patches-bounces+larch=yhetil.org@gnu.org>)
	for <larch@yhetil.org>; Tue, 23 Jun 2020 11:33: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 20689940990
	for <larch@yhetil.org>; Tue, 23 Jun 2020 11:33:12 +0000 (UTC)
Received: from localhost ([::1]:53022 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 1jnhAr-00018T-AE
	for larch@yhetil.org; Tue, 23 Jun 2020 07:33:09 -0400
Received: from eggs.gnu.org ([2001:470:142:3::10]:41512)
 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 1jnhAk-00017k-1n
 for guix-patches@gnu.org; Tue, 23 Jun 2020 07:33:02 -0400
Received: from debbugs.gnu.org ([209.51.188.43]:52274)
 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 1jnhAj-0008OC-Nt
 for guix-patches@gnu.org; Tue, 23 Jun 2020 07:33:01 -0400
Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2)
 (envelope-from <Debian-debbugs@debbugs.gnu.org>) id 1jnhAj-0004yv-LF
 for guix-patches@gnu.org; Tue, 23 Jun 2020 07:33: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: Tue, 23 Jun 2020 11:33:01 +0000
Resent-Message-ID: <handler.40815.B40815.159291197419136@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.159291197419136
 (code B ref 40815); Tue, 23 Jun 2020 11:33:01 +0000
Received: (at 40815) by debbugs.gnu.org; 23 Jun 2020 11:32:54 +0000
Received: from localhost ([127.0.0.1]:35587 helo=debbugs.gnu.org)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <debbugs-submit-bounces@debbugs.gnu.org>)
 id 1jnhAX-0004yV-Ak
 for submit@debbugs.gnu.org; Tue, 23 Jun 2020 07:32:54 -0400
Received: from m42-5.mailgun.net ([69.72.42.5]:25888)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <bounce+ca63a8.08547a-40815=debbugs.gnu.org@mg.wilsonb.com>)
 id 1jnhAS-0004y9-HK
 for 40815@debbugs.gnu.org; Tue, 23 Jun 2020 07:32:48 -0400
DKIM-Signature: a=rsa-sha256; v=1; c=relaxed/relaxed; d=mg.wilsonb.com;
 q=dns/txt; 
 s=krs; t=1592911967; h=Content-Type: MIME-Version: Message-Id:
 In-Reply-To: References: Subject: From: Cc: To: Date: Sender;
 bh=a10opU8ccwtmcRfUszvEOfA+87Kjm8YRP2AACKESBw4=;
 b=s8REuDcP8Ato9mg8ULwYCbAnXtuFcwedEcqtOuyGUzE6/5yi6lemZehSRJyFvsY5Wc3oJQ8i
 abuOG4NGUcaejtuwioak5BqyhsRzjXpy39d7vxwgCSsJel9yzKoSsYspRTxXA8cBBZM31xK/
 eQS1/z8fXwvP1cGj3WGWa5zxadpKt6EvRiv1eKkCOAZ9wCd0GYll1/ROBJboU2PKHiajNDBX
 Ny3JZeysIbQ+dm/vLruC7wTuYTEGYSuBc7LSj2X1VPOuLDvGLNviohS7vC3WmtxGhDXwAF5S
 8C++3U2JZA4OlHrtzFF6lZhsww7atPp46OBv9ysdXqr6AiiUdWOw8A==
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-n06.prod.us-east-1.postgun.com with SMTP id
 5ef1e84686de6ccd44aa255f (version=TLS1.3, cipher=TLS_AES_128_GCM_SHA256);
 Tue, 23 Jun 2020 11:32:22 GMT
Received: from localhost (KD111239209250.au-net.ne.jp [111.239.209.250])
 by wilsonb.com (Postfix) with ESMTPSA id 3577FA2B2F;
 Tue, 23 Jun 2020 11:32:19 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wilsonb.com;
 s=201703; t=1592911939;
 bh=a10opU8ccwtmcRfUszvEOfA+87Kjm8YRP2AACKESBw4=;
 h=Date:To:Cc:From:Subject:References:In-Reply-To:From;
 b=0HIkxt2aR9sLOuPT641G5Ps2egmRKDJQL2IWEO8htYI86uuDMjMT+NTcr2VK5NYqz
 vBN9Yoco7n9CRU4NMtYnOsgoNBJZl15oF8vsi/y1rOMEBD+Z4GAigFftstyERpRTsl
 b969LNsJW/4uwZx8FPOKfortwrim3gS5mBYgx3RZtfyMmPNPcw8U7B10E7HiLXyYkj
 DzuzA56nzmrdPxPp4euEL15fwsOqGDqbPSB4902zPx3JHjZY688hFR0MwY85yZuHfL
 W+pVejkC36TeHxsw3NKyFwkZHf+l+YKGh8yu692zq98Qfyf745woOvpvvDmJlQAPTk
 JbXsV9yHvl+MrMJx4KWJnJIqHDRBB6gmzXtz/uyeRdYbsQ8T5jFEh4TskXNmbueJ7k
 FVN5FaSEG1Y25z+AY5VkFYpzQxtTuWVKTaYd/L6GS9ddO6SXokhxz0/5RQ8wV8vkcq
 kQFo1H6jX4V8s3ezGWS5HPG8pjeWwK5p6gLrrgJZPboAl9aqqthS/Z+DQCBGygFxkL
 cfSSpOIa/x0pQuMsLayfnWBgzz0L+MbLSlDUc0AeW/k/nSGlI5z2fKi3Cf+mybRfbX
 xjYVOFC8VGHLrVTyg2Ms0YqiVmQO25e6VS3Bw95v43mY1wi5wkC/2AG7PECn7VfW6d
 M+F1WdPYIZgNv+YNf/s3JeGU=
Date: Tue, 23 Jun 2020 20:32:15 +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: <23UB7VNWCB6BC.23I1T2MHNG4ZI@wilsonb.com>
User-Agent: mblaze/0.7
MIME-Version: 1.0
Content-Type: multipart/signed; micalg="pgp-sha1";
 protocol="application/pgp-signature";
 boundary="----_=_72224fa1070edd531e04536d_=_"
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=s8REuDcP;
	dkim=fail (rsa verify failed) header.d=wilsonb.com header.s=201703 header.b=0HIkxt2a;
	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: SSRn7RP1Aupb

This is a multipart message in MIME format.

------_=_72224fa1070edd531e04536d_=_
MIME-Version: 1.0
Content-Type: multipart/mixed; boundary="----_=_1629333b79c91715769c82f7_=_"

This is a multipart message in MIME format.

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

Hello Nicolas,

Thank you for taking a look at this!

> Unfortunately I cannot comment about Texlive packages, and particularly
> about the issue you're encountering there, but I can give some advice on
> this package definition.

This patch has been languishing around for quite a while, and instead of
waiting for texlive-amsfonts to get fixed, I propose nuking the "doc" outpu=
t
for now so we can get this pushed.

The attached patch does just this. I commented out the parts specific to th=
e
"doc" output and also included FIXME explanations of what's going on.

> I suggest to let-bind the commit hash around the package definition, add
> a revision number, and a comment explaining why you're not using plain
> v0.182 tag.

Done.

> > +    (build-system gnu-build-system)
> > +    (inputs
> > +     `(("book"
> > +        ,(origin
> > +           (method url-fetch)
> > +           (uri (string-append "https://github.com/metamath/"
> > +                               "metamath-book/archive/second_edition.t=
ar.gz"))
>=20
> IIRC, this URL is reliable. You could fetch "second_editon" tag instead.

This is now a commented out section, but I went ahead and updated it as you=

suggested. Since this is a non-cosmetic change, I also test built it before=

commenting out all the "doc" output stuff.

> Nitpick: [outputs] is often located right after the source keyword.

Moved. Not sure why I put it down there in the first place. I chock it up t=
o
this being my first package attempt.

> You cannot use "e.g." in Texinfo syntax, because the last dot confuses
> it. It should be either "e.g.,", or "e.g.@:".
>=20
> > +Arithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc.  S=
ee the
> > +Metamath book")
>=20
> Missing final full stop.

Fixed. Thanks for the attention to detail.

> I think there are other licenses involved. Could you try to list them,
> too?

Were you referring to CC0 for the metamath book?

I added this license in a FIXME comment. As far as I can tell, the metamath=

executable itself is just GLP2+, but if I'm missing something please let me=

know.


Hopefully, in the near future I will find time to dig into the texlive-amsf=
onts
issue, but for now, does this look good?

If we end up pushing just the metamath patch, the other texlive package pat=
ches
obviously aren't needed for now, but would it be worth pushing these? Shoul=
d I
submit separate issues for them?

Cheers,


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

=46rom f7e7a323df50fc5c6d4aefb30f67991c367dfabc 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 | 75 ++++++++++++++++++++++++++++++++++++++++++
=201 file changed, 75 insertions(+)
=0Adiff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
=69ndex 45d699e39c..82b98d8f7d 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,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.27.0
=0A=

------_=_1629333b79c91715769c82f7_=_--

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

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

iI0EABYIADUWIQQ7FdZn/PDWvxE6cmR2pStZ7i7CgQUCXvHoOBccZWxhZXh1b3Rl
ZUB3aWxzb25iLmNvbQAKCRB2pStZ7i7CgYIHAQC4vb+FbU2y/Tq2vfTjkKLCe3p+
RfrmFdsSZzDPiSY9tAD9Ew21FUW7H0AEPRuquynZyccz5xSWfeW8mZeOqWNnCQY=
=ds0W
-----END PGP SIGNATURE-----

------_=_72224fa1070edd531e04536d_=_--