From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <guix-patches-bounces+larch=yhetil.org@gnu.org>
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 eNqyNoI2uV41SQAA0tVLHw
	(envelope-from <guix-patches-bounces+larch=yhetil.org@gnu.org>)
	for <larch@yhetil.org>; Mon, 11 May 2020 11:26:58 +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 2PJ2MZA2uV5AUAAA1q6Kng
	(envelope-from <guix-patches-bounces+larch=yhetil.org@gnu.org>)
	for <larch@yhetil.org>; Mon, 11 May 2020 11:27: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 89D3B940BFF
	for <larch@yhetil.org>; Mon, 11 May 2020 11:27:09 +0000 (UTC)
Received: from localhost ([::1]:43672 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 1jY6aT-0001A8-Vj
	for larch@yhetil.org; Mon, 11 May 2020 07:27:10 -0400
Received: from eggs.gnu.org ([2001:470:142:3::10]:57142)
 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 1jY6aM-00018v-9H
 for guix-patches@gnu.org; Mon, 11 May 2020 07:27:02 -0400
Received: from debbugs.gnu.org ([209.51.188.43]:39883)
 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 1jY6aL-000564-W6
 for guix-patches@gnu.org; Mon, 11 May 2020 07:27:02 -0400
Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2)
 (envelope-from <Debian-debbugs@debbugs.gnu.org>) id 1jY6aL-0004oN-Sk
 for guix-patches@gnu.org; Mon, 11 May 2020 07:27:01 -0400
X-Loop: help-debbugs@gnu.org
Subject: [bug#40815] gnu: Add metamath
Resent-From: "B. Wilson" <elaexuotee@wilsonb.com>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces@debbugs.gnu.org>
Resent-CC: guix-patches@gnu.org
Resent-Date: Mon, 11 May 2020 11:27:01 +0000
Resent-Message-ID: <handler.40815.B.158919638618425@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: Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= <kuba@kadziolka.net>
Cc: 40815@debbugs.gnu.org
X-Debbugs-Original-Cc: guix-patches@gnu.org
Received: via spool by submit@debbugs.gnu.org id=B.158919638618425
 (code B ref -1); Mon, 11 May 2020 11:27:01 +0000
Received: (at submit) by debbugs.gnu.org; 11 May 2020 11:26:26 +0000
Received: from localhost ([127.0.0.1]:51425 helo=debbugs.gnu.org)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <debbugs-submit-bounces@debbugs.gnu.org>)
 id 1jY6Zf-0004mt-25
 for submit@debbugs.gnu.org; Mon, 11 May 2020 07:26:26 -0400
Received: from lists.gnu.org ([209.51.188.17]:47928)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <bounce+686de0.08547a-guix-patches=gnu.org@mg.wilsonb.com>)
 id 1jY6ZS-0004mK-Oc
 for submit@debbugs.gnu.org; Mon, 11 May 2020 07:26:15 -0400
Received: from eggs.gnu.org ([2001:470:142:3::10]:57040)
 by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
 (Exim 4.90_1)
 (envelope-from <bounce+686de0.08547a-guix-patches=gnu.org@mg.wilsonb.com>)
 id 1jY6ZS-0000hY-IK
 for guix-patches@gnu.org; Mon, 11 May 2020 07:26:06 -0400
Received: from m42-5.mailgun.net ([69.72.42.5]:31642)
 by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
 (Exim 4.90_1)
 (envelope-from <bounce+686de0.08547a-guix-patches=gnu.org@mg.wilsonb.com>)
 id 1jY6ZP-0004mQ-La
 for guix-patches@gnu.org; Mon, 11 May 2020 07:26:06 -0400
DKIM-Signature: a=rsa-sha256; v=1; c=relaxed/relaxed; d=mg.wilsonb.com;
 q=dns/txt; 
 s=krs; t=1589196363; h=Content-Type: MIME-Version: Message-Id:
 In-Reply-To: References: From: Subject: Cc: To: Date: Sender;
 bh=+Rp2ScEzenkZUGKiKm5zKfCE4WC4ZNbzH8P8nJaRsMk=;
 b=Nin0I1XhtkyJtjJxgIDGiNfY71DmJieZT9oHZdCioa22RTmVUygmHV3WhCgVxsilJe7zsyoC
 FjcSvmScDhsdm82dhK6LvNYLOmFcNcuPqxpk1Llz7yhefYtyyYNj4ghYaa3TTvDw7tUlWStx
 jvN0R9MiTjbuKDybUjNrsRhQSMCstTvTNv9TQHvD8xLJE1xyJrlu7Ej4h/RkD39pv0P/Fp7f
 R50S1+i+vTSz8z+RhKrq6PjCb03kgfVXrExrKy3RPZXdjwwaEJiRlLMZGtLhlAWZJLogTAxh
 kyyF4lVtDOk8Txf4D73NOLOjZogq5yoRJTjrQnXWskm8HjFskGH1Tw==
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 5eb93642.7fd1c8ec4c30-smtp-out-n05;
 Mon, 11 May 2020 11:25:54 -0000 (UTC)
Received: from localhost (KD111239199242.au-net.ne.jp [111.239.199.242])
 by wilsonb.com (Postfix) with ESMTPSA id EEB9BA00C8;
 Mon, 11 May 2020 11:25:49 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wilsonb.com;
 s=201703; t=1589196350;
 bh=+Rp2ScEzenkZUGKiKm5zKfCE4WC4ZNbzH8P8nJaRsMk=;
 h=Date:To:Cc:Subject:From:References:In-Reply-To:From;
 b=x2NWy6BoKKwYuYKcLLpOYak7UmN+CQaCAn0XRSBRHOXc2RhDIaa0rpa6YPYKdwLyu
 0P+ZPHOD7GVVsJq3KOs2gX1vZgQnSRhLCjquduW5dqumvZeu9wEcht80h/ftXx0Op2
 V24JNnLKVafE11czzhEVgFXjWRfGw4C960jsZEAEuFQWNhA5+gX+GlVTJFCYXaB4rX
 2bQwpu0AXiL6sJIy2w3F9Rn2jaT7glk523CAjVmB8KGfrv75oywYRpQ85omzTM2aRN
 RLHCrVqxHOS1NQcKrGYD4MHp3wyL4sPpvDhiLkvivCnIpW9C/72y5G3qvpWT8UjbS+
 u15bBAQmTCZG/BnR3IHipL+6pmrkCNBmRVvgP2jdde2DtTETVecq12kI0wvIEqn7Oy
 AKN8ctWRwf+nziAQW07UeCZer4yobaQk8ae4D4N3c3qrXd91hZweIFKXMDKN7g4iWq
 nmSWzZUzerCLu/orOMGwPXz+dvDaAUDfc2WtwODzWZHB9D49yA7+WP7WFsiZloxmXC
 dshG2wCSXrJsZ13Lpol6Zu9hO6diayy7gTXDq7j5vX6VdL36ps5Enqo5387za9n+A7
 qCjWrmO+XNB3ION8XsP8RfZRd0mdzams6B1+r35rOUBxRVgay9iJB7WIdOiMU1gCAg
 ntd8JTIMrReVnWw26DyU3xvg=
Date: Mon, 11 May 2020 20:25:36 +0900
References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com>
 <20200426172945.7ez6i2fl3pjcoexd@gravity>
 <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com>
 <20200427121248.cga7p43flnusf7zo@gravity>
In-Reply-To: <20200427121248.cga7p43flnusf7zo@gravity>
Message-Id: <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com>
User-Agent: mblaze/0.5.1
MIME-Version: 1.0
Content-Type: multipart/signed; micalg="pgp-sha1";
 protocol="application/pgp-signature";
 boundary="----_=_0a1b9dd2691359a86d6aaff6_=_"
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 07:26:01
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: 1.8 (+)
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: "B. Wilson" <elaexuotee@wilsonb.com>, "B. Wilson via Guix-patches" <guix-patches@gnu.org>
From: "B. Wilson via Guix-patches" via <guix-patches@gnu.org>
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=Nin0I1Xh;
	dkim=fail (rsa verify failed) header.d=wilsonb.com header.s=201703 header.b=x2NWy6Bo;
	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.53976677651143];
	 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:+,5:+,6:+,7:+,8:+,9:+,10:+,11:~];
	 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)[];
	 URIBL_BLOCKED(0.00)[gnu.org:email,scratchpost.org:email,nixo.xyz:email,wspr.io:url,metamath.org:url,kadziolka.net:email,vkten.in:email,wilsonb.com:email,set.mm:url];
	 FROM_HAS_DN(0.00)[];
	 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)[];
	 RECEIVED_SPAMHAUS_PBL(0.00)[111.239.199.242:received];
	 RWL_MAILSPIKE_POSSIBLE(0.00)[209.51.188.17:from];
	 RCVD_COUNT_SEVEN(0.00)[11];
	 FORGED_SENDER_MAILLIST(0.00)[]
X-TUID: Nzlae0P+9iZz

This is a multipart message in MIME format.

------_=_0a1b9dd2691359a86d6aaff6_=_
MIME-Version: 1.0
Content-Type: multipart/mixed; boundary="----_=_4472d14409cc91f020ddb2ab_=_"

This is a multipart message in MIME format.

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

Well, after a good bit of wrangling, here is another round.

We have URLs pointing to static sources; I got upstream to fix things so we=

don't need a patch; and now we're generating the doc output's pdf from the =
TeX
source.

The latter is what made this take so much time and effort.

On the one hand, it required packaging up 6 texlive dependencies, which are=

included in the attached patches. On the other hand, it turns out that the
texlive-amsfonts package is broken, which we need to typset the metamath do=
c
output. This caused me tons of grief but turns out to be a known issue:

https://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D40558

Thus, as of commit a1f84aca, the attached patch for metamath actually break=
s.
However, with the proposed patched included in issue #40558 above, it build=
s
just fine.

Regarding the patches for the texlive packages, I did all of them as
simple-texlive-package templates with #:trivial? #t, grabbing the files fro=
m
tex/latex and doc/latex. Is this reasonable? Looking at other packages, I
cannot tell whether it'd be preferable to directly generate everything from=
 the
*.dtx and *.sty sources.

Also, regarding texlive-mathstyle and texlive-flexisym, their files reside
under latex/breqn, but since they have their own ctan pages, I opted to spl=
it
them into separate packages and make the dependencies explicit. Does that s=
eem
reasonable?

Anyway, thanks for taking a look! Hopefully, these look mergeable apart fro=
m
the texlive-amsfonts issue.


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

=46rom 2f1efc596c83ae4bf63925c612b54161f55838a1 Mon Sep 17 00:00:00 2001
=46rom: "B. Wilson" <elaexuotee@wilsonb.com>
=44ate: Mon, 11 May 2020 20:02:41 +0900
=53ubject: [PATCH 1/7] gnu: Add texlive-mathstyle.
=54o: guix-patches@gnu.org
=0A* gnu/packages/tex.scm (texlive-mathstyle): New Variable.
=2D--
=20gnu/packages/tex.scm | 17 +++++++++++++++++
=201 file changed, 17 insertions(+)
=0Adiff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scm
=69ndex 683f9d7283..f6d92b5f1c 100644
=2D-- a/gnu/packages/tex.scm
=2B++ b/gnu/packages/tex.scm
=40@ -13,6 +13,7 @@
=20;;; Copyright =C2=A9 2018 Danny Milosavljevic <dannym+a@scratchpost.org>=
=0A ;;; Copyright =C2=A9 2018 Arun Isaac <arunisaac@systemreboot.net>
=20;;; Copyright =C2=A9 2020 Vincent Legoll <vincent.legoll@gmail.com>
=2B;;; Copyright =C2=A9 2020 B. Wilson <elaexuotee@wilsonb.com>
=20;;;
=20;;; This file is part of GNU Guix.
=20;;;
=40@ -7322,3 +7323,19 @@ facilities designed to cope with the more specific=
=20demands of academic
=20writing, especially in the humanities and the social sciences.  All quot=
=65
=20styles as well as the optional active quotes are freely configurable.")
=20      (license license:lppl1.3c+))))
=2B
=2B(define-public texlive-mathstyle
=2B  (package
=2B    (inherit (simple-texlive-package
=2B              "texlive-mathstyle"
=2B              (list "/tex/latex/breqn/mathstyle.sty"
=2B                    "/doc/latex/breqn/mathstyle.pdf")
=2B              (base32 "0rlnp20ns70ir0sac4qwcigr4a25s813cijvjamwm6q42y6wj=
=38vp")
=2B              #:trivial? #t))
=2B    (propagated-inputs `(("texlive-latex-l3kernel" ,texlive-latex-l3kern=
=65l)))
=2B    (home-page "https://www.ctan.org/pkg/mathstyle")
=2B    (synopsis "Manage mathematics typesetting style")
=2B    (description "Flexisym converts mathematical symbol definitions to t=
=68e form
=2Bthey need for breqn to work.  The package offers support for breqn and i=
=73 part
=2Bof the bundle of the same name.")
=2B    (license license:lppl1.3c+)))
=2D-=20
=32.26.2
=0A=

------_=_4472d14409cc91f020ddb2ab_=_
Content-Disposition: attachment; filename=0002-gnu-Add-texlive-flexisym.patch
Content-Type: text/x-patch
Content-Transfer-Encoding: quoted-printable

=46rom 03068f1e5f01fde67f53aa1ea7dcb477c0ab669e Mon Sep 17 00:00:00 2001
=46rom: "B. Wilson" <elaexuotee@wilsonb.com>
=44ate: Mon, 11 May 2020 20:03:54 +0900
=53ubject: [PATCH 2/7] gnu: Add texlive-flexisym.
=54o: guix-patches@gnu.org
=0A* gnu/packages/tex.scm (texlive-flexisym): New variable.
=2D--
=20gnu/packages/tex.scm | 21 +++++++++++++++++++++
=201 file changed, 21 insertions(+)
=0Adiff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scm
=69ndex f6d92b5f1c..6727a2c985 100644
=2D-- a/gnu/packages/tex.scm
=2B++ b/gnu/packages/tex.scm
=40@ -7339,3 +7339,24 @@ styles as well as the optional active quotes are f=
=72eely configurable.")
=20they need for breqn to work.  The package offers support for breqn and i=
=73 part
=20of the bundle of the same name.")
=20    (license license:lppl1.3c+)))
=2B
=2B(define-public texlive-flexisym
=2B  (package
=2B    (inherit (simple-texlive-package
=2B              "texlive-flexisym"
=2B              (list "/tex/latex/breqn/flexisym.sty"
=2B                    "/tex/latex/breqn/cmbase.sym"
=2B                    "/tex/latex/breqn/mathpazo.sym"
=2B                    "/tex/latex/breqn/mathptmx.sym"
=2B                    "/tex/latex/breqn/msabm.sym"
=2B                    "/doc/latex/breqn/flexisym.pdf")
=2B              (base32 "0vjhk94s7z83wcb38ww5nzbjywvybfwm6vg7a2yy8ic2sjm0p=
=6Axj")
=2B              #:trivial? #t))
=2B    (propagated-inputs `(("texlive-latex-l3kernel" ,texlive-latex-l3kern=
=65l)
=2B                         ("texlive-mathstyle" ,texlive-mathstyle)))
=2B    (home-page "https://www.ctan.org/pkg/flexisym")
=2B    (synopsis "Symbol manipulation for breqn")
=2B    (description "Flexisym converts mathematical symbol definitions to t=
=68e form
=2Bthey need for breqn to work.  The package offers support for breqn and i=
=73 part
=2Bof the bundle of the same name.")
=2B    (license license:lppl1.3c+)))
=2D-=20
=32.26.2
=0A=

------_=_4472d14409cc91f020ddb2ab_=_
Content-Disposition: attachment; filename=0003-gnu-Add-texlive-breqn.patch
Content-Type: text/x-patch
Content-Transfer-Encoding: quoted-printable

=46rom aca179c3100bced9438c91dc25a1cafe9a9814bd Mon Sep 17 00:00:00 2001
=46rom: "B. Wilson" <elaexuotee@wilsonb.com>
=44ate: Mon, 11 May 2020 20:05:58 +0900
=53ubject: [PATCH 3/7] gnu: Add texlive-breqn.
=54o: guix-patches@gnu.org
=0A* gnu/packages/tex.scm (texlive-breqn): New variable.
=2D--
=20gnu/packages/tex.scm | 28 ++++++++++++++++++++++++++++
=201 file changed, 28 insertions(+)
=0Adiff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scm
=69ndex 6727a2c985..710ad2ba20 100644
=2D-- a/gnu/packages/tex.scm
=2B++ b/gnu/packages/tex.scm
=40@ -7360,3 +7360,31 @@ of the bundle of the same name.")
=20they need for breqn to work.  The package offers support for breqn and i=
=73 part
=20of the bundle of the same name.")
=20    (license license:lppl1.3c+)))
=2B
=2B(define-public texlive-breqn
=2B  (package
=2B    (inherit (simple-texlive-package
=2B              "texlive-breqn"
=2B              (list "/tex/latex/breqn/breqn.sty"
=2B                    "/doc/latex/breqn/breqn.pdf")
=2B              (base32 "0mdm3yyimr8fv8pg2b2zv62fjbx98xy60a3dzj55djdir6hyx=
=666h")
=2B              #:trivial? #t))
=2B    (propagated-inputs `(("texlive-latex-amsmath" ,texlive-latex-amsmath=
=29
=2B                         ("texlive-flexisym" ,texlive-flexisym)
=2B                         ("texlive-latex-graphics" ,texlive-latex-graphi=
=63s)
=2B                         ("texlive-latex-l3kernel" ,texlive-latex-l3kern=
=65l)
=2B                         ("texlive-latex-tools" ,texlive-latex-tools)))
=2B    (home-page "http://wspr.io/breqn/")
=2B    (synopsis "Automated line breaking of displayed equations")
=2B    (description "The package provides solutions to a number of common
=2Bdifficulties in writing displayed equations and getting high-quality out=
=70ut.
=2BFor example, it is a well-known inconvenience that if an equation must b=
=65
=2Bbroken into more than one line, @code{left...right} constructs cannot sp=
=61n
=2Blines.  The breqn package makes them work as one would expect whether or=
=20not
=2Bthere is an intervening line break.  The single most ambitious goal of t=
=68e
=2Bpackage, however, is to support automatic linebreaking of displayed equa=
=74ions.
=2BSuch linebreaking cannot be done without substantial changes under the h=
=6Fod in
=2Bthe way formulae are processed; the code must be watched carefully, keep=
=69ng an
=2Beye on possible glitches.  The bundle also contains the flexisym and mat=
=68style
=2Bpackages, which are both designated as support for breqn.")
=2B    (license license:lppl1.3c+)))
=2D-=20
=32.26.2
=0A=

------_=_4472d14409cc91f020ddb2ab_=_
Content-Disposition: attachment; filename=0004-gnu-Add-texlive-makecell.patch
Content-Type: text/x-patch
Content-Transfer-Encoding: quoted-printable

=46rom f3298a40c3fe945c9dc0cbfc3f9a7fa9bfb73cb8 Mon Sep 17 00:00:00 2001
=46rom: "B. Wilson" <elaexuotee@wilsonb.com>
=44ate: Mon, 11 May 2020 20:07:03 +0900
=53ubject: [PATCH 4/7] gnu: Add texlive-makecell.
=54o: guix-patches@gnu.org
=0A* gnu/packages/tex.scm (texlive-makecell): New variable.
=2D--
=20gnu/packages/tex.scm | 29 +++++++++++++++++++++++++++++
=201 file changed, 29 insertions(+)
=0Adiff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scm
=69ndex 710ad2ba20..ca5b9dbb2e 100644
=2D-- a/gnu/packages/tex.scm
=2B++ b/gnu/packages/tex.scm
=40@ -7388,3 +7388,32 @@ the way formulae are processed; the code must be w=
=61tched carefully, keeping an
=20eye on possible glitches.  The bundle also contains the flexisym and mat=
=68style
=20packages, which are both designated as support for breqn.")
=20    (license license:lppl1.3c+)))
=2B
=2B(define-public texlive-makecell
=2B  (package
=2B    (inherit (simple-texlive-package
=2B              "texlive-makecell"
=2B              (list "/tex/latex/makecell/"
=2B                    "/doc/latex/makecell/makecell.pdf")
=2B              (base32 "1zdcmya5dxrnjf7lf0wmnhcjlwdha5gdzdx7xrgyi61gqwj7c=
=78in")
=2B              #:trivial? #t))
=2B    (propagated-inputs `(("texlive-latex-tools" ,texlive-latex-tools)))
=2B    (home-page "https://www.ctan.org/pkg/makecell")
=2B    (synopsis "Tabular column heads and multilined cells")
=2B    (description "This package supports common layouts for tabular colum=
=6E heads
=2Bin whole documents, based on one-column tabular environment.  In additio=
=6E, it
=2Bcan create multi-lined tabular cells.
=2B
=2BThe Package also offers:
=2B
=2B@itemize
=2B@item a macro which changes the vertical space around all the cells in a=
=0A+      tabular environment (similar to the function of the tabls package=
=2C but
=2B      using the facilities of the array);
=2B@item macros for multirow cells, which use the facilities of the multiro=
=77
=2B      package;
=2B@item macros to number rows in tables, or to skip cells;
=2B@item diagonally divided cells;
=2B@item horizontal lines in tabular environments with defined thickness.
=2B@end itemize")
=2B    (license license:lppl)))
=2D-=20
=32.26.2
=0A=

------_=_4472d14409cc91f020ddb2ab_=_
Content-Disposition: attachment; filename=0005-gnu-Add-texlive-microtype.patch
Content-Type: text/x-patch
Content-Transfer-Encoding: quoted-printable

=46rom c03dc294ea70b4fe210f038ff14945d0005228c3 Mon Sep 17 00:00:00 2001
=46rom: "B. Wilson" <elaexuotee@wilsonb.com>
=44ate: Mon, 11 May 2020 20:08:10 +0900
=53ubject: [PATCH 5/7] gnu: Add texlive-microtype.
=54o: guix-patches@gnu.org
=0A* gnu/packages/tex.scm (texlive-microtype): New variable.
=2D--
=20gnu/packages/tex.scm | 34 ++++++++++++++++++++++++++++++++++
=201 file changed, 34 insertions(+)
=0Adiff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scm
=69ndex ca5b9dbb2e..2d290fdb82 100644
=2D-- a/gnu/packages/tex.scm
=2B++ b/gnu/packages/tex.scm
=40@ -7417,3 +7417,37 @@ The Package also offers:
=20@item horizontal lines in tabular environments with defined thickness.
=20@end itemize")
=20    (license license:lppl)))
=2B
=2B(define-public texlive-microtype
=2B  (package
=2B    (inherit (simple-texlive-package
=2B              "texlive-microtype"
=2B              (list "/tex/latex/microtype/"
=2B                    "/doc/latex/microtype/")
=2B              (base32 "0xmjpzbj4nqmnl5m7xx1bshdk2c8n57rmbvn0j479ypj4wdlq=
=39iy")
=2B              #:trivial? #t))
=2B    (propagated-inputs `(("texlive-latex-graphics" ,texlive-latex-graphi=
=63s)))
=2B    (home-page "https://www.ctan.org/pkg/microtype")
=2B    (synopsis "Subliminal refinements towards typographical perfection")=
=0A+    (description "The package provides a LaTeX interface to the
=2Bmicro-typographic extensions that were introduced by pdfTeX and have sin=
=63e also
=2Bpropagated to XeTeX and LuaTeX: most prominently, character protrusion a=
=6Ed font
=2Bexpansion, furthermore the adjustment of interword spacing and additiona=
=6C
=2Bkerning, as well as hyphenatable letterspacing (tracking) and the possib=
=69lity
=2Bto disable all or selected ligatures.
=2B
=2BThese features may be applied to customisable sets of fonts, and all
=2Bmicro-typographic aspects of the fonts can be configured in a straight-f=
=6Frward
=2Band flexible way.  Settings for various fonts are provided.
=2B
=2BNote that character protrusion requires pdfTeX, LuaTeX, or XeTeX.  Font
=2Bexpansion works with pdfTeX or LuaTeX.  The package will by default enab=
=6Ce
=2Bprotrusion and expansion if they can safely be assumed to work.  Disabli=
=6Eg
=2Bligatures requires pdfTeX or LuaTeX, while the adjustment of interword s=
=70acing
=2Band of kerning only works with pdfTeX.  Letterspacing is available with =
=70dfTeX
=2Bor LuaTeX.
=2B
=2BThe alternative package @code{letterspace}, which also works with plain =
=54eX,
=2Bprovides the user commands for letterspacing only, omitting support for =
=61ll
=2Bother extensions.")
=2B    (license license:lppl1.3c+)))
=2D-=20
=32.26.2
=0A=

------_=_4472d14409cc91f020ddb2ab_=_
Content-Disposition: attachment; filename=0006-gnu-Add-texlive-tabu.patch
Content-Type: text/x-patch
Content-Transfer-Encoding: quoted-printable

=46rom 01ce7a13c2897263e754bb8164c2472bc683d6bf Mon Sep 17 00:00:00 2001
=46rom: "B. Wilson" <elaexuotee@wilsonb.com>
=44ate: Mon, 11 May 2020 20:09:31 +0900
=53ubject: [PATCH 6/7] gnu: Add texlive-tabu.
=54o: guix-patches@gnu.org
=0A* gnu/packages/tex.scm (texlive-tabu): New variable.
=2D--
=20gnu/packages/tex.scm | 39 +++++++++++++++++++++++++++++++++++++++
=201 file changed, 39 insertions(+)
=0Adiff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scm
=69ndex 2d290fdb82..f382330773 100644
=2D-- a/gnu/packages/tex.scm
=2B++ b/gnu/packages/tex.scm
=40@ -7451,3 +7451,42 @@ The alternative package @code{letterspace}, which =
=61lso works with plain TeX,
=20provides the user commands for letterspacing only, omitting support for =
=61ll
=20other extensions.")
=20    (license license:lppl1.3c+)))
=2B
=2B(define-public texlive-tabu
=2B  (package
=2B    (inherit (simple-texlive-package
=2B              "texlive-tabu"
=2B              (list "/tex/latex/tabu/"
=2B                    "/doc/latex/tabu/")
=2B              (base32 "156lkisyrpvn82ng2kxdlly60ny5vaz4lp9xlc66azy5ma06a=
=67vw")
=2B              #:trivial? #t))
=2B    (propagated-inputs
=2B     `(("texlive-latex-tools" ,texlive-latex-tools)
=2B       ("texlive-latex-varwidth" ,texlive-latex-varwidth)))
=2B    (home-page "https://www.ctan.org/pkg/tabu")
=2B    (synopsis "Flexible LaTeX tabulars")
=2B    (description "The package provides an environment, @code{tabu}, whic=
=68 will
=2Bmake any sort of tabular (that doesn=E2=80=99t need to split across page=
=73), and an
=2Benvironment @code{longtabu} which provides the facilities of @code{tabu}=
=20in a
=2Bmodified longtable environment.  (Note that this latter offers an enhanc=
=65ment
=2Bof ltxtable.)
=2B
=2BThe package requires the array package, and needs e-TeX to run (since ar=
=72ay.sty
=2Bis present in every conforming distribution of LaTeX, and since every pu=
=62licly
=2Bavailable LaTeX format is built using e-TeX, the requirements are provid=
=65d by
=2Bdefault on any reasonable system).  The package also requires xcolor for=
=0A+coloured rules in tables, and colortbl for coloured cells.  The @code{l=
=6Fngtabu}
=2Benvironment further requires that longtable be loaded.  The package itse=
=6Cf does
=2Bnot load any of these packages for the user.
=2B
=2BThe @code{tabu} environment may be used in place of @code{tabular},
=2B@code{tabular*} and @code{tabularx} environments, as well as the @code{a=
=72ray}
=2Benvironment in maths mode.  It overloads @code{tabularx}=E2=80=99s X-col=
=75mn
=2Bspecification, allowing a width specification, alignment (@code{l}, @cod=
=65{r},
=2B@code{c} and @code{j}) and column type indication (@code{p}, @code{m} an=
=64
=2B@code{b}).
=2B
=2B@code{\begin@{tabu@}} to @code{<dimen>} specifies a target width, and
=2B@code{\begin@{tabu@}} spread @code{<dimen>} enlarges the environment=
=E2=80=99s
=2Bnatural width.")
=2B    (license license:lppl1.3c+)))
=2D-=20
=32.26.2
=0A=

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

=46rom 7fd676d14283204b9f367d301293af339c8906a1 Mon Sep 17 00:00:00 2001
=46rom: "B. Wilson" <elaexuotee@wilsonb.com>
=44ate: Mon, 11 May 2020 20:10:48 +0900
=53ubject: [PATCH 7/7] gnu: Add metamath.
=54o: guix-patches@gnu.org
=0A* gnu/packages/maths.scm (metamath): New variable.
=2D--
=20gnu/packages/maths.scm | 74 ++++++++++++++++++++++++++++++++++++++++++
=201 file changed, 74 insertions(+)
=0Adiff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
=69ndex 8fbce15418..2054e1ad8e 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@ -5615,3 +5616,76 @@ 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"))=
=29)
=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 ((docdir (assoc-ref outputs "doc")))
=2B                 (install-file
=2B                  (string-append book-builddir "/metamath.pdf")
=2B                  (string-append docdir "/share/doc/metamath"))
=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=

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


Jakub K=C4=85dzio=C5=82ka <kuba@kadziolka.net> wrote:
> On Mon, Apr 27, 2020 at 01:21:03PM +0900, x@wilsonb.com wrote:
> > > > +(define-public metamath
> > > > +  (package
> > > > +    (name "metamath")
> > > > +    (version "0.182")
> > > > +    (source
> > > > +     (origin
> > > > +       (method url-fetch)
> > > > +       (uri "http://us2.metamath.org/downloads/metamath-program.zi=
p")
> > >=20
> > > This looks like an unversioned URL. That's not ideal, since when
> > > upstream will release a new version, it will break the hash below. I
> > > looked around on their website and couldn't find a versioned URL, but=
 I
> > > also couldn't find the one you're using. We could fetch from GitHub
> > > instead...
> >=20
> > This is a long story.
> >=20
> > The official tar linked on upstream's homepage is also unversioned and =
gets
> > updated daily via some automatic script. The reason being that they als=
o
> > provide snapshots of the databases from the set.mm repository.
> >=20
> > To boot, the GitHub repository (https://github.com/metamath/metamath-ex=
e) only
> > contains a single, outdated release tar, which is simply a spurious byp=
roduct
> > of a prolonged discussion I had with upstream regarding the problems th=
eir
> > release tars pose for package maintainers.
>=20
> I notice, though, that the commits in the repository are up to date. We
> could pin a specific commit ID. This practice is relatively common in
> Guix and does not pose a problem.
>=20
> Regards,
> Jakub K=C4=85dzio=C5=82ka



------_=_4472d14409cc91f020ddb2ab_=_--

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

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

iI0EABYIADUWIQQ7FdZn/PDWvxE6cmR2pStZ7i7CgQUCXrk2JhccZWxhZXh1b3Rl
ZUB3aWxzb25iLmNvbQAKCRB2pStZ7i7CgcGWAPwMgFVykVHZwIk/HallMco66hG4
5WX4jWPQRkUH3usrPgD/ZDq1R5XcYq1OyeyqytaKJSYrEI2Wi7lnIOtSFzBd2gg=
=znPr
-----END PGP SIGNATURE-----

------_=_0a1b9dd2691359a86d6aaff6_=_--