From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp0 ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms11 with LMTPS id eNqyNoI2uV41SQAA0tVLHw (envelope-from ) for ; 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 ) for ; 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 ; 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 ) 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 ) 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 ) 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 ) 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" Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 11 May 2020 11:27:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 40815 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: To: Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= 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 ) 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 ) 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 ) 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 ) 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: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: "Guix-patches" Reply-to: "B. Wilson" , "B. Wilson via Guix-patches" From: "B. Wilson via Guix-patches" via X-Scanner: scn0 X-Spam-Score: -2.11 Authentication-Results: aspmx1.migadu.com; dkim=fail (rsa verify failed) header.d=mg.wilsonb.com header.s=krs header.b=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" =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 = =0A ;;; Copyright =C2=A9 2018 Arun Isaac =20;;; Copyright =C2=A9 2020 Vincent Legoll =2B;;; Copyright =C2=A9 2020 B. Wilson =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" =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" =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" =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" =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" =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{} specifies a target width, and =2B@code{\begin@{tabu@}} spread @code{} 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" =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 =20;;; Copyright =C2=A9 2020 Vincent Legoll =20;;; Copyright =C2=A9 2020 Nicol=C3=B2 Balzarotti =2B;;; Copyright =C2=A9 2020 B. Wilson =20;;; =20;;; This file is part of GNU Guix. =20;;; =40@ -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 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_=_--