GNU bug report logs - #40815
gnu: Add metamath

Please note: This is a static page, with minimal formatting, updated once a day.
Click here to see this page with the latest information and nicer formatting.

Package: guix-patches; Reported by: "B. Wilson" <elaexuotee@HIDDEN>; dated Fri, 24 Apr 2020 11:55:01 UTC; Maintainer for guix-patches is guix-patches@HIDDEN.

Message received at submit <at> debbugs.gnu.org:


Received: (at submit) by debbugs.gnu.org; 11 May 2020 11:26:26 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon May 11 07:26:26 2020
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 <at> debbugs.gnu.org>)
	id 1jY6Zf-0004mt-25
	for submit <at> 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@HIDDEN>)
 id 1jY6ZS-0004mK-Oc
 for submit <at> 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@HIDDEN>)
 id 1jY6ZS-0000hY-IK
 for guix-patches@HIDDEN; 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@HIDDEN>)
 id 1jY6ZP-0004mQ-La
 for guix-patches@HIDDEN; 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
To: Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= <kuba@HIDDEN>
Subject: Re: gnu: Add metamath
From: "B. Wilson" <elaexuotee@HIDDEN>
References: <3JR2ES0G0DYM2.3NI13ZSG185CK@HIDDEN>
 <20200426172945.7ez6i2fl3pjcoexd@gravity>
 <2RKLUI9248WBS.24Y0W3OIHXG53@HIDDEN>
 <20200427121248.cga7p43flnusf7zo@gravity>
In-Reply-To: <20200427121248.cga7p43flnusf7zo@gravity>
Message-Id: <3S4EBJJJJ806M.2BHUR2A6GTXWM@HIDDEN>
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@HIDDEN;
 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-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
 has NOT identified this incoming email as spam.  The original
 message has been attached to this so you can view it or label
 similar future email.  If you have any questions, see
 the administrator of that system for details.
 Content preview:  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. 
 Content analysis details:   (2.8 points, 10.0 required)
 pts rule name              description
 ---- ---------------------- --------------------------------------------------
 0.0 URIBL_BLOCKED          ADMINISTRATOR NOTICE: The query to URIBL was
 blocked.  See
 http://wiki.apache.org/spamassassin/DnsBlocklists#dnsbl-block
 for more information. [URIs: wilsonb.com]
 1.8 PDS_OTHER_BAD_TLD      Untrustworthy TLDs
 [URI: nixo.xyz (xyz)]
 1.0 SPF_SOFTFAIL           SPF: sender does not match SPF record (softfail)
 0.0 SPF_HELO_NONE          SPF: HELO does not publish an SPF Record
 -0.0 RCVD_IN_MSPIKE_H2      RBL: Average reputation (+2)
 [209.51.188.17 listed in wl.mailspike.net]
X-Debbugs-Envelope-To: submit
Cc: guix-patches@HIDDEN
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: 1.8 (+)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
 has NOT identified this incoming email as spam.  The original
 message has been attached to this so you can view it or label
 similar future email.  If you have any questions, see
 the administrator of that system for details.
 
 Content preview:  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. 
 
 Content analysis details:   (1.8 points, 10.0 required)
 
  pts rule name              description
 ---- ---------------------- --------------------------------------------------
  0.0 URIBL_BLOCKED          ADMINISTRATOR NOTICE: The query to URIBL was
                             blocked.  See
                             http://wiki.apache.org/spamassassin/DnsBlocklists#dnsbl-block
                              for more information.
                             [URIs: wspr.io]
  1.8 PDS_OTHER_BAD_TLD      Untrustworthy TLDs
                             [URI: nixo.xyz (xyz)]
  1.0 SPF_SOFTFAIL           SPF: sender does not match SPF record (softfail)
  0.0 SPF_HELO_NONE          SPF: HELO does not publish an SPF Record
 -1.0 MAILING_LIST_MULTI     Multiple indicators imply a widely-seen list
                             manager

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@HIDDEN>
=44ate: Mon, 11 May 2020 20:02:41 +0900
=53ubject: [PATCH 1/7] gnu: Add texlive-mathstyle.
=54o: guix-patches@HIDDEN
=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@HIDDEN>=
=0A ;;; Copyright =C2=A9 2018 Arun Isaac <arunisaac@HIDDEN>
=20;;; Copyright =C2=A9 2020 Vincent Legoll <vincent.legoll@HIDDEN>
=2B;;; Copyright =C2=A9 2020 B. Wilson <elaexuotee@HIDDEN>
=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@HIDDEN>
=44ate: Mon, 11 May 2020 20:03:54 +0900
=53ubject: [PATCH 2/7] gnu: Add texlive-flexisym.
=54o: guix-patches@HIDDEN
=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@HIDDEN>
=44ate: Mon, 11 May 2020 20:05:58 +0900
=53ubject: [PATCH 3/7] gnu: Add texlive-breqn.
=54o: guix-patches@HIDDEN
=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@HIDDEN>
=44ate: Mon, 11 May 2020 20:07:03 +0900
=53ubject: [PATCH 4/7] gnu: Add texlive-makecell.
=54o: guix-patches@HIDDEN
=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@HIDDEN>
=44ate: Mon, 11 May 2020 20:08:10 +0900
=53ubject: [PATCH 5/7] gnu: Add texlive-microtype.
=54o: guix-patches@HIDDEN
=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@HIDDEN>
=44ate: Mon, 11 May 2020 20:09:31 +0900
=53ubject: [PATCH 6/7] gnu: Add texlive-tabu.
=54o: guix-patches@HIDDEN
=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@HIDDEN>
=44ate: Mon, 11 May 2020 20:10:48 +0900
=53ubject: [PATCH 7/7] gnu: Add metamath.
=54o: guix-patches@HIDDEN
=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@HIDDEN>
=20;;; Copyright =C2=A9 2020 Vincent Legoll <vincent.legoll@HIDDEN>
=20;;; Copyright =C2=A9 2020 Nicol=C3=B2 Balzarotti <nicolo@HIDDEN>
=2B;;; Copyright =C2=A9 2020 B. Wilson <elaexuotee@HIDDEN>
=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@HIDDEN> wrote:
> On Mon, Apr 27, 2020 at 01:21:03PM +0900, x@HIDDEN 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_=_--




Information forwarded to guix-patches@HIDDEN:
bug#40815; Package guix-patches. Full text available.

Message received at submit <at> debbugs.gnu.org:


Received: (at submit) by debbugs.gnu.org; 27 Apr 2020 12:13:02 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Apr 27 08:13:02 2020
Received: from localhost ([127.0.0.1]:35800 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1jT2dB-000886-NH
	for submit <at> debbugs.gnu.org; Mon, 27 Apr 2020 08:13:01 -0400
Received: from lists.gnu.org ([209.51.188.17]:60856)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <kuba@HIDDEN>) id 1jT2dA-00087w-I1
 for submit <at> debbugs.gnu.org; Mon, 27 Apr 2020 08:13:00 -0400
Received: from eggs.gnu.org ([2001:470:142:3::10]:34606)
 by lists.gnu.org with esmtp (Exim 4.90_1)
 (envelope-from <kuba@HIDDEN>) id 1jT2d9-0000iy-JT
 for guix-patches@HIDDEN; Mon, 27 Apr 2020 08:13:00 -0400
X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on eggs.gnu.org
X-Spam-Level: 
X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00, FROM_EXCESS_BASE64, 
 SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no
 version=3.4.2
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.90_1)
 (envelope-from <kuba@HIDDEN>) id 1jT2d3-0007yX-VI
 for guix-patches@HIDDEN; Mon, 27 Apr 2020 08:12:59 -0400
Received: from pat.zlotemysli.pl ([37.59.186.212]:59034)
 by eggs.gnu.org with esmtp (Exim 4.90_1)
 (envelope-from <kuba@HIDDEN>) id 1jT2d3-0007v4-BF
 for guix-patches@HIDDEN; Mon, 27 Apr 2020 08:12:53 -0400
Received: (qmail 31266 invoked by uid 1009); 27 Apr 2020 14:12:50 +0200
Received: from 188.123.215.55 (kuba@HIDDEN@188.123.215.55) by pat
 (envelope-from <kuba@HIDDEN>, uid 1002) with qmail-scanner-2.08st 
 (clamdscan: 0.98.6/25794. spamassassin: 3.4.0. perlscan: 2.08st.  
 Clear:RC:1(188.123.215.55):. 
 Processed in 0.027118 secs); 27 Apr 2020 12:12:50 -0000
Received: from unknown (HELO gravity) (kuba@HIDDEN@188.123.215.55)
 by pat.zlotemysli.pl with SMTP; 27 Apr 2020 14:12:50 +0200
Date: Mon, 27 Apr 2020 14:12:48 +0200
From: Jakub =?utf-8?B?S8SFZHppb8WCa2E=?= <kuba@HIDDEN>
To: x@HIDDEN
Subject: Re: gnu: Add metamath
Message-ID: <20200427121248.cga7p43flnusf7zo@gravity>
References: <3JR2ES0G0DYM2.3NI13ZSG185CK@HIDDEN>
 <20200426172945.7ez6i2fl3pjcoexd@gravity>
 <2RKLUI9248WBS.24Y0W3OIHXG53@HIDDEN>
MIME-Version: 1.0
Content-Type: multipart/signed; micalg=pgp-sha256;
 protocol="application/pgp-signature"; boundary="4hmaoeel7hlxin4v"
Content-Disposition: inline
In-Reply-To: <2RKLUI9248WBS.24Y0W3OIHXG53@HIDDEN>
Received-SPF: none client-ip=37.59.186.212; envelope-from=kuba@HIDDEN;
 helo=pat.zlotemysli.pl
X-detected-operating-system: by eggs.gnu.org: First seen = 2020/04/27 08:12:51
X-ACL-Warn: Detected OS   = Linux 3.1-3.10
X-Received-From: 37.59.186.212
X-Spam-Score: -2.3 (--)
X-Debbugs-Envelope-To: submit
Cc: "B. Wilson" <elaexuotee@HIDDEN>, guix-patches@HIDDEN
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -3.3 (---)


--4hmaoeel7hlxin4v
Content-Type: text/plain; charset=utf-8
Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable

On Mon, Apr 27, 2020 at 01:21:03PM +0900, x@HIDDEN wrote:
> > > +(define-public metamath
> > > +  (package
> > > +    (name "metamath")
> > > +    (version "0.182")
> > > +    (source
> > > +     (origin
> > > +       (method url-fetch)
> > > +       (uri "http://us2.metamath.org/downloads/metamath-program.zip")
> >=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 ge=
ts
> updated daily via some automatic script. The reason being that they also
> provide snapshots of the databases from the set.mm repository.
>=20
> To boot, the GitHub repository (https://github.com/metamath/metamath-exe)=
 only
> contains a single, outdated release tar, which is simply a spurious bypro=
duct
> of a prolonged discussion I had with upstream regarding the problems their
> release tars pose for package maintainers.

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.

Regards,
Jakub K=C4=85dzio=C5=82ka

--4hmaoeel7hlxin4v
Content-Type: application/pgp-signature; name="signature.asc"

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

iQIzBAABCAAdFiEE5Xa/ss9usT31cTO54xWnWEYTFWQFAl6mzDoACgkQ4xWnWEYT
FWSMcA//ZY1G0QDy9ZPMdTqUxb6HO2bgd20g44sU8nRZXkQYKkLCuCGpu3we4zbz
vt5F1CprCZh6GkdGfZi6ROj/o42C+hW8R1uRg4Q2gWNFq1NaqyL/ie5SWL0Xoa9g
U0ClJZnwK9a2dEDbEj5X6dZJUzSLBBmv9l4Dm5Sr14w0ijovZmI8vz6IGlJ8fZoE
z7TMOz/XgEgGg7OMmjok9Q0FrS36xKmkiak+BNC9t1ozMbHfVI3XNKn3ba4tmktB
wyCtOSKJ5T+gv5myAtIlxJn3dseOHX9T+TuUKAyYFLTwdantdNvWDMuIOy9eE4A3
xTHbhTNYzAwu+WAgY5Pg6OtqUNnFfN5qb0JqEQFChUW/dY27/INdA+kgMhSdat34
L1dKGobUs22cWPxrQN1JpuxMVVB7YZC48/B/O6JYC3VhS3h7Lwt+Pl9IhHM0XEUo
V2hRTzrHl3J5AflC7uVFLlGxqW/fF7yHVXd2ip9koXIayj52OzyBZnc1VIXdHYX0
GB/7dS/nX7bqFQ0Eoz4nsvTmFbJkObEPKJLjY5ITRjH0EWle0NuDNUiIt1Ul1L79
9tED8iRFbIpxGsgtS3keaK0SxcNO4dWxeFMflk8XvnEc7smqGj5uKzS5888h80ta
2EAvxC2vMt4VxtRSJ6w5BKVls7diIn9/yons4OD4zv4atan91hM=
=f/wi
-----END PGP SIGNATURE-----

--4hmaoeel7hlxin4v--




Information forwarded to guix-patches@HIDDEN:
bug#40815; Package guix-patches. Full text available.

Message received at submit <at> debbugs.gnu.org:


Received: (at submit) by debbugs.gnu.org; 27 Apr 2020 04:43:31 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Apr 27 00:43:31 2020
Received: from localhost ([127.0.0.1]:35339 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1jSvcA-0002sC-QH
	for submit <at> debbugs.gnu.org; Mon, 27 Apr 2020 00:43:31 -0400
Received: from lists.gnu.org ([209.51.188.17]:43876)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <bounce+686de0.08547a-guix-patches=gnu.org@HIDDEN>)
 id 1jSvH4-0002Mq-CG
 for submit <at> debbugs.gnu.org; Mon, 27 Apr 2020 00:21:51 -0400
Received: from eggs.gnu.org ([2001:470:142:3::10]:48408)
 by lists.gnu.org with esmtp (Exim 4.90_1)
 (envelope-from <bounce+686de0.08547a-guix-patches=gnu.org@HIDDEN>)
 id 1jSvH0-0003Ez-7D
 for guix-patches@HIDDEN; Mon, 27 Apr 2020 00:21:42 -0400
X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on eggs.gnu.org
X-Spam-Level: 
X-Spam-Status: No, score=-2.1 required=5.0 tests=BAYES_00,DKIM_SIGNED,
 DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,RCVD_IN_DNSWL_NONE,SPF_PASS,
 URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.2
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.90_1)
 (envelope-from <bounce+686de0.08547a-guix-patches=gnu.org@HIDDEN>)
 id 1jSvGw-0005qL-Gu
 for guix-patches@HIDDEN; Mon, 27 Apr 2020 00:21:37 -0400
Received: from m42-5.mailgun.net ([69.72.42.5]:30203)
 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@HIDDEN>)
 id 1jSvGv-0005m8-Ur
 for guix-patches@HIDDEN; Mon, 27 Apr 2020 00:21:34 -0400
DKIM-Signature: a=rsa-sha256; v=1; c=relaxed/relaxed; d=mg.wilsonb.com;
 q=dns/txt; 
 s=krs; t=1587961293; h=Content-Type: MIME-Version: Message-Id:
 In-Reply-To: References: From: Subject: Cc: To: Date: Sender;
 bh=qQb9fHjjbVR0TLIG/wntA0v8joKorGVYGQ/KSTbee/k=;
 b=w52RCnRmKdIJgsroaRWuxzOBR60CCMqv/Zre6OUUlEW7NCKvIn4/RXpHBoOr7RfrcsQFDvTP
 ZrqBO3HE4MQeyY3PsAa7EXbMY8kpV/2eh04jrD4iCoNCSdxhknnon7a+ZzOi+OLFeSElURV1
 YKuZxWsfA6iP11zyKN2a1UB68fblwSMvnv9KEAXdM8v1dQXS9/qiHTuGMEJiZLvG/gpEPg4U
 yuJRYm0KRtmAwg9RXA7/hg/HKFqTnmTUi6khvg4rMIIxlOYjx417ISzf9fel2jEfyMWd2enU
 f+14cPaorh1+1m0v4j987kiKiRX8SeiSWhiys7c/BbjxlZvI7MHeGA==
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 5ea65dba.7f059337f5d0-smtp-out-n01;
 Mon, 27 Apr 2020 04:21:14 -0000 (UTC)
Received: from localhost (KD111239210021.au-net.ne.jp [111.239.210.21])
 by wilsonb.com (Postfix) with ESMTPSA id 4AF8DA1A70;
 Mon, 27 Apr 2020 04:21:11 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wilsonb.com;
 s=201703; t=1587961271;
 bh=qQb9fHjjbVR0TLIG/wntA0v8joKorGVYGQ/KSTbee/k=;
 h=Date:To:Cc:Subject:From:References:In-Reply-To:From;
 b=vdqoBgE4F/o3wkCRFKbPR4oAQWiNeO4cRLY3tB3X4mmbb/NsEoeKdgNt0jWcM7jbM
 rMft/Mm4r8RTGGoWa2yzh6cvYetcDoQz2UBEX1i1oG5QlJhG7j7UZEzUaRT49trdzp
 kgCIw9a7vpgRVtGgk+1zAcyBtl0kyKf0HrF0vEZ0ckpgMsxdUv/akHUiQEpOzPVHFH
 NniQaVRgJzA1I9D+H3gVfTCfNu+0oOMVsD7a4+ssJTLYIsYX/10iUJ43XJWCRGb321
 u0YPCVQPkPA9sPiHEv2EuCRHFbtS9/5FVmGWHUbN6KJjeiC73SjA1+x4GqAAEluunu
 sIdGP0vrHtLjzyWsAae8WExaItUpD6rEiQ9AwwWcjB0XXCy5LJIqbyzDhf8VvOVBhZ
 9Clg0im3LiXhPseufSclJjR3kn09rgRUd1GyuK/8vLI2ckJ02MTOPqqGqdk+M8nauN
 du+WnWLHj5fbe+/pkjN8QaKXFR1ogaUPb4p/+qOVOxGyfRt0r4uEE3U2Jg4jP9eKQ1
 JNQZCyVsp56ZCvVwgHbVwVzGrd+TtseScSWBQ7qaUuWrE/9rIYBZj0dQ9SfWi63J0H
 G+mk4umh+ciuvoEV1KC+fE3tBfJtX5Rb10W/EtyKemR5u7jBSl1it5RE9xmaMGYUvd
 u1SEFfLuidPRHHpGRVKys7kU=
Date: Mon, 27 Apr 2020 13:21:03 +0900
To: Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= <kuba@HIDDEN>
Subject: Re: gnu: Add metamath
From: x@HIDDEN
References: <3JR2ES0G0DYM2.3NI13ZSG185CK@HIDDEN>
 <20200426172945.7ez6i2fl3pjcoexd@gravity>
In-Reply-To: <20200426172945.7ez6i2fl3pjcoexd@gravity>
Message-Id: <2RKLUI9248WBS.24Y0W3OIHXG53@HIDDEN>
User-Agent: mblaze/0.5.1
MIME-Version: 1.0
Content-Type: multipart/signed; micalg="pgp-sha1";
 protocol="application/pgp-signature";
 boundary="----_=_066652fb3881ddd546832cb7_=_"
Received-SPF: pass client-ip=69.72.42.5;
 envelope-from=bounce+686de0.08547a-guix-patches=gnu.org@HIDDEN;
 helo=m42-5.mailgun.net
X-detected-operating-system: by eggs.gnu.org: First seen = 2020/04/27 00:21:29
X-ACL-Warn: Detected OS   = Linux 2.2.x-3.x [generic]
X-Received-From: 69.72.42.5
X-Spam-Score: 0.7 (/)
X-Debbugs-Envelope-To: submit
X-Mailman-Approved-At: Mon, 27 Apr 2020 00:43:29 -0400
Cc: "B. Wilson" <elaexuotee@HIDDEN>, guix-patches@HIDDEN
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -0.3 (/)

This is a multipart message in MIME format.

------_=_066652fb3881ddd546832cb7_=_
MIME-Version: 1.0
Content-Type: multipart/mixed; boundary="----_=_4c7ce6301e5de0be6c4a9da4_=_"

This is a multipart message in MIME format.

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

Jakub K=C4=85dzio=C5=82ka <kuba@HIDDEN> wrote:
> On Fri, Apr 24, 2020 at 08:48:30PM +0900, B. Wilson wrote:
> > This is my first packaging attempt, so careful critiques are very
> > welcome.
>=20
> Welcome to Guix, then!

Thanks!

> > diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
> > index 73ee161e81..c70557ef8f 100644
> > --- a/gnu/packages/maths.scm
> > +++ b/gnu/packages/maths.scm
> > @@ -38,6 +38,7 @@
> >  ;;; Copyright =C2=A9 2020 R Veera Kumar <vkor@HIDDEN>
> >  ;;; Copyright =C2=A9 2020 Vincent Legoll <vincent.legoll@HIDDEN>
> >  ;;; Copyright =C2=A9 2020 Nicol=C3=B2 Balzarotti <nicolo@HIDDEN>
> > +;;; Copyright =C2=A9 2020 B. Wilson <elaexuotee@HIDDEN>
>=20
> Huh, we usually don't abbreviate first names. It's fine if you prefer it
> this way, though. (BTW, the LaTeX on your website is broken.)

"B. Wilson" is typically the name I use for public development. If it poses=
 a
problem, I do not mind chosing some other alias.

Also, thank you for taking the time to audit my meagre and severely neglect=
ed
website.

> > +(define-public metamath
> > +  (package
> > +    (name "metamath")
> > +    (version "0.182")
> > +    (source
> > +     (origin
> > +       (method url-fetch)
> > +       (uri "http://us2.metamath.org/downloads/metamath-program.zip")
>=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...

This is a long story.

The official tar linked on upstream's homepage is also unversioned and gets=

updated daily via some automatic script. The reason being that they also
provide snapshots of the databases from the set.mm repository.

To boot, the GitHub repository (https://github.com/metamath/metamath-exe) o=
nly
contains a single, outdated release tar, which is simply a spurious byprodu=
ct
of a prolonged discussion I had with upstream regarding the problems their
release tars pose for package maintainers.

All in all I spent a few weeks discussing the problem, eventually resulting=
 in
the url seen in the patch. IIRC this url did end up on the main homepage, b=
ut
for some reason it seems to be missing now.

There were other technical complications, but the current status is that
upstream is a single developer making a special effort to accomodate us her=
e.
The rest of the (quite small) metamath community mostly just conform's
to the somewhat anachronistic workflow that the developer has in place.

Anyway, I recognize the current status makes packaging problematic and will=

open a dialog with upstream again, but given the background, I am not sure =
how
this will go.

> > The package definition itself is pretty bog standard, apart from how
> > the "doc" output is supplied. Upstream provides the official
> > documentation as a pdf offered separately from the source. I decided
> > to include this as an input and manually copy it over. Upstream does
> > also have a repo with the TeX sources. Would it be better to typset it
> > directly instead?
>=20
> AFAIK, building from source is preferred. grep for texlive-union to see
> how it can be done without pulling in gigabytes of dependencies.
>=20
> The no-versioned-URL problem also applies to the documentation, and
> this would let you solve two problems at once ;)

Thank you. I will look into this.

> > +    (arguments
> > +     `(#:phases
> > +       (modify-phases %standard-phases
> > +         (add-after 'install 'install-doc
> > +           (lambda* (#:key inputs outputs #:allow-other-keys)
> > +             (mkdir-p (string-append (assoc-ref outputs "doc") "/share=
/doc"))
> > +             (copy-file (assoc-ref inputs "book")
> > +                        (string-append (assoc-ref outputs "doc")
> > +                                       "/share/doc/metamath.pdf"))))))=
)
>=20
> Let me cite an excerpt from your build log: ;)
>=20
> ## WARNING: phase `install-doc' returned `#<unspecified>'.  Return values=
 other than #t
> ## are deprecated.  Please migrate this package so that its phase
> ## procedures report errors by raising an exception, and otherwise
> ## always return #t.
>=20
> Also, consider binding the path to the /share/doc directory in a variable=
:
> (let ((docdir (string-append ...)))
>   (mkdir-p docdir)
>   (copy-file (assoc-ref inputs "book")
>              (string-append docdir "/metamath.pdf"))
>   #t)

Ew. I can't believe I missed that warning. Thank you for pointing it out.

Regarding the local bindings, I did notice that pattern used liberally in t=
he
repo. My reasoning for using the forms directly is simply that they only ge=
t
used once. Anyway, my revised patch will include the `let' since that's ind=
eed
more idiomatic.

> > Also, regarding my `install-doc' phase, is the way I copy over the
> > /gnu/store/<hash>-metamath.pdf file reasonable? Unfortunately,
> > `install-file' doesn't allow renaming the destination, so I had to
> > mimic its effect. Is there a better, or more idiomatic way to do this
> > kind of thing?
>=20
> Nothing comes to mind as far as other alternatives for mkdir-p +
> copy-file go.

Thanks. Though it is unlikely to be part of the final patch, as per the abo=
ve
revisions, the confirmation is helpful.

> > diff --git a/gnu/packages/patches/metamath-remove-missing-file-refs.pat=
ch b/gnu/packages/patches/metamath-remove-missing-file-refs.patch
> > new file mode 100644
> > index 0000000000..bc4748de98
> > --- /dev/null
> > +++ b/gnu/packages/patches/metamath-remove-missing-file-refs.patch
>=20
> Make sure to add this new file to gnu/local.mk!
>=20
> > @@ -0,0 +1,17 @@
> > +--- metamath.orig/Makefile.am	2020-01-27 20:43:55.650195602 +0900
> > ++++ metamath/Makefile.am	2020-01-27 20:44:18.876578014 +0900
> > +@@ -36,14 +36,6 @@
> > + 	mmwtex.c \
> > + 	$(noinst_HEADERS)
> > +=20
> > +-dist_pkgdata_DATA =3D \
> > +-	big-unifier.mm \
> > +-	demo0.mm \
> > +-	miu.mm \
> > +-	peano.mm \
> > +-	ql.mm \
> > +-	set.mm
> > +-
> > +=20
> > + EXTRA_DIST =3D \
> > + 	LICENSE.TXT \
>=20
> I suppose your not including the databases is intentional, but the
> reasoning behind that seems not entirely clear to me - wouldn't the
> program be more useful when packaged with its database?

The package fails to build without the patch because the archive doesn't
actually include the files, which are expected to be cloned from the set.mm=

repository. I don't have full insight as to why Makefile.am is like this bu=
t
will try to push the fix to upstream as well.

> Regards,
> Jakub K=C4=85dzio=C5=82ka

Thank you for the thorough review! I will give this package another try.


Cheers,

B. Wilson

------_=_4c7ce6301e5de0be6c4a9da4_=_--

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

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

iQEzBAABCAAdFiEEgkvKaje0gDM2mRnu9Mg1slJBq0oFAl6mXZ0ACgkQ9Mg1slJB
q0pSbAf/SN+gzr0Nc0i7IY9ARkdh1oPWHsGxwnb56yRagqC7YIZj0xS42FmW0GUZ
pvS213gfvgZ5LNEvr6nBpfvbvk9Qo1pqRF6h1VSFr1+E4HIvMrPxiRWLk3zgqMP3
WEGOQX5nbdWSHVFb+7j/WbWVAnHUOXUbmLzB3SQi3QnRA8KMgendfskS9maA4hvP
DMYm+/fG7xQP9o8sPugqerrwatMTSqDtjHeBgd7FtFAyCHAT9XILEzUZqaBBOPLL
B0QqvuHRsEKGlkXH1GVAYrW5MBWWDoiYrQwRTye1hkumexXXczeebXPZ10vVWH5w
52rsK2J9mnKTH9gGLIfeZOU4pf6kZA==
=lU/t
-----END PGP SIGNATURE-----

------_=_066652fb3881ddd546832cb7_=_--




Information forwarded to guix-patches@HIDDEN:
bug#40815; Package guix-patches. Full text available.

Message received at submit <at> debbugs.gnu.org:


Received: (at submit) by debbugs.gnu.org; 26 Apr 2020 17:30:10 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Sun Apr 26 13:30:10 2020
Received: from localhost ([127.0.0.1]:34828 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1jSl6P-0006XV-GM
	for submit <at> debbugs.gnu.org; Sun, 26 Apr 2020 13:30:09 -0400
Received: from lists.gnu.org ([209.51.188.17]:56507)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <kuba@HIDDEN>) id 1jSl6G-0006X1-Gh
 for submit <at> debbugs.gnu.org; Sun, 26 Apr 2020 13:30:00 -0400
Received: from eggs.gnu.org ([2001:470:142:3::10]:58288)
 by lists.gnu.org with esmtp (Exim 4.90_1)
 (envelope-from <kuba@HIDDEN>) id 1jSl6F-0006m2-OQ
 for guix-patches@HIDDEN; Sun, 26 Apr 2020 13:29:52 -0400
X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on eggs.gnu.org
X-Spam-Level: 
X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00, FROM_EXCESS_BASE64, 
 SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no
 version=3.4.2
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.90_1)
 (envelope-from <kuba@HIDDEN>) id 1jSl6E-0007nU-NF
 for guix-patches@HIDDEN; Sun, 26 Apr 2020 13:29:51 -0400
Received: from pat.zlotemysli.pl ([37.59.186.212]:51512)
 by eggs.gnu.org with esmtp (Exim 4.90_1)
 (envelope-from <kuba@HIDDEN>) id 1jSl6E-0007dg-3I
 for guix-patches@HIDDEN; Sun, 26 Apr 2020 13:29:50 -0400
Received: (qmail 32691 invoked by uid 1009); 26 Apr 2020 19:29:47 +0200
Received: from 188.123.215.55 (kuba@HIDDEN@188.123.215.55) by pat
 (envelope-from <kuba@HIDDEN>, uid 1002) with qmail-scanner-2.08st 
 (clamdscan: 0.98.6/25793. spamassassin: 3.4.0. perlscan: 2.08st.  
 Clear:RC:1(188.123.215.55):. 
 Processed in 0.035632 secs); 26 Apr 2020 17:29:47 -0000
Received: from unknown (HELO gravity) (kuba@HIDDEN@188.123.215.55)
 by pat.zlotemysli.pl with SMTP; 26 Apr 2020 19:29:47 +0200
Date: Sun, 26 Apr 2020 19:29:45 +0200
From: Jakub =?utf-8?B?S8SFZHppb8WCa2E=?= <kuba@HIDDEN>
To: "B. Wilson" <elaexuotee@HIDDEN>
Subject: Re: gnu: Add metamath
Message-ID: <20200426172945.7ez6i2fl3pjcoexd@gravity>
References: <3JR2ES0G0DYM2.3NI13ZSG185CK@HIDDEN>
MIME-Version: 1.0
Content-Type: multipart/signed; micalg=pgp-sha256;
 protocol="application/pgp-signature"; boundary="mvry24ynlhbmxf7s"
Content-Disposition: inline
In-Reply-To: <3JR2ES0G0DYM2.3NI13ZSG185CK@HIDDEN>
Received-SPF: none client-ip=37.59.186.212; envelope-from=kuba@HIDDEN;
 helo=pat.zlotemysli.pl
X-detected-operating-system: by eggs.gnu.org: First seen = 2020/04/26 11:59:02
X-ACL-Warn: Detected OS   = Linux 3.1-3.10
X-Received-From: 37.59.186.212
X-Spam-Score: -0.3 (/)
X-Debbugs-Envelope-To: submit
Cc: guix-patches@HIDDEN
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: 1.0 (+)


--mvry24ynlhbmxf7s
Content-Type: text/plain; charset=utf-8
Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable

On Fri, Apr 24, 2020 at 08:48:30PM +0900, B. Wilson wrote:
> This is my first packaging attempt, so careful critiques are very
> welcome.

Welcome to Guix, then!

> diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
> index 73ee161e81..c70557ef8f 100644
> --- a/gnu/packages/maths.scm
> +++ b/gnu/packages/maths.scm
> @@ -38,6 +38,7 @@
>  ;;; Copyright =C2=A9 2020 R Veera Kumar <vkor@HIDDEN>
>  ;;; Copyright =C2=A9 2020 Vincent Legoll <vincent.legoll@HIDDEN>
>  ;;; Copyright =C2=A9 2020 Nicol=C3=B2 Balzarotti <nicolo@HIDDEN>
> +;;; Copyright =C2=A9 2020 B. Wilson <elaexuotee@HIDDEN>

Huh, we usually don't abbreviate first names. It's fine if you prefer it
this way, though. (BTW, the LaTeX on your website is broken.)

> +(define-public metamath
> +  (package
> +    (name "metamath")
> +    (version "0.182")
> +    (source
> +     (origin
> +       (method url-fetch)
> +       (uri "http://us2.metamath.org/downloads/metamath-program.zip")

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...

> The package definition itself is pretty bog standard, apart from how
> the "doc" output is supplied. Upstream provides the official
> documentation as a pdf offered separately from the source. I decided
> to include this as an input and manually copy it over. Upstream does
> also have a repo with the TeX sources. Would it be better to typset it
> directly instead?

AFAIK, building from source is preferred. grep for texlive-union to see
how it can be done without pulling in gigabytes of dependencies.

The no-versioned-URL problem also applies to the documentation, and
this would let you solve two problems at once ;)

> +    (arguments
> +     `(#:phases
> +       (modify-phases %standard-phases
> +         (add-after 'install 'install-doc
> +           (lambda* (#:key inputs outputs #:allow-other-keys)
> +             (mkdir-p (string-append (assoc-ref outputs "doc") "/share/d=
oc"))
> +             (copy-file (assoc-ref inputs "book")
> +                        (string-append (assoc-ref outputs "doc")
> +                                       "/share/doc/metamath.pdf")))))))

Let me cite an excerpt from your build log: ;)

## WARNING: phase `install-doc' returned `#<unspecified>'.  Return values o=
ther than #t
## are deprecated.  Please migrate this package so that its phase
## procedures report errors by raising an exception, and otherwise
## always return #t.

Also, consider binding the path to the /share/doc directory in a variable:
(let ((docdir (string-append ...)))
  (mkdir-p docdir)
  (copy-file (assoc-ref inputs "book")
             (string-append docdir "/metamath.pdf"))
  #t)

> Also, regarding my `install-doc' phase, is the way I copy over the
> /gnu/store/<hash>-metamath.pdf file reasonable? Unfortunately,
> `install-file' doesn't allow renaming the destination, so I had to
> mimic its effect. Is there a better, or more idiomatic way to do this
> kind of thing?

Nothing comes to mind as far as other alternatives for mkdir-p +
copy-file go.

> diff --git a/gnu/packages/patches/metamath-remove-missing-file-refs.patch=
 b/gnu/packages/patches/metamath-remove-missing-file-refs.patch
> new file mode 100644
> index 0000000000..bc4748de98
> --- /dev/null
> +++ b/gnu/packages/patches/metamath-remove-missing-file-refs.patch

Make sure to add this new file to gnu/local.mk!

> @@ -0,0 +1,17 @@
> +--- metamath.orig/Makefile.am	2020-01-27 20:43:55.650195602 +0900
> ++++ metamath/Makefile.am	2020-01-27 20:44:18.876578014 +0900
> +@@ -36,14 +36,6 @@
> + 	mmwtex.c \
> + 	$(noinst_HEADERS)
> +=20
> +-dist_pkgdata_DATA =3D \
> +-	big-unifier.mm \
> +-	demo0.mm \
> +-	miu.mm \
> +-	peano.mm \
> +-	ql.mm \
> +-	set.mm
> +-
> +=20
> + EXTRA_DIST =3D \
> + 	LICENSE.TXT \

I suppose your not including the databases is intentional, but the
reasoning behind that seems not entirely clear to me - wouldn't the
program be more useful when packaged with its database?

Regards,
Jakub K=C4=85dzio=C5=82ka

--mvry24ynlhbmxf7s
Content-Type: application/pgp-signature; name="signature.asc"

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

iQIzBAABCAAdFiEE5Xa/ss9usT31cTO54xWnWEYTFWQFAl6lxQUACgkQ4xWnWEYT
FWTWrQ//YvS+LnMl9qyPMprweSuHNuo3ZitJ4qSwETrk3k7lXaRwW/vtL5+NTZKv
0H/gRNA23yEyfZ9spUNWQPS4Q52vYNtOg24yQFvYjPXUBVHSUzlHSVaQSXwbnIz5
RNY+B5orPum+plPbXxPSopuxXew1QmzSU5mqMxVbl445zlGEAv7j40TyIbnTWT0F
X14mYtu/RPll2EBhxmIu+xXXr963zGsgV8RU+7sb7DzuK0DKFesZW95wZdSu+eIE
Jv6vHxs9Xai33rFbEmz7j3zDKpUL9jTCju2xmvkP1Jl9yUPgKIpmwaPoIz1kiB01
qPTZIYXpekO5FOgaZkBsRS3pxtBLhWARDoEriyZ6LywXtlnLYS0PBqgf1fP386//
Aj8ueSvBR9G5d0JW/4ggtoAPrAUDg9ndhDSs5LGnROIWSKv52HwslBNzc5BA+7Ky
uHxbZG5EVbC7uvDSUtBJ3YAbgydJYCng3OF90UUnpgVKKXF6hTmF+N3jrFHPtiUf
XK0gKETUS2wi6PtX6nWeT5GPSTuGPF0i/MYF6QjdJPnpGkKLezNmMirnvarQNxiu
OH1T+vcbzGJ4xZXPAuKZ4hu4Uq3NNZGYugOT5Mvk5CzdPmAd/AS/jw75lAwUZFYf
+YXHSV8XYZDNfmA376KjikFgvuZCfHoQoYLFj/rQaN5mFS82PPQ=
=q6hC
-----END PGP SIGNATURE-----

--mvry24ynlhbmxf7s--




Information forwarded to guix-patches@HIDDEN:
bug#40815; Package guix-patches. Full text available.

Message received at submit <at> debbugs.gnu.org:


Received: (at submit) by debbugs.gnu.org; 24 Apr 2020 11:54:14 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Fri Apr 24 07:54:14 2020
Received: from localhost ([127.0.0.1]:56598 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1jRwuC-0006gd-PE
	for submit <at> debbugs.gnu.org; Fri, 24 Apr 2020 07:54:14 -0400
Received: from lists.gnu.org ([209.51.188.17]:36377)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <bounce+686de0.08547a-guix-patches=gnu.org@HIDDEN>)
 id 1jRwu2-0006g6-PL
 for submit <at> debbugs.gnu.org; Fri, 24 Apr 2020 07:54:02 -0400
Received: from eggs.gnu.org ([2001:470:142:3::10]:53154)
 by lists.gnu.org with esmtp (Exim 4.90_1)
 (envelope-from <bounce+686de0.08547a-guix-patches=gnu.org@HIDDEN>)
 id 1jRwty-00017X-CH
 for guix-patches@HIDDEN; Fri, 24 Apr 2020 07:53:54 -0400
X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on eggs.gnu.org
X-Spam-Level: 
X-Spam-Status: No, score=-2.1 required=5.0 tests=BAYES_00,DKIM_SIGNED,
 DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,RCVD_IN_DNSWL_NONE,
 RCVD_IN_MSPIKE_H2,SPF_PASS,URIBL_BLOCKED autolearn=unavailable
 autolearn_force=no version=3.4.2
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.90_1)
 (envelope-from <bounce+686de0.08547a-guix-patches=gnu.org@HIDDEN>)
 id 1jRwtx-0007hN-09
 for guix-patches@HIDDEN; Fri, 24 Apr 2020 07:53:49 -0400
Received: from m42-5.mailgun.net ([69.72.42.5]:51083)
 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@HIDDEN>)
 id 1jRwtw-0007ez-DH
 for guix-patches@HIDDEN; Fri, 24 Apr 2020 07:53:48 -0400
DKIM-Signature: a=rsa-sha256; v=1; c=relaxed/relaxed; d=mg.wilsonb.com;
 q=dns/txt; 
 s=krs; t=1587729227; h=Content-Type: MIME-Version: Message-Id: From:
 Subject: To: Date: Sender;
 bh=cXni3pRk8uUxO6ZD16LBh1L8XeiXLk8toumhfwqCafE=;
 b=76y7BqdxDUoi25dbRw+x9kNiODPiOfQAF5G3a2lbM4hQ2pTGyNaMEAaH03lTSWrSaCNTWJrV
 KVLa7TXT/icLN7p7GhGB2YfxDMnLOMZ90zL1FMD/qwHcBB6wPYkdnf2jnx/TKbgFjvrRvcvr
 hLv+PpHIJvfoJASu/VpzRrnSCpa2WjZ2+SYOi3rgeFdE/zAj0Oq1UfqPERoPOvYEtqBsPxa0
 RG4qrtgoTAVITJghn65fa4oUEqfuDDQh4KuEmbGQ3z+mFn6ymh90EWRl1vq5AxoG2Ixt6iWq
 txYYCXppFdWcMkGSlfViMkBiQuFAaJWANmwGxjKCl1KUdyVesbY3jQ==
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 5ea2d21e.7f7eeaee75a0-smtp-out-n05;
 Fri, 24 Apr 2020 11:48:46 -0000 (UTC)
Received: from localhost (KD111239206026.au-net.ne.jp [111.239.206.26])
 by wilsonb.com (Postfix) with ESMTPSA id 4E6B0A1A70
 for <guix-patches@HIDDEN>; Fri, 24 Apr 2020 11:48:42 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wilsonb.com;
 s=201703; t=1587728922;
 bh=cXni3pRk8uUxO6ZD16LBh1L8XeiXLk8toumhfwqCafE=;
 h=Date:To:Subject:From:From;
 b=t1QfKTPl6p/zwRRBuD0W5xBJp2PJ3QQi6ThSZvHTI3TilkjEfzLzwNstsvhx35mLE
 V9sFEXjvBVh5OcRxqjiPMjaAFQP6BBMy8Cuc29OGGANK0LSmoxpWvL48cjR+PPLQ1R
 VNnNft4pWWexOOkyDJZmEvjqJ4JDljd5tWukwNH7uNBH3yW9v9vaCeXqhS0EStClQL
 T7JRp11ZZntaHDmmOoLTGXNSZ2W3MmLXGHANLtaZL9dabFWQtHv9DvHI3vcEALDmAS
 3wyF0x4wDCDFbgj5HxuF9hui/YBRSyYFUGEDdRyUaQC0GIxrsj7Lkc3fkHCDQ038QG
 wginj+5S0oLIUD5ZaceL4gpN/b2/bBx6cAC/Ce3kxUhMCSGAqj7Flh7Nru7oZrk2dl
 Ewed61PniwHwgR0mESUT769JWWITPEfJjsT9aoxL97ZW2y/G8744rYgsdmejc/3ysM
 92JL8nVTAWRCheb8D5uUdrAOvuwibV++9E2MSGGaOsj9pdM0u5EzI3zPXzhJaGebus
 vVKB5lpgCRFbn3X/zCDltgK91LFqbOgGHGwoLKwutqy68gSO8Zz7to6XPELKIMsiOc
 JdeWMs3GaB/Rryj5A2DjMQvn0T5CvCuOApUkOpg8YGHtGUjTp5yJoUhs/GoOCfApxU
 wpCtQxhNYqcKzvjfWSmgedII=
Date: Fri, 24 Apr 2020 20:48:30 +0900
To: guix-patches@HIDDEN
Subject: gnu: Add metamath
From: "B. Wilson" <elaexuotee@HIDDEN>
Message-Id: <3JR2ES0G0DYM2.3NI13ZSG185CK@HIDDEN>
User-Agent: mblaze/0.5.1
MIME-Version: 1.0
Content-Type: multipart/signed; micalg="pgp-sha1";
 protocol="application/pgp-signature";
 boundary="----_=_61af54047ea067b0308e476b_=_"
Received-SPF: pass client-ip=69.72.42.5;
 envelope-from=bounce+686de0.08547a-guix-patches=gnu.org@HIDDEN;
 helo=m42-5.mailgun.net
X-detected-operating-system: by eggs.gnu.org: First seen = 2020/04/24 07:48:46
X-ACL-Warn: Detected OS   = Linux 2.2.x-3.x [generic]
X-Received-From: 69.72.42.5
X-Spam-Score: 2.3 (++)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
 has NOT identified this incoming email as spam.  The original
 message has been attached to this so you can view it or label
 similar future email.  If you have any questions, see
 the administrator of that system for details.
 Content preview:  This is my first packaging attempt, so careful critiques are
 very welcome. The package definition itself is pretty bog standard, apart
 from how the "doc" output is supplied. Upstream provides the official
 documentation
 as a pdf offered separately from the source. I decided t [...] 
 Content analysis details:   (2.3 points, 10.0 required)
 pts rule name              description
 ---- ---------------------- --------------------------------------------------
 0.0 URIBL_BLOCKED          ADMINISTRATOR NOTICE: The query to URIBL was
 blocked.  See
 http://wiki.apache.org/spamassassin/DnsBlocklists#dnsbl-block
 for more information. [URIs: ql.mm]
 0.0 SPF_HELO_NONE          SPF: HELO does not publish an SPF Record
 2.0 PDS_OTHER_BAD_TLD      Untrustworthy TLDs
 [URI: nixo.xyz (xyz)]
 1.0 SPF_SOFTFAIL           SPF: sender does not match SPF record (softfail)
 -0.7 RCVD_IN_DNSWL_LOW      RBL: Sender listed at https://www.dnswl.org/,
 low trust [209.51.188.17 listed in list.dnswl.org]
X-Debbugs-Envelope-To: submit
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: 2.0 (++)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
 has NOT identified this incoming email as spam.  The original
 message has been attached to this so you can view it or label
 similar future email.  If you have any questions, see
 the administrator of that system for details.
 
 Content preview:  This is my first packaging attempt, so careful critiques are
    very welcome. The package definition itself is pretty bog standard, apart
    from how the "doc" output is supplied. Upstream provides the official documentation
    as a pdf offered separately from the source. I decided t [...] 
 
 Content analysis details:   (2.0 points, 10.0 required)
 
  pts rule name              description
 ---- ---------------------- --------------------------------------------------
  0.0 URIBL_BLOCKED          ADMINISTRATOR NOTICE: The query to URIBL was
                             blocked.  See
                             http://wiki.apache.org/spamassassin/DnsBlocklists#dnsbl-block
                              for more information.
                             [URIs: metamath.org]
  0.0 SPF_HELO_NONE          SPF: HELO does not publish an SPF Record
  2.0 PDS_OTHER_BAD_TLD      Untrustworthy TLDs
                             [URI: nixo.xyz (xyz)]
  1.0 SPF_SOFTFAIL           SPF: sender does not match SPF record (softfail)
 -1.0 MAILING_LIST_MULTI     Multiple indicators imply a widely-seen list
                             manager

This is a multipart message in MIME format.

------_=_61af54047ea067b0308e476b_=_
MIME-Version: 1.0
Content-Type: multipart/mixed; boundary="----_=_749b366b4a10e90540d726a7_=_"

This is a multipart message in MIME format.

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


This is my first packaging attempt, so careful critiques are very welcome.

The package definition itself is pretty bog standard, apart from how the "d=
oc" output is supplied. Upstream provides the official documentation as a p=
df offered separately from the source. I decided to include this as an inpu=
t and manually copy it over. Upstream does also have a repo with the TeX so=
urces. Would it be better to typset it directly instead?

Also, regarding my `install-doc' phase, is the way I copy over the /gnu/sto=
re/<hash>-metamath.pdf file reasonable? Unfortunately, `install-file' doesn=
't allow renaming the destination, so I had to mimic its effect. Is there a=
 better, or more idiomatic way to do this kind of thing?

Anyway, cheers and guix!


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

=46rom 808e8d73cb231d2fbf34b88683fb0c3fe5d631e9 Mon Sep 17 00:00:00 2001
=46rom: "B. Wilson" <elaexuotee@HIDDEN>
=44ate: Thu, 23 Apr 2020 20:28:49 +0900
=53ubject: [PATCH] gnu: Add metamath
=0A* gnu/packages/maths.scm (metamath): New variable.
=2A gnu/packages/patches/metamath-remove-missing-file-refs.patch: New file.=
=0A---
=20gnu/packages/maths.scm                        | 45 +++++++++++++++++++
=20.../metamath-remove-missing-file-refs.patch   | 17 +++++++
=202 files changed, 62 insertions(+)
=20create mode 100644 gnu/packages/patches/metamath-remove-missing-file-ref=
=73.patch
=0Adiff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
=69ndex 73ee161e81..c70557ef8f 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@HIDDEN>
=20;;; Copyright =C2=A9 2020 Vincent Legoll <vincent.legoll@HIDDEN>
=20;;; Copyright =C2=A9 2020 Nicol=C3=B2 Balzarotti <nicolo@HIDDEN>
=2B;;; Copyright =C2=A9 2020 B. Wilson <elaexuotee@HIDDEN>
=20;;;
=20;;; This file is part of GNU Guix.
=20;;;
=40@ -5519,3 +5520,47 @@ 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 url-fetch)
=2B       (uri "http://us2.metamath.org/downloads/metamath-program.zip")
=2B       (sha256
=2B        (base32 "0k1ffd1bglkgdb6pkjnxw3dc7p697x70nx8hcpvw9cwbv3k9vf71"))=
=0A+       (patches (search-patches "metamath-remove-missing-file-refs.patc=
=68"))))
=2B    (build-system gnu-build-system)
=2B    (inputs
=2B     `(("book"
=2B        ,(origin
=2B           (method url-fetch)
=2B           (uri "http://us2.metamath.org/downloads/metamath.pdf")
=2B           (sha256
=2B            (base32 "0nc0dz2zk8n2yija8qdvdgnmpqafyfl1nxf3yrr9g2hldnqvlpi=
=34"))))))
=2B    (native-inputs `(("autoconf" ,autoconf)
=2B                     ("automake" ,automake)
=2B                     ("unzip" ,unzip)))
=2B    (outputs '("out" "doc"))
=2B    (arguments
=2B     `(#:phases
=2B       (modify-phases %standard-phases
=2B         (add-after 'install 'install-doc
=2B           (lambda* (#:key inputs outputs #:allow-other-keys)
=2B             (mkdir-p (string-append (assoc-ref outputs "doc") "/share/d=
=6Fc"))
=2B             (copy-file (assoc-ref inputs "book")
=2B                        (string-append (assoc-ref outputs "doc")
=2B                                       "/share/doc/metamath.pdf")))))))
=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+)))
=64iff --git a/gnu/packages/patches/metamath-remove-missing-file-refs.patch=
=20b/gnu/packages/patches/metamath-remove-missing-file-refs.patch
=6Eew file mode 100644
=69ndex 0000000000..bc4748de98
=2D-- /dev/null
=2B++ b/gnu/packages/patches/metamath-remove-missing-file-refs.patch
=40@ -0,0 +1,17 @@
=2B--- metamath.orig/Makefile.am	2020-01-27 20:43:55.650195602 +0900
=2B+++ metamath/Makefile.am	2020-01-27 20:44:18.876578014 +0900
=2B@@ -36,14 +36,6 @@
=2B 	mmwtex.c \
=2B 	$(noinst_HEADERS)
=2B=20
=2B-dist_pkgdata_DATA =3D \
=2B-	big-unifier.mm \
=2B-	demo0.mm \
=2B-	miu.mm \
=2B-	peano.mm \
=2B-	ql.mm \
=2B-	set.mm
=2B-
=2B=20
=2B EXTRA_DIST =3D \
=2B 	LICENSE.TXT \
=2D-=20
=32.26.2
=0A=

------_=_749b366b4a10e90540d726a7_=_--

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

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

iI0EABYIADUWIQQ7FdZn/PDWvxE6cmR2pStZ7i7CgQUCXqLSBxccZWxhZXh1b3Rl
ZUB3aWxzb25iLmNvbQAKCRB2pStZ7i7CgXo7AQDcG/0uGr5EKhqF7g73hwv6QTFe
aad57p6ZOz1BRHG2RQD9FC0Ii+0hVXdRhkO9F76rjeQNLswsmEwO6DYNh8IeZwY=
=MYEL
-----END PGP SIGNATURE-----

------_=_61af54047ea067b0308e476b_=_--




Acknowledgement sent to "B. Wilson" <elaexuotee@HIDDEN>:
New bug report received and forwarded. Copy sent to guix-patches@HIDDEN. Full text available.
Report forwarded to guix-patches@HIDDEN:
bug#40815; Package guix-patches. Full text available.
Please note: This is a static page, with minimal formatting, updated once a day.
Click here to see this page with the latest information and nicer formatting.
Last modified: Mon, 11 May 2020 11:30:02 UTC

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997 nCipher Corporation Ltd, 1994-97 Ian Jackson.