From debbugs-submit-bounces@debbugs.gnu.org Fri Apr 24 07:54:14 2020 Received: (at submit) by debbugs.gnu.org; 24 Apr 2020 11:54:14 +0000 Received: from localhost ([127.0.0.1]:56598 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jRwuC-0006gd-PE for submit@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 ) id 1jRwu2-0006g6-PL for submit@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 ) id 1jRwty-00017X-CH for guix-patches@gnu.org; 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 ) id 1jRwtx-0007hN-09 for guix-patches@gnu.org; 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 ) id 1jRwtw-0007ez-DH for guix-patches@gnu.org; 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 ; 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@gnu.org Subject: gnu: Add metamath From: "B. Wilson" Message-Id: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> 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@mg.wilsonb.com; 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@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" 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/-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" =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 =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@ -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_=_-- From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 26 13:30:10 2020 Received: (at submit) by debbugs.gnu.org; 26 Apr 2020 17:30:10 +0000 Received: from localhost ([127.0.0.1]:34828 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jSl6P-0006XV-GM for submit@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 ) id 1jSl6G-0006X1-Gh for submit@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 ) id 1jSl6F-0006m2-OQ for guix-patches@gnu.org; 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 ) id 1jSl6E-0007nU-NF for guix-patches@gnu.org; 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 ) id 1jSl6E-0007dg-3I for guix-patches@gnu.org; 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@kadziolka.net@188.123.215.55) by pat (envelope-from , 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@kadziolka.net@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=?= To: "B. Wilson" Subject: Re: gnu: Add metamath Message-ID: <20200426172945.7ez6i2fl3pjcoexd@gravity> References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> 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@wilsonb.com> Received-SPF: none client-ip=37.59.186.212; envelope-from=kuba@kadziolka.net; 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@gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" 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 > ;;; Copyright =C2=A9 2020 Vincent Legoll > ;;; Copyright =C2=A9 2020 Nicol=C3=B2 Balzarotti > +;;; Copyright =C2=A9 2020 B. Wilson 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 `#'. 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/-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-- From debbugs-submit-bounces@debbugs.gnu.org Mon Apr 27 00:43:31 2020 Received: (at submit) by debbugs.gnu.org; 27 Apr 2020 04:43:31 +0000 Received: from localhost ([127.0.0.1]:35339 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jSvcA-0002sC-QH for submit@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 ) id 1jSvH4-0002Mq-CG for submit@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 ) id 1jSvH0-0003Ez-7D for guix-patches@gnu.org; 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 ) id 1jSvGw-0005qL-Gu for guix-patches@gnu.org; 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 ) id 1jSvGv-0005m8-Ur for guix-patches@gnu.org; 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?= Subject: Re: gnu: Add metamath From: x@wilsonb.com References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> <20200426172945.7ez6i2fl3pjcoexd@gravity> In-Reply-To: <20200426172945.7ez6i2fl3pjcoexd@gravity> Message-Id: <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com> 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@mg.wilsonb.com; 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" , guix-patches@gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" 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 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 > > ;;; Copyright =C2=A9 2020 Vincent Legoll > > ;;; Copyright =C2=A9 2020 Nicol=C3=B2 Balzarotti > > +;;; Copyright =C2=A9 2020 B. Wilson >=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 `#'. 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/-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_=_-- From debbugs-submit-bounces@debbugs.gnu.org Mon Apr 27 08:13:02 2020 Received: (at submit) by debbugs.gnu.org; 27 Apr 2020 12:13:02 +0000 Received: from localhost ([127.0.0.1]:35800 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jT2dB-000886-NH for submit@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 ) id 1jT2dA-00087w-I1 for submit@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 ) id 1jT2d9-0000iy-JT for guix-patches@gnu.org; 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 ) id 1jT2d3-0007yX-VI for guix-patches@gnu.org; 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 ) id 1jT2d3-0007v4-BF for guix-patches@gnu.org; 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@kadziolka.net@188.123.215.55) by pat (envelope-from , 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@kadziolka.net@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=?= To: x@wilsonb.com Subject: Re: gnu: Add metamath Message-ID: <20200427121248.cga7p43flnusf7zo@gravity> References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> <20200426172945.7ez6i2fl3pjcoexd@gravity> <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com> 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@wilsonb.com> Received-SPF: none client-ip=37.59.186.212; envelope-from=kuba@kadziolka.net; 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" , guix-patches@gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" 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@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.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-- From debbugs-submit-bounces@debbugs.gnu.org Mon May 11 07:26:26 2020 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 To: Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= Subject: Re: gnu: Add metamath From: "B. Wilson" 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-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@gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" 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" =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_=_-- From debbugs-submit-bounces@debbugs.gnu.org Mon May 11 10:07:30 2020 Received: (at submit) by debbugs.gnu.org; 11 May 2020 14:07:30 +0000 Received: from localhost ([127.0.0.1]:52891 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jY95a-000461-UQ for submit@debbugs.gnu.org; Mon, 11 May 2020 10:07:30 -0400 Received: from lists.gnu.org ([209.51.188.17]:44138) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jY95Q-00045a-Mj for submit@debbugs.gnu.org; Mon, 11 May 2020 10:07:26 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:54962) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1jY95Q-0002yM-H9 for guix-patches@gnu.org; Mon, 11 May 2020 10:07:16 -0400 Received: from m42-5.mailgun.net ([69.72.42.5]:47538) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1jY958-0002Pz-MV for guix-patches@gnu.org; Mon, 11 May 2020 10:07:16 -0400 DKIM-Signature: a=rsa-sha256; v=1; c=relaxed/relaxed; d=mg.wilsonb.com; q=dns/txt; s=krs; t=1589206034; h=Content-Type: MIME-Version: Message-Id: In-Reply-To: References: From: Subject: Cc: To: Date: Sender; bh=b8A0YMDlP5an8n7MXbIeMQdhk0NKM2YTV4d3kMhdkvk=; b=Y4iv6RyOPinwj7xI/GM4kyFm4QWpwEahK4+qjNEta7jty7KieKA6g9q6W4hQBMaoDf6y6BH9 Wk1IsSIUtP7qfQOeLUDJ/c77B1lpgW8j2DqM63tuY6N0Qx73/M/ohZHmlHNKDDRA5M95ecU6 J1XOIRH5RQZonJwLBnFHxJUqvkcdSNmJMWL0gWcQUgATIhJ3ev+bNefJ/a8Y0wsoiotr4cWp 0gAwg8MRAf2FhwcE/7vPdZwcdQCjG/NwCOWpx2ruIURsPx8HTi2/qPjwzi9HygFT1i5tgugQ DD6X5AsRfOGJ7UAOc9COJ66iCkWWLgbGtPHdYlmqJR7KODKXj2aNSA== 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 5eb95bc8.7fd1c9000f60-smtp-out-n05; Mon, 11 May 2020 14:06:00 -0000 (UTC) Received: from localhost (KD111239199242.au-net.ne.jp [111.239.199.242]) by wilsonb.com (Postfix) with ESMTPSA id 55FAAA00C8; Mon, 11 May 2020 14:05:57 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wilsonb.com; s=201703; t=1589205957; bh=b8A0YMDlP5an8n7MXbIeMQdhk0NKM2YTV4d3kMhdkvk=; h=Date:To:Cc:Subject:From:References:In-Reply-To:From; b=G8yUP+Ks9UiczJpcENjKokLO2+ZBbo1/JfJax7LUvMvNiyzwHiuYxGan1Dk8Vw3jg vYuvkBhU8t9REmvC4JU4z1WtoXvpezh8F4RCWU/vhvq0NfbyQBan2MTI7+ibNdjSN/ psim5a+SrLKdOs2l1lzUhkG0wd1z3qNntUB69CE3Kh/O081TPeJ9WUgFBcMpMjjis0 jQXSjeiqlI3+k+z6pQpMhZ8BLiEsjK4QBrmJSCFd3mSZ/ADzQPr3hTqaHrNDltWuQq 2lzNEb4rkI5CQy/PNNUpS8t4W3+AipNig0tcjTN/HYtmbdD70TZIRXhNtbztCqWkFg YlZSRoxE0bakZTyowqMpT0buX6qx1mGlB8UUdEJqJtDjTpm2AhZGxgAnvSD1W/agko 3MWpQNjt2vk+g/ZPBDH5mCtygw3TuDHfDu7GdEEwLEIUAGeda1qlL9ya/2k0qQUliy WDis9WbetcRZcyIw8McWp8sKWr8Cq+IcPzWuHhR5RYAZkGc9B++MziX6pz3X7gyZNM s4BKFOr9h8Al7H1TIuWaRtYzVnHsgUOdUNXz2Fbyaz/khKcS27aT6ksdQdsiRFSAUj LcxnJs4p3eCRIEheC4JnLsaN9hde8U3seT4Ovnh+S7zx8SWl64O+YD2pncxpSB1QLE bGn6NKWTSR9IhWC/imjusDY4= Date: Mon, 11 May 2020 23:05:48 +0900 To: guix-patches@gnu.org Subject: Re: gnu: Add metamath From: "B. Wilson" References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> <20200426172945.7ez6i2fl3pjcoexd@gravity> <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com> <20200427121248.cga7p43flnusf7zo@gravity> <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com> In-Reply-To: <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com> Message-Id: <25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com> User-Agent: mblaze/0.5.1 MIME-Version: 1.0 Content-Type: multipart/signed; micalg="pgp-sha1"; protocol="application/pgp-signature"; boundary="----_=_273a89163ec2adca5de5ddad_=_" 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 10:06:57 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: Updated patch for metamath, containing two fixes: * Rename source repo checkout to match package name (fixes lint warning), and * Consolidate pdf under share/doc/- with LICENSE.TXT. From f7c803351c483ff0efe0e65604fec3de001f7282 Mon Sep 17 00:00:00 2001 From: "B. Wilson" Date: Mon, 11 May 2020 20:10:48 +0900 Subject: [PATCH] gnu: Add metamath. To: guix-pat [...] 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: Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.5 (/) This is a multipart message in MIME format. ------_=_273a89163ec2adca5de5ddad_=_ MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----_=_0956a90551bf04152c547a44_=_" This is a multipart message in MIME format. ------_=_0956a90551bf04152c547a44_=_ Content-Type: text/plain; charset=UTF-8 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Updated patch for metamath, containing two fixes: * Rename source repo checkout to match package name (fixes lint warning), a= nd * Consolidate pdf under share/doc/- with LICENSE.TXT. ------_=_0956a90551bf04152c547a44_=_ Content-Disposition: attachment; filename=0001-gnu-Add-metamath.patch Content-Type: text/x-patch Content-Transfer-Encoding: quoted-printable =46rom f7c803351c483ff0efe0e65604fec3de001f7282 Mon Sep 17 00:00:00 2001 =46rom: "B. Wilson" =44ate: Mon, 11 May 2020 20:10:48 +0900 =53ubject: [PATCH] gnu: Add metamath. =54o: guix-patches@gnu.org =0A* gnu/packages/maths.scm (metamath): New variable. =2D-- =20gnu/packages/maths.scm | 75 ++++++++++++++++++++++++++++++++++++++++++ =201 file changed, 75 insertions(+) =0Adiff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm =69ndex 8fbce15418..5dc600ccb5 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,77 @@ and conversions, physical constants, symbolic calc= =75lations (including =20integrals and equations), arbitrary precision, uncertainity propagation,= =0A interval arithmetic, plotting.") =20 (license license:gpl2+))) =2B =2B(define-public metamath =2B (package =2B (name "metamath") =2B (version "0.182") =2B (source =2B (origin =2B (method git-fetch) =2B (uri (git-reference =2B (url "https://github.com/metamath/metamath-exe.git") =2B (commit "5df616efe4119ff88daf77e7041d45b6fa39c578"))) =2B (sha256 =2B (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"))= =0A+ (file-name (string-append name "-" version "-checkout")))) =2B (build-system gnu-build-system) =2B (inputs =2B `(("book" =2B ,(origin =2B (method url-fetch) =2B (uri (string-append "https://github.com/metamath/" =2B "metamath-book/archive/second_edition.tar= =2Egz")) =2B (sha256 =2B (base32 =2B "1kbgajik9dn870db1zslqyvhn2j8g7shb8d6dm6njwqfkygiliir")))))= =29 =2B (native-inputs `(("autoconf" ,autoconf) =2B ("automake" ,automake) =2B ("texlive" ,(texlive-union =2B (list texlive-amsfonts =2B texlive-bibtex =2B texlive-breqn =2B texlive-makecell =2B texlive-microtype =2B texlive-tabu =2B texlive-latex-anysize =2B texlive-latex-hyperref =2B texlive-latex-needspace =2B texlive-latex-tools))))) =2B (outputs '("out" "doc")) =2B (arguments =2B `(#:phases =2B (let ((book-builddir "metamath-book-second_edition")) =2B (modify-phases %standard-phases =2B (add-after 'unpack 'unpack-doc =2B (lambda* (#:key inputs #:allow-other-keys) =2B (let ((book-tar (assoc-ref inputs "book"))) =2B (invoke "tar" "xzf" book-tar)))) =2B (add-after 'build 'build-doc =2B (lambda _ =2B (with-directory-excursion book-builddir =2B (invoke "touch" "metamath.ind") =2B (invoke "pdflatex" "metamath") =2B (invoke "pdflatex" "metamath") =2B (invoke "bibtex" "metamath") =2B (invoke "makeindex" "metamath") =2B (invoke "pdflatex" "metamath") =2B (invoke "pdflatex" "metamath")))) =2B (add-after 'build-doc 'install-doc =2B (lambda* (#:key outputs #:allow-other-keys) =2B (let* ((pkg (strip-store-file-name (assoc-ref outputs "ou= =74"))) =2B (out-doc (assoc-ref outputs "doc"))) =2B (install-file (string-append book-builddir "/metamath.p= =64f") =2B (string-append out-doc "/share/doc/" pkg)= =29 =2B #t))))))) =2B (home-page "http://us.metamath.org/") =2B (synopsis "Proof verifier based on a minimalistic formalism") =2B (description "Metamath is a tiny formal language and that can expres= =73 =2Btheorems in abstract mathematics, with an accompyaning @code{metamath} =2Bexecutable that verifies databases of these proofs. There is a public =2Bdatabase, @url{https://github.com/metamath/set.mm, set.mm}, implementing= =0A+first-order logic and Zermelo-Frenkel set theory with Choice, along wit= =68 a =2Blarge swath of associated, high-level theorems, e.g. the Fundamental The= =6Frem of =2BArithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc. See= =20the =2BMetamath book") =2B (license license:gpl2+))) =2D-=20 =32.26.2 =0A= ------_=_0956a90551bf04152c547a44_=_-- ------_=_273a89163ec2adca5de5ddad_=_ Content-Disposition: attachment; filename=signature.asc Content-Type: application/pgp-signature Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- iI0EABYIADUWIQQ7FdZn/PDWvxE6cmR2pStZ7i7CgQUCXrlbuhccZWxhZXh1b3Rl ZUB3aWxzb25iLmNvbQAKCRB2pStZ7i7CgXKJAP9sukjdMRBDlRrDFz0pYqT5VKeX 5fvlKGDfibjWAs6vpAEA3CFPgyuHawPX1KY7gsLLFg1h0jtnoM/D305fsDpe8ws= =pFWs -----END PGP SIGNATURE----- ------_=_273a89163ec2adca5de5ddad_=_-- From debbugs-submit-bounces@debbugs.gnu.org Wed May 13 03:25:44 2020 Received: (at 40815) by debbugs.gnu.org; 13 May 2020 07:25:44 +0000 Received: from localhost ([127.0.0.1]:57255 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jYllr-0001bO-7g for submit@debbugs.gnu.org; Wed, 13 May 2020 03:25:44 -0400 Received: from m42-5.mailgun.net ([69.72.42.5]:11341) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jYlln-0001b7-46 for 40815@debbugs.gnu.org; Wed, 13 May 2020 03:25:38 -0400 DKIM-Signature: a=rsa-sha256; v=1; c=relaxed/relaxed; d=mg.wilsonb.com; q=dns/txt; s=krs; t=1589354737; h=Content-Type: MIME-Version: Message-Id: Subject: From: To: Date: Sender; bh=PKXMj1p67RsaBaj4Qb6Jzz0UUWut2IjSSaWOVGRTqSE=; b=qvESmOodrnTAkCU0X26A3kNxdSrqfYO+/A6I3Vd1CXG5ET//vAMNnprnTtokFgVukGkTF+rv vo6tzkntNxmSLnqpUrGYfTx04Q+YtqWYFRnvTUlMC/VIRF6KM+nigb/KiMouO1EZ/tPMYn6o GmxWT/cMhhUd4mfQ/sbkH9Tph7U0hrj/kUzTsW+UDaTZ7J7Hz0rEnqysBgm9xYPCU2kFkEwm yH2PaUaqwCvhG+HXEdnmOAmudg0L+o5fxWc6+n5HH/aGVOADdmLzPOZoeJ0xwY3SZ4BFwpDJ iepapd09bGw7/7Txhd1r/h6BpPRlBdhqsUIx1irSM/0f9MW6gEvArw== X-Mailgun-Sending-Ip: 69.72.42.5 X-Mailgun-Sid: WyIxOGZjZiIsICI0MDgxNUBkZWJidWdzLmdudS5vcmciLCAiMDg1NDdhIl0= Received: from wilsonb.com (wilsonb.com [104.199.203.42]) by mxa.mailgun.org with ESMTP id 5ebba0dd.7fe5efd7be40-smtp-out-n05; Wed, 13 May 2020 07:25:17 -0000 (UTC) Received: from localhost (KD111239206087.au-net.ne.jp [111.239.206.87]) by wilsonb.com (Postfix) with ESMTPSA id 716E0A137A for <40815@debbugs.gnu.org>; Wed, 13 May 2020 07:25:15 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wilsonb.com; s=201703; t=1589354715; bh=PKXMj1p67RsaBaj4Qb6Jzz0UUWut2IjSSaWOVGRTqSE=; h=Date:To:From:Subject:From; b=kfwFAVAbXyZcqN4JvNtZLceM1VgKaXncIMy6+Xws0C4ayqeot0H9LJW9Hoe3k5/aU BpotTmPH6pby36FEbAOKPzFjzNbs0EPq13S+kZMGXQarqHjd5XJKAvyuf5lLGfuvNq gs9J9uUsvZGhmedyXyefBeCqkI4TLG4DcvAu+Zgs7BQyVmWjK694M0pHNvkEXfvTnw OBKWnpCa0VsjMTtPQDIBK1JaioFyBV3VvJA3m1iMRDWDnnE7xAD0I+nnq4NnyN0gtL S2mWWFsq0u+ky9HXwOXwtAIEwqm6DC9qjoxKGHIFrusOIpDJ43WzBZq7qdJsCuhoEE 1pc+W7CWAm0o0twjppxrN0D+IWTY6wUkAQWczQ4L4+b9TExOxDgzUUCsTtlyM4Z+Iy kxmcmls7s3/LX9WTjes8vP32HCkxDvV5XF/ujHaiR8x4NRnTBUFjY/fMI9ZwilW0yc VHapqj7U4MaT9CYQpFQ4uLUf+59V9mcLarl1c1flpv2pc1NJei9AsUv5dWTFvdie9S n0xfl+iaJDTEOUo3OH9sdBlt+S5rsK2rwbr+RJybgomudH9WktdKiv87Ajk8Z7jzoJ Ah73/XF9RQYHAFV6s4g0npzSpDPMbHkfKQt0WtZe02LvCVmKV92yrRN+X0qPUVjXPf RNHL6alHOsAt+cm25QFkI4Tg= Date: Wed, 13 May 2020 16:25:11 +0900 To: 40815@debbugs.gnu.org From: elaexuotee@wilsonb.com Subject: gnu: Add metamath. Message-Id: <3A31ISRYFT791.2TFZ4E8NIDG43@wilsonb.com> User-Agent: mblaze/0.5.1 MIME-Version: 1.0 Content-Type: multipart/signed; micalg="pgp-sha1"; protocol="application/pgp-signature"; boundary="----_=_205eb33e5ee0479245956195_=_" 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: Just discovered the (git-file-name ...) function. This is a simple update to the metamath patch to use this instead of manually using string-append. From 0e9facf67f5af44bb8e605631a0be6c90ce23000 Mon Sep 17 00:00:00 2001 From: "B. Wilson" Date: Mon, 11 May 2020 20:10:48 +0900 Subject: [PATCH] gnu: Add metamath. To: guix-pat [...] 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: gnu.org] -0.0 RCVD_IN_DNSWL_NONE RBL: Sender listed at https://www.dnswl.org/, no trust [69.72.42.5 listed in list.dnswl.org] 0.0 RCVD_IN_MSPIKE_H3 RBL: Good reputation (+3) [69.72.42.5 listed in wl.mailspike.net] 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record -0.0 SPF_PASS SPF: sender matches SPF record 1.8 PDS_OTHER_BAD_TLD Untrustworthy TLDs [URI: nixo.xyz (xyz)] 0.0 RCVD_IN_MSPIKE_WL Mailspike good senders X-Debbugs-Envelope-To: 40815 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 0.8 (/) This is a multipart message in MIME format. ------_=_205eb33e5ee0479245956195_=_ MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----_=_673a3b405c10a00e2c730834_=_" This is a multipart message in MIME format. ------_=_673a3b405c10a00e2c730834_=_ Content-Type: text/plain; charset=UTF-8 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Just discovered the (git-file-name ...) function. This is a simple update t= o the metamath patch to use this instead of manually using string-append. ------_=_673a3b405c10a00e2c730834_=_ Content-Disposition: attachment; filename=0001-gnu-Add-metamath.patch Content-Type: text/x-patch Content-Transfer-Encoding: quoted-printable =46rom 0e9facf67f5af44bb8e605631a0be6c90ce23000 Mon Sep 17 00:00:00 2001 =46rom: "B. Wilson" =44ate: Mon, 11 May 2020 20:10:48 +0900 =53ubject: [PATCH] gnu: Add metamath. =54o: guix-patches@gnu.org =0A* gnu/packages/maths.scm (metamath): New variable. =2D-- =20gnu/packages/maths.scm | 75 ++++++++++++++++++++++++++++++++++++++++++ =201 file changed, 75 insertions(+) =0Adiff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm =69ndex d60c033dbc..5a7230cb53 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@ -5635,3 +5636,77 @@ and conversions, physical constants, symbolic calc= =75lations (including =20integrals and equations), arbitrary precision, uncertainity propagation,= =0A interval arithmetic, plotting.") =20 (license license:gpl2+))) =2B =2B(define-public metamath =2B (package =2B (name "metamath") =2B (version "0.182") =2B (source =2B (origin =2B (method git-fetch) =2B (uri (git-reference =2B (url "https://github.com/metamath/metamath-exe.git") =2B (commit "5df616efe4119ff88daf77e7041d45b6fa39c578"))) =2B (sha256 =2B (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"))= =0A+ (file-name (git-file-name name version)))) =2B (build-system gnu-build-system) =2B (inputs =2B `(("book" =2B ,(origin =2B (method url-fetch) =2B (uri (string-append "https://github.com/metamath/" =2B "metamath-book/archive/second_edition.tar= =2Egz")) =2B (sha256 =2B (base32 =2B "1kbgajik9dn870db1zslqyvhn2j8g7shb8d6dm6njwqfkygiliir")))))= =29 =2B (native-inputs `(("autoconf" ,autoconf) =2B ("automake" ,automake) =2B ("texlive" ,(texlive-union =2B (list texlive-amsfonts =2B texlive-bibtex =2B texlive-breqn =2B texlive-makecell =2B texlive-microtype =2B texlive-tabu =2B texlive-latex-anysize =2B texlive-latex-hyperref =2B texlive-latex-needspace =2B texlive-latex-tools))))) =2B (outputs '("out" "doc")) =2B (arguments =2B `(#:phases =2B (let ((book-builddir "metamath-book-second_edition")) =2B (modify-phases %standard-phases =2B (add-after 'unpack 'unpack-doc =2B (lambda* (#:key inputs #:allow-other-keys) =2B (let ((book-tar (assoc-ref inputs "book"))) =2B (invoke "tar" "xzf" book-tar)))) =2B (add-after 'build 'build-doc =2B (lambda _ =2B (with-directory-excursion book-builddir =2B (invoke "touch" "metamath.ind") =2B (invoke "pdflatex" "metamath") =2B (invoke "pdflatex" "metamath") =2B (invoke "bibtex" "metamath") =2B (invoke "makeindex" "metamath") =2B (invoke "pdflatex" "metamath") =2B (invoke "pdflatex" "metamath")))) =2B (add-after 'build-doc 'install-doc =2B (lambda* (#:key outputs #:allow-other-keys) =2B (let* ((pkg (strip-store-file-name (assoc-ref outputs "ou= =74"))) =2B (out-doc (assoc-ref outputs "doc"))) =2B (install-file (string-append book-builddir "/metamath.p= =64f") =2B (string-append out-doc "/share/doc/" pkg)= =29 =2B #t))))))) =2B (home-page "http://us.metamath.org/") =2B (synopsis "Proof verifier based on a minimalistic formalism") =2B (description "Metamath is a tiny formal language and that can expres= =73 =2Btheorems in abstract mathematics, with an accompyaning @code{metamath} =2Bexecutable that verifies databases of these proofs. There is a public =2Bdatabase, @url{https://github.com/metamath/set.mm, set.mm}, implementing= =0A+first-order logic and Zermelo-Frenkel set theory with Choice, along wit= =68 a =2Blarge swath of associated, high-level theorems, e.g. the Fundamental The= =6Frem of =2BArithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc. See= =20the =2BMetamath book") =2B (license license:gpl2+))) =2D-=20 =32.26.2 =0A= ------_=_673a3b405c10a00e2c730834_=_-- ------_=_205eb33e5ee0479245956195_=_ Content-Disposition: attachment; filename=signature.asc Content-Type: application/pgp-signature Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- iI0EABYIADUWIQQ7FdZn/PDWvxE6cmR2pStZ7i7CgQUCXrug1hccZWxhZXh1b3Rl ZUB3aWxzb25iLmNvbQAKCRB2pStZ7i7CgfzUAQDulEAGYH6mXFyTY0u9lTQo7QMO xztc0htALud3m9OtQQEA/2wSBD0wzWU9Z6Erd1rX3PW9EBya4y+z3ouXeSLy1Qo= =cnZ1 -----END PGP SIGNATURE----- ------_=_205eb33e5ee0479245956195_=_-- From debbugs-submit-bounces@debbugs.gnu.org Thu Jun 04 13:49:40 2020 Received: (at submit) by debbugs.gnu.org; 4 Jun 2020 17:49:40 +0000 Received: from localhost ([127.0.0.1]:47426 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jgtzn-0006Fg-JG for submit@debbugs.gnu.org; Thu, 04 Jun 2020 13:49:39 -0400 Received: from lists.gnu.org ([209.51.188.17]:42170) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jgtzm-0006FX-K6 for submit@debbugs.gnu.org; Thu, 04 Jun 2020 13:49:38 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:33790) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1jgtzk-0007cc-WF for guix-patches@gnu.org; Thu, 04 Jun 2020 13:49:38 -0400 Received: from relay10.mail.gandi.net ([217.70.178.230]:57159) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1jgtzi-0007rs-V5 for guix-patches@gnu.org; Thu, 04 Jun 2020 13:49:36 -0400 Received: from localhost (40-67.ipv4.commingeshautdebit.fr [185.131.40.67]) (Authenticated sender: admin@nicolasgoaziou.fr) by relay10.mail.gandi.net (Postfix) with ESMTPSA id 376A5240003; Thu, 4 Jun 2020 17:49:29 +0000 (UTC) From: Nicolas Goaziou To: "B. Wilson via Guix-patches" via Subject: Re: [bug#40815] gnu: Add metamath References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> <20200426172945.7ez6i2fl3pjcoexd@gravity> <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com> <20200427121248.cga7p43flnusf7zo@gravity> <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com> <25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com> Date: Thu, 04 Jun 2020 19:49:28 +0200 In-Reply-To: <25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com> (B. Wilson via Guix-patches's message of "Mon, 11 May 2020 23:05:48 +0900") Message-ID: <87d06eraaf.fsf@nicolasgoaziou.fr> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain Received-SPF: pass client-ip=217.70.178.230; envelope-from=mail@nicolasgoaziou.fr; helo=relay10.mail.gandi.net X-detected-operating-system: by eggs.gnu.org: First seen = 2020/06/04 13:49:31 X-ACL-Warn: Detected OS = Linux 3.11 and newer X-Spam_score_int: -25 X-Spam_score: -2.6 X-Spam_bar: -- X-Spam_report: (-2.6 / 5.0 requ) BAYES_00=-1.9, RCVD_IN_DNSWL_LOW=-0.7, RCVD_IN_MSPIKE_H2=-0.001, SPF_PASS=-0.001, URIBL_BLOCKED=0.001 autolearn=_AUTOLEARN X-Spam_action: no action X-Spam-Score: -1.6 (-) X-Debbugs-Envelope-To: submit Cc: Jakub =?utf-8?B?S8SFZHppb8WCa2E=?= , "B. Wilson" , 40815@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -2.6 (--) Hello, "B. Wilson via Guix-patches" via writes: > Updated patch for metamath, containing two fixes: > > * Rename source repo checkout to match package name (fixes lint warning), and > * Consolidate pdf under share/doc/- with LICENSE.TXT. Thank you! Unfortunately I cannot comment about Texlive packages, and particularly about the issue you're encountering there, but I can give some advice on this package definition. > +(define-public metamath > + (package > + (name "metamath") > + (version "0.182") I suggest to let-bind the commit hash around the package definition, add a revision number, and a comment explaining why you're not using plain v0.182 tag. > + (source > + (origin > + (method git-fetch) > + (uri (git-reference > + (url "https://github.com/metamath/metamath-exe.git") > + (commit "5df616efe4119ff88daf77e7041d45b6fa39c578"))) > + (sha256 > + (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp")) > + (file-name (string-append name "-" version "-checkout")))) This should be `git-file-name', but I saw you fixed it already. > + (build-system gnu-build-system) > + (inputs > + `(("book" > + ,(origin > + (method url-fetch) > + (uri (string-append "https://github.com/metamath/" > + "metamath-book/archive/second_edition.tar.gz")) IIRC, this URL is reliable. You could fetch "second_editon" tag instead. > + (sha256 > + (base32 > + "1kbgajik9dn870db1zslqyvhn2j8g7shb8d6dm6njwqfkygiliir")))))) > + (native-inputs `(("autoconf" ,autoconf) > + ("automake" ,automake) > + ("texlive" ,(texlive-union > + (list texlive-amsfonts > + texlive-bibtex > + texlive-breqn > + texlive-makecell > + texlive-microtype > + texlive-tabu > + texlive-latex-anysize > + texlive-latex-hyperref > + texlive-latex-needspace > + texlive-latex-tools))))) > + (outputs '("out" "doc")) Nitpick: this is often located right after the source keyword. > + (description "Metamath is a tiny formal language and that can express > +theorems in abstract mathematics, with an accompyaning @code{metamath} > +executable that verifies databases of these proofs. There is a public > +database, @url{https://github.com/metamath/set.mm, set.mm}, implementing > +first-order logic and Zermelo-Frenkel set theory with Choice, along with a > +large swath of associated, high-level theorems, e.g. the Fundamental > Theorem of You cannot use "e.g." in Texinfo syntax, because the last dot confuses it. It should be either "e.g.,", or "e.g.@:". > +Arithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc. See the > +Metamath book") Missing final full stop. > + (license license:gpl2+))) I think there are other licenses involved. Could you try to list them, too? Regards, -- Nicolas Goaziou From debbugs-submit-bounces@debbugs.gnu.org Tue Jun 23 07:32:54 2020 Received: (at 40815) by debbugs.gnu.org; 23 Jun 2020 11:32:54 +0000 Received: from localhost ([127.0.0.1]:35587 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jnhAX-0004yV-Ak for submit@debbugs.gnu.org; Tue, 23 Jun 2020 07:32:54 -0400 Received: from m42-5.mailgun.net ([69.72.42.5]:25888) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jnhAS-0004y9-HK for 40815@debbugs.gnu.org; Tue, 23 Jun 2020 07:32:48 -0400 DKIM-Signature: a=rsa-sha256; v=1; c=relaxed/relaxed; d=mg.wilsonb.com; q=dns/txt; s=krs; t=1592911967; h=Content-Type: MIME-Version: Message-Id: In-Reply-To: References: Subject: From: Cc: To: Date: Sender; bh=a10opU8ccwtmcRfUszvEOfA+87Kjm8YRP2AACKESBw4=; b=s8REuDcP8Ato9mg8ULwYCbAnXtuFcwedEcqtOuyGUzE6/5yi6lemZehSRJyFvsY5Wc3oJQ8i abuOG4NGUcaejtuwioak5BqyhsRzjXpy39d7vxwgCSsJel9yzKoSsYspRTxXA8cBBZM31xK/ eQS1/z8fXwvP1cGj3WGWa5zxadpKt6EvRiv1eKkCOAZ9wCd0GYll1/ROBJboU2PKHiajNDBX Ny3JZeysIbQ+dm/vLruC7wTuYTEGYSuBc7LSj2X1VPOuLDvGLNviohS7vC3WmtxGhDXwAF5S 8C++3U2JZA4OlHrtzFF6lZhsww7atPp46OBv9ysdXqr6AiiUdWOw8A== X-Mailgun-Sending-Ip: 69.72.42.5 X-Mailgun-Sid: WyIxOGZjZiIsICI0MDgxNUBkZWJidWdzLmdudS5vcmciLCAiMDg1NDdhIl0= Received: from wilsonb.com (wilsonb.com [104.199.203.42]) by smtp-out-n06.prod.us-east-1.postgun.com with SMTP id 5ef1e84686de6ccd44aa255f (version=TLS1.3, cipher=TLS_AES_128_GCM_SHA256); Tue, 23 Jun 2020 11:32:22 GMT Received: from localhost (KD111239209250.au-net.ne.jp [111.239.209.250]) by wilsonb.com (Postfix) with ESMTPSA id 3577FA2B2F; Tue, 23 Jun 2020 11:32:19 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wilsonb.com; s=201703; t=1592911939; bh=a10opU8ccwtmcRfUszvEOfA+87Kjm8YRP2AACKESBw4=; h=Date:To:Cc:From:Subject:References:In-Reply-To:From; b=0HIkxt2aR9sLOuPT641G5Ps2egmRKDJQL2IWEO8htYI86uuDMjMT+NTcr2VK5NYqz vBN9Yoco7n9CRU4NMtYnOsgoNBJZl15oF8vsi/y1rOMEBD+Z4GAigFftstyERpRTsl b969LNsJW/4uwZx8FPOKfortwrim3gS5mBYgx3RZtfyMmPNPcw8U7B10E7HiLXyYkj DzuzA56nzmrdPxPp4euEL15fwsOqGDqbPSB4902zPx3JHjZY688hFR0MwY85yZuHfL W+pVejkC36TeHxsw3NKyFwkZHf+l+YKGh8yu692zq98Qfyf745woOvpvvDmJlQAPTk JbXsV9yHvl+MrMJx4KWJnJIqHDRBB6gmzXtz/uyeRdYbsQ8T5jFEh4TskXNmbueJ7k FVN5FaSEG1Y25z+AY5VkFYpzQxtTuWVKTaYd/L6GS9ddO6SXokhxz0/5RQ8wV8vkcq kQFo1H6jX4V8s3ezGWS5HPG8pjeWwK5p6gLrrgJZPboAl9aqqthS/Z+DQCBGygFxkL cfSSpOIa/x0pQuMsLayfnWBgzz0L+MbLSlDUc0AeW/k/nSGlI5z2fKi3Cf+mybRfbX xjYVOFC8VGHLrVTyg2Ms0YqiVmQO25e6VS3Bw95v43mY1wi5wkC/2AG7PECn7VfW6d M+F1WdPYIZgNv+YNf/s3JeGU= Date: Tue, 23 Jun 2020 20:32:15 +0900 To: Nicolas Goaziou From: elaexuotee@wilsonb.com Subject: Re: [bug#40815] gnu: Add metamath References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> <20200426172945.7ez6i2fl3pjcoexd@gravity> <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com> <20200427121248.cga7p43flnusf7zo@gravity> <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com> <25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com> <87d06eraaf.fsf@nicolasgoaziou.fr> In-Reply-To: <87d06eraaf.fsf@nicolasgoaziou.fr> Message-Id: <23UB7VNWCB6BC.23I1T2MHNG4ZI@wilsonb.com> User-Agent: mblaze/0.7 MIME-Version: 1.0 Content-Type: multipart/signed; micalg="pgp-sha1"; protocol="application/pgp-signature"; boundary="----_=_72224fa1070edd531e04536d_=_" X-Spam-Score: 2.0 (++) X-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: Hello Nicolas, Thank you for taking a look at this! > Unfortunately I cannot comment about Texlive packages, and particularly > about the issue you're encountering there, but I can give some advice on > this package definition. Content analysis details: (2.0 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs [URI: nixo.xyz (xyz)] 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record -0.0 SPF_PASS SPF: sender matches SPF record -0.0 RCVD_IN_DNSWL_NONE RBL: Sender listed at https://www.dnswl.org/, no trust [69.72.42.5 listed in list.dnswl.org] -0.0 RCVD_IN_MSPIKE_H2 RBL: Average reputation (+2) [69.72.42.5 listed in wl.mailspike.net] X-Debbugs-Envelope-To: 40815 Cc: , Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= , 40815@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 1.0 (+) This is a multipart message in MIME format. ------_=_72224fa1070edd531e04536d_=_ MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----_=_1629333b79c91715769c82f7_=_" This is a multipart message in MIME format. ------_=_1629333b79c91715769c82f7_=_ Content-Type: text/plain; charset=UTF-8 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Hello Nicolas, Thank you for taking a look at this! > Unfortunately I cannot comment about Texlive packages, and particularly > about the issue you're encountering there, but I can give some advice on > this package definition. This patch has been languishing around for quite a while, and instead of waiting for texlive-amsfonts to get fixed, I propose nuking the "doc" outpu= t for now so we can get this pushed. The attached patch does just this. I commented out the parts specific to th= e "doc" output and also included FIXME explanations of what's going on. > I suggest to let-bind the commit hash around the package definition, add > a revision number, and a comment explaining why you're not using plain > v0.182 tag. Done. > > + (build-system gnu-build-system) > > + (inputs > > + `(("book" > > + ,(origin > > + (method url-fetch) > > + (uri (string-append "https://github.com/metamath/" > > + "metamath-book/archive/second_edition.t= ar.gz")) >=20 > IIRC, this URL is reliable. You could fetch "second_editon" tag instead. This is now a commented out section, but I went ahead and updated it as you= suggested. Since this is a non-cosmetic change, I also test built it before= commenting out all the "doc" output stuff. > Nitpick: [outputs] is often located right after the source keyword. Moved. Not sure why I put it down there in the first place. I chock it up t= o this being my first package attempt. > You cannot use "e.g." in Texinfo syntax, because the last dot confuses > it. It should be either "e.g.,", or "e.g.@:". >=20 > > +Arithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc. S= ee the > > +Metamath book") >=20 > Missing final full stop. Fixed. Thanks for the attention to detail. > I think there are other licenses involved. Could you try to list them, > too? Were you referring to CC0 for the metamath book? I added this license in a FIXME comment. As far as I can tell, the metamath= executable itself is just GLP2+, but if I'm missing something please let me= know. Hopefully, in the near future I will find time to dig into the texlive-amsf= onts issue, but for now, does this look good? If we end up pushing just the metamath patch, the other texlive package pat= ches obviously aren't needed for now, but would it be worth pushing these? Shoul= d I submit separate issues for them? Cheers, ------_=_1629333b79c91715769c82f7_=_ Content-Disposition: attachment; filename=0001-gnu-Add-metamath.patch Content-Type: text/x-patch Content-Transfer-Encoding: quoted-printable =46rom f7e7a323df50fc5c6d4aefb30f67991c367dfabc Mon Sep 17 00:00:00 2001 =46rom: "B. Wilson" =44ate: Mon, 11 May 2020 20:10:48 +0900 =53ubject: [PATCH] gnu: Add metamath. =54o: guix-patches@gnu.org =0A* gnu/packages/maths.scm (metamath): New variable. =2D-- =20gnu/packages/maths.scm | 75 ++++++++++++++++++++++++++++++++++++++++++ =201 file changed, 75 insertions(+) =0Adiff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm =69ndex 45d699e39c..82b98d8f7d 100644 =2D-- a/gnu/packages/maths.scm =2B++ b/gnu/packages/maths.scm =40@ -38,6 +38,7 @@ =20;;; Copyright =C2=A9 2020 R Veera Kumar =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@ -5686,3 +5687,77 @@ and conversions, physical constants, symbolic calc= =75lations (including =20integrals and equations), arbitrary precision, uncertainity propagation,= =0A interval arithmetic, plotting.") =20 (license license:gpl2+))) =2B =2B(define-public metamath =2B (package =2B (name "metamath") =2B (version "0.182") =2B (source =2B (origin =2B (method git-fetch) =2B (uri (git-reference =2B (url "https://github.com/metamath/metamath-exe.git") =2B (commit "5df616efe4119ff88daf77e7041d45b6fa39c578"))) =2B (sha256 =2B (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"))= =0A+ (file-name (git-file-name name version)))) =2B (build-system gnu-build-system) =2B (inputs =2B `(("book" =2B ,(origin =2B (method url-fetch) =2B (uri (string-append "https://github.com/metamath/" =2B "metamath-book/archive/second_edition.tar= =2Egz")) =2B (sha256 =2B (base32 =2B "1kbgajik9dn870db1zslqyvhn2j8g7shb8d6dm6njwqfkygiliir")))))= =29 =2B (native-inputs `(("autoconf" ,autoconf) =2B ("automake" ,automake) =2B ("texlive" ,(texlive-union =2B (list texlive-amsfonts =2B texlive-bibtex =2B texlive-breqn =2B texlive-makecell =2B texlive-microtype =2B texlive-tabu =2B texlive-latex-anysize =2B texlive-latex-hyperref =2B texlive-latex-needspace =2B texlive-latex-tools))))) =2B (outputs '("out" "doc")) =2B (arguments =2B `(#:phases =2B (let ((book-builddir "metamath-book-second_edition")) =2B (modify-phases %standard-phases =2B (add-after 'unpack 'unpack-doc =2B (lambda* (#:key inputs #:allow-other-keys) =2B (let ((book-tar (assoc-ref inputs "book"))) =2B (invoke "tar" "xzf" book-tar)))) =2B (add-after 'build 'build-doc =2B (lambda _ =2B (with-directory-excursion book-builddir =2B (invoke "touch" "metamath.ind") =2B (invoke "pdflatex" "metamath") =2B (invoke "pdflatex" "metamath") =2B (invoke "bibtex" "metamath") =2B (invoke "makeindex" "metamath") =2B (invoke "pdflatex" "metamath") =2B (invoke "pdflatex" "metamath")))) =2B (add-after 'build-doc 'install-doc =2B (lambda* (#:key outputs #:allow-other-keys) =2B (let* ((pkg (strip-store-file-name (assoc-ref outputs "ou= =74"))) =2B (out-doc (assoc-ref outputs "doc"))) =2B (install-file (string-append book-builddir "/metamath.p= =64f") =2B (string-append out-doc "/share/doc/" pkg)= =29 =2B #t))))))) =2B (home-page "http://us.metamath.org/") =2B (synopsis "Proof verifier based on a minimalistic formalism") =2B (description "Metamath is a tiny formal language and that can expres= =73 =2Btheorems in abstract mathematics, with an accompyaning @code{metamath} =2Bexecutable that verifies databases of these proofs. There is a public =2Bdatabase, @url{https://github.com/metamath/set.mm, set.mm}, implementing= =0A+first-order logic and Zermelo-Frenkel set theory with Choice, along wit= =68 a =2Blarge swath of associated, high-level theorems, e.g. the Fundamental The= =6Frem of =2BArithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc. See= =20the =2BMetamath book") =2B (license license:gpl2+))) =2D-=20 =32.27.0 =0A= ------_=_1629333b79c91715769c82f7_=_-- ------_=_72224fa1070edd531e04536d_=_ Content-Disposition: attachment; filename=signature.asc Content-Type: application/pgp-signature Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- iI0EABYIADUWIQQ7FdZn/PDWvxE6cmR2pStZ7i7CgQUCXvHoOBccZWxhZXh1b3Rl ZUB3aWxzb25iLmNvbQAKCRB2pStZ7i7CgYIHAQC4vb+FbU2y/Tq2vfTjkKLCe3p+ RfrmFdsSZzDPiSY9tAD9Ew21FUW7H0AEPRuquynZyccz5xSWfeW8mZeOqWNnCQY= =ds0W -----END PGP SIGNATURE----- ------_=_72224fa1070edd531e04536d_=_-- From debbugs-submit-bounces@debbugs.gnu.org Tue Jun 23 21:15:13 2020 Received: (at 40815) by debbugs.gnu.org; 24 Jun 2020 01:15:13 +0000 Received: from localhost ([127.0.0.1]:37456 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jnu0I-000624-OL for submit@debbugs.gnu.org; Tue, 23 Jun 2020 21:15:13 -0400 Received: from m42-5.mailgun.net ([69.72.42.5]:58556) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jnu0C-000618-EE for 40815@debbugs.gnu.org; Tue, 23 Jun 2020 21:15:04 -0400 DKIM-Signature: a=rsa-sha256; v=1; c=relaxed/relaxed; d=mg.wilsonb.com; q=dns/txt; s=krs; t=1592961301; h=Content-Type: MIME-Version: Message-Id: In-Reply-To: References: Subject: From: Cc: To: Date: Sender; bh=5xWv9A+n1/p/KuIw5CR6hefmq8fmrfTDM1WS4I0VnNg=; b=PBq+mVsIMvpuBnor5YpmZm+nwSGocYMX/Ib8gVkmupVppEMGFjyVU9Vd7XnxTDc+ZiUpQ/+m 3Y3wokbSDU9gOJ0w/HRguofAcY2ryqy1EsI7+jdXmKbHMRHV9wK63Tak7JrCQUlweDv19NFE StC6ib9PBkx7RcjmkSdVsDWLskQkbaWmTSa3yORQDBzYC4Bk0iuvKLp1VH/E08JP39DF7EfR ET/JullMT8NdGCNHZwipSGYETJnQdPq3btX7BItEw7Bfgx1vHVjWK5NYlPjyFsoNsEcMNkPI l381gq2iJUtmKFkgH708VtyEhK+SgJuXY23inKFUxh9AwvzZL0ErBQ== X-Mailgun-Sending-Ip: 69.72.42.5 X-Mailgun-Sid: WyIxOGZjZiIsICI0MDgxNUBkZWJidWdzLmdudS5vcmciLCAiMDg1NDdhIl0= Received: from wilsonb.com (wilsonb.com [104.199.203.42]) by smtp-out-n13.prod.us-east-1.postgun.com with SMTP id 5ef2a906a3d8a44743275490 (version=TLS1.3, cipher=TLS_AES_128_GCM_SHA256); Wed, 24 Jun 2020 01:14:46 GMT Received: from localhost (KD111239204110.au-net.ne.jp [111.239.204.110]) by wilsonb.com (Postfix) with ESMTPSA id 8AE98A2C1E; Wed, 24 Jun 2020 01:14:43 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wilsonb.com; s=201703; t=1592961283; bh=5xWv9A+n1/p/KuIw5CR6hefmq8fmrfTDM1WS4I0VnNg=; h=Date:To:Cc:From:Subject:References:In-Reply-To:From; b=J7TITzrLrOPvFOOjMdcdwEGdu1HT5xbL+awrvUzJsTDbI/M6c4sFGNoQiDtqe56qL YB1CQapi4Zw1Z+EicBBmeohHLYhZCvMJS1RzG6ipWdR550nanonaGZKaChjX7AAuIX zyqwu7YjZROBZmaEiL4NSsjrhsa5rRRkTKCVK4nwDfPmzojIUXOBhNYTLneFviPg0t g6RItWdErQITI8UTCtKuKk0A51YNQOoN2B11mx1MW0DzTfWnuwF6EGVa/iDpeVaqk/ ULHpGOdhjYaFArQxuxm5aMamMuZGuFZKX2qd9zq5Q8s59UEYQgoiazm8/f4edcRX9/ LSLqJR8BUG5HBa5EIwXGSiyKzj3tvH9zuLp91k8zsedNcWNCaXUgH7gqFFGV/1idZj EpEK96qD2YML2RzDHsE8yeZuplhRK5n4pOLUiS3cG8CMwQ7LqhCGCHJUmtzVCVSHj3 zckxPLXFbyTessr3wqin4lTWMBrSH2uN8pq+Uq+y2D0x+PDqTD0PxFj9yoTv3hJglo 6/pXLgatUxMMmviBU0JCHr2JgvS+mbqrMjUA7XeW0pUvWsMxdW2Y4cMLsVBFzdfUuq rNQlId0ia+JEcY8/u7cYT0Q7s70ssehF4fOj88DxzLqsl0UL5ZODAAkz1XD1OoKrZ3 +1lGwmWitqbSZyErN8k4HUNc= Date: Wed, 24 Jun 2020 10:14:39 +0900 To: Nicolas Goaziou From: elaexuotee@wilsonb.com Subject: Re: [bug#40815] gnu: Add metamath References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> <20200426172945.7ez6i2fl3pjcoexd@gravity> <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com> <20200427121248.cga7p43flnusf7zo@gravity> <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com> <25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com> <87d06eraaf.fsf@nicolasgoaziou.fr> In-Reply-To: <87d06eraaf.fsf@nicolasgoaziou.fr> Message-Id: <31H3GR8EOYWGZ.2EEY2GE3LMLRZ@wilsonb.com> User-Agent: mblaze/0.7 MIME-Version: 1.0 Content-Type: multipart/signed; micalg="pgp-sha1"; protocol="application/pgp-signature"; boundary="----_=_23e6165e77eb4ce4043f1aa2_=_" X-Spam-Score: 2.0 (++) X-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: Oops. Looks like my previous emais's patch was for the version that *didn't* comment out the "doc" output. The one included here should be correct. From 74db38db11a7e107119362983e388cfb5ead3431 Mon Sep 17 00:00:00 2001 From: "B. Wilson" Date: Mon, 11 May 2020 20:10:48 +0900 Subject: [PATCH] gnu: Add metamath. To: guix-pat [...] Content analysis details: (2.0 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs [URI: nixo.xyz (xyz)] 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record -0.0 SPF_PASS SPF: sender matches SPF record -0.0 RCVD_IN_MSPIKE_H2 RBL: Average reputation (+2) [69.72.42.5 listed in wl.mailspike.net] -0.0 RCVD_IN_DNSWL_NONE RBL: Sender listed at https://www.dnswl.org/, no trust [69.72.42.5 listed in list.dnswl.org] X-Debbugs-Envelope-To: 40815 Cc: Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= , 40815@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 1.0 (+) This is a multipart message in MIME format. ------_=_23e6165e77eb4ce4043f1aa2_=_ MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----_=_398bc6d86f3b7154107c411f_=_" This is a multipart message in MIME format. ------_=_398bc6d86f3b7154107c411f_=_ Content-Type: text/plain; charset=UTF-8 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Oops. Looks like my previous emais's patch was for the version that *didn't= * comment out the "doc" output. The one included here should be correct. ------_=_398bc6d86f3b7154107c411f_=_ Content-Disposition: attachment; filename=0001-gnu-Add-metamath.patch Content-Type: text/x-patch Content-Transfer-Encoding: quoted-printable =46rom 74db38db11a7e107119362983e388cfb5ead3431 Mon Sep 17 00:00:00 2001 =46rom: "B. Wilson" =44ate: Mon, 11 May 2020 20:10:48 +0900 =53ubject: [PATCH] gnu: Add metamath. =54o: guix-patches@gnu.org =0A* gnu/packages/maths.scm (metamath): New variable. =2D-- =20gnu/packages/maths.scm | 97 ++++++++++++++++++++++++++++++++++++++++++ =201 file changed, 97 insertions(+) =0Adiff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm =69ndex 45d699e39c..e6f4cbe980 100644 =2D-- a/gnu/packages/maths.scm =2B++ b/gnu/packages/maths.scm =40@ -38,6 +38,7 @@ =20;;; Copyright =C2=A9 2020 R Veera Kumar =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@ -5686,3 +5687,99 @@ and conversions, physical constants, symbolic calc= =75lations (including =20integrals and equations), arbitrary precision, uncertainity propagation,= =0A interval arithmetic, plotting.") =20 (license license:gpl2+))) =2B =2B(define-public metamath =2B ;; Upstream pushed a commit on top of v0.182 that fixes a bug in Makef= =69le.am. =2B ;; Using this commit lets us avoid directly including the patch here. = =20In the =2B ;; next version bump, we should be able to replace this and directly u= =73e the =2B ;; version tag. =2B (let ((commit "5df616efe4119ff88daf77e7041d45b6fa39c578") =2B (revision "0") =2B (book-name "metamath-book") =2B (book-version "second_edition")) =2B (package =2B (name "metamath") =2B (version (git-version "0.182" revision commit)) =2B (source =2B (origin =2B (method git-fetch) =2B (uri (git-reference =2B (url "https://github.com/metamath/metamath-exe.git") =2B (commit commit))) =2B (sha256 =2B (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"= =29) =2B (file-name (git-file-name name version)))) =2B ;; FIXME: Unfortunately, there seems to be a problem with =2B ;; texlive-amsfonts that prevents us from typsetting the "doc" out= =70ut =2B ;; pdf. Once fixed, this along with the commented out sections be= =6Cow, =2B ;; should be enabled. =2B ; (outputs '("out" "doc")) =2B (build-system gnu-build-system) =2B ;; FIXME: Enable for "doc" output. See previous comment. =2B ; (inputs =2B ; `((,book-name =2B ; ,(origin =2B ; (method git-fetch) =2B ; (uri (git-reference =2B ; (url "https://github.com/metamath/metamath-book.git= =22) =2B ; (commit book-version))) =2B ; (sha256 =2B ; (base32 =2B ; "1kk9nfhs0h8qccpxp1qh072bpfis7h05rlnz3qn1z641d9i4ryyq")= =29 =2B ; (file-name (git-file-name book-name book-version)))))) =2B (native-inputs `(("autoconf" ,autoconf) =2B ("automake" ,automake) =2B ;; FIXME: Required inputs to build the "doc" outp= =75t. =2B ;; See above comment. =2B ; ("texlive" ,(texlive-union =2B ; (list texlive-amsfonts =2B ; texlive-bibtex =2B ; texlive-breqn =2B ; texlive-makecell =2B ; texlive-microtype =2B ; texlive-tabu =2B ; texlive-latex-anysize =2B ; texlive-latex-hyperref =2B ; texlive-latex-needspace =2B ; texlive-latex-tools))) =2B )) =2B ;; FIXME: Arguments to build the "doc" output. See above comment.= =0A+ ; (arguments =2B ; `(#:phases =2B ; (let ((book-builddir "metamath-book-second_edition")) =2B ; (modify-phases %standard-phases =2B ; (add-after 'unpack 'unpack-doc =2B ; (lambda* (#:key inputs #:allow-other-keys) =2B ; (let ((book (assoc-ref inputs ,book-name))) =2B ; (mkdir-p book-builddir) =2B ; (copy-recursively book book-builddir)))) =2B ; (add-after 'build 'build-doc =2B ; (lambda _ =2B ; (with-directory-excursion book-builddir =2B ; (invoke "touch" "metamath.ind") =2B ; (invoke "pdflatex" "metamath") =2B ; (invoke "pdflatex" "metamath") =2B ; (invoke "bibtex" "metamath") =2B ; (invoke "makeindex" "metamath") =2B ; (invoke "pdflatex" "metamath") =2B ; (invoke "pdflatex" "metamath")))) =2B ; (add-after 'build-doc 'install-doc =2B ; (lambda* (#:key outputs #:allow-other-keys) =2B ; (let* ((pkg (strip-store-file-name (assoc-ref outputs= =20"out"))) =2B ; (out-doc (assoc-ref outputs "doc"))) =2B ; (install-file (string-append book-builddir "/metama= =74h.pdf") =2B ; (string-append out-doc "/share/doc/" = =70kg)) =2B ; #t))))))) =2B (home-page "http://us.metamath.org/") =2B (synopsis "Proof verifier based on a minimalistic formalism") =2B (description "Metamath is a tiny formal language and that can expr= =65ss =2Btheorems in abstract mathematics, with an accompyaning @code{metamath} =2Bexecutable that verifies databases of these proofs. There is a public =2Bdatabase, @url{https://github.com/metamath/set.mm, set.mm}, implementing= =0A+first-order logic and Zermelo-Frenkel set theory with Choice, along wit= =68 a =2Blarge swath of associated, high-level theorems, e.g.@: the Fundamental T= =68eorem =2Bof Arithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc. = =53ee the =2BMetamath book.") =2B ;; FIXME: The "doc" output requires license:cc0. See above comment.= =0A+ ; (license '(,license:gpl2+ ,license:cc0))))) =2B (license license:gpl2+)))) =2D-=20 =32.27.0 =0A= ------_=_398bc6d86f3b7154107c411f_=_-- ------_=_23e6165e77eb4ce4043f1aa2_=_ Content-Disposition: attachment; filename=signature.asc Content-Type: application/pgp-signature Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- iI0EABYIADUWIQQ7FdZn/PDWvxE6cmR2pStZ7i7CgQUCXvKo/hccZWxhZXh1b3Rl ZUB3aWxzb25iLmNvbQAKCRB2pStZ7i7CgQ8aAP9XbXNroGsRIn0faF8qKaip/7hk VkGCMYnT03pq23eziAEApzEayV7nNLR5WBY9C7rmqV4yzJTl2LvEdiyxsSbhhA0= =MvlX -----END PGP SIGNATURE----- ------_=_23e6165e77eb4ce4043f1aa2_=_-- From debbugs-submit-bounces@debbugs.gnu.org Fri Jun 26 03:19:55 2020 Received: (at 40815) by debbugs.gnu.org; 26 Jun 2020 07:19:55 +0000 Received: from localhost ([127.0.0.1]:41750 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1joieR-0002dI-3q for submit@debbugs.gnu.org; Fri, 26 Jun 2020 03:19:55 -0400 Received: from relay7-d.mail.gandi.net ([217.70.183.200]:54521) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1joieO-0002cw-5p for 40815@debbugs.gnu.org; Fri, 26 Jun 2020 03:19:53 -0400 X-Originating-IP: 185.131.40.67 Received: from localhost (40-67.ipv4.commingeshautdebit.fr [185.131.40.67]) (Authenticated sender: admin@nicolasgoaziou.fr) by relay7-d.mail.gandi.net (Postfix) with ESMTPSA id AC67F20007; Fri, 26 Jun 2020 07:19:44 +0000 (UTC) From: Nicolas Goaziou To: elaexuotee@wilsonb.com Subject: Re: [bug#40815] gnu: Add metamath References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> <20200426172945.7ez6i2fl3pjcoexd@gravity> <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com> <20200427121248.cga7p43flnusf7zo@gravity> <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com> <25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com> <87d06eraaf.fsf@nicolasgoaziou.fr> <23UB7VNWCB6BC.23I1T2MHNG4ZI@wilsonb.com> Date: Fri, 26 Jun 2020 09:19:56 +0200 In-Reply-To: <23UB7VNWCB6BC.23I1T2MHNG4ZI@wilsonb.com> (elaexuotee@wilsonb.com's message of "Tue, 23 Jun 2020 20:32:15 +0900") Message-ID: <878sgas38j.fsf@nicolasgoaziou.fr> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: -0.7 (/) X-Debbugs-Envelope-To: 40815 Cc: Jakub =?utf-8?B?S8SFZHppb8WCa2E=?= , 40815@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.7 (-) Hello, laexuotee@wilsonb.com writes: > This patch has been languishing around for quite a while, and instead of > waiting for texlive-amsfonts to get fixed, I propose nuking the "doc" output > for now so we can get this pushed. Note the book could also go into another package, once texlive-amsfonts is fixed. Meanwhile, I think we can remove the comments in this one and apply it. WDYT? > Were you referring to CC0 for the metamath book? Probably, yes. > If we end up pushing just the metamath patch, the other texlive package patches > obviously aren't needed for now, but would it be worth pushing these? Should I > submit separate issues for them? I don't have enough knowledge to comment LaTeX packages. I suggest to submit them as separate issues. If still no one comments of them, I'll apply them later. Regards, -- Nicolas Goaziou From debbugs-submit-bounces@debbugs.gnu.org Fri Jun 26 04:47:00 2020 Received: (at 40815) by debbugs.gnu.org; 26 Jun 2020 08:47:00 +0000 Received: from localhost ([127.0.0.1]:41804 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jok0c-0004mD-Em for submit@debbugs.gnu.org; Fri, 26 Jun 2020 04:47:00 -0400 Received: from m42-5.mailgun.net ([69.72.42.5]:64455) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jok0V-0004lt-Ic for 40815@debbugs.gnu.org; Fri, 26 Jun 2020 04:46:53 -0400 DKIM-Signature: a=rsa-sha256; v=1; c=relaxed/relaxed; d=mg.wilsonb.com; q=dns/txt; s=krs; t=1593161210; h=Content-Type: MIME-Version: Message-Id: In-Reply-To: References: Subject: From: Cc: To: Date: Sender; bh=yUyZVlkcwHeA82HMJzNjAaEjhPrVIC+XlmfAMqLzClw=; b=ay9btskvftY1xIHzUCcnfOn+CLh5BtFJ4AzQ6WPgjaZuF4sYocAR+NHyoSwBOleLe0VPMTgt lQXWP8GQ5ZfxNeO9vDCY5RIPl5BJSOxw1FNFCe6vOIq9qyWyGyDJN81P6CSTD8SWk6R062zh YemWquPHsUtK4pv+YpuK+fVlqPhPQTpJutwfWZrBNuBmYQOWI5ZJUQ3udC+63uSORYtKG9Zd /xfZgOmfmNekfzny2UFFHcX7uVQobby2p3ygrHgtAKqhmKBVgQI/o1oFq850Xbm3UmtktZaD fNrYF/xyYJyZT3RFb9uRtCKTuRvsvLhY+W5lj6MjcMTaFVAIgwQGQA== X-Mailgun-Sending-Ip: 69.72.42.5 X-Mailgun-Sid: WyIxOGZjZiIsICI0MDgxNUBkZWJidWdzLmdudS5vcmciLCAiMDg1NDdhIl0= Received: from wilsonb.com (wilsonb.com [104.199.203.42]) by smtp-out-n14.prod.us-east-1.postgun.com with SMTP id 5ef5b5e986de6ccd4492fe83 (version=TLS1.3, cipher=TLS_AES_128_GCM_SHA256); Fri, 26 Jun 2020 08:46:33 GMT Received: from localhost (KD111239192210.au-net.ne.jp [111.239.192.210]) by wilsonb.com (Postfix) with ESMTPSA id 5D869A1A42; Fri, 26 Jun 2020 08:46:30 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wilsonb.com; s=201703; t=1593161190; bh=yUyZVlkcwHeA82HMJzNjAaEjhPrVIC+XlmfAMqLzClw=; h=Date:To:Cc:From:Subject:References:In-Reply-To:From; b=1e2H9KiqbRu0GUAob5ZpWZ4/WnQgfX+ky3MOzf+fKnS5rozPT/a5fxV9vVK6DbVua zkEacaS8CR8I0/775KFHA7cvohkV6wazDU7L56QRcwOSUZhFBBPqDbHMAmMpP8W/0b awVm4oNPS7REh0GxYEHhEykGko8INwXZ9/mhtyestl+eqAWDd3JCyJmX1Thubc8vMD OymWjP1i51Z3WHFqipFOctRRS5qXOGHOliCkEhGsrSji4+6GCm3QN7a4mqKfB/EMOl oWmqHc2zYh5TcCHDXLs7heAQ9z3zwLXXPCW/pvEPxiGahcjvG2eG3OQcTh/dqzX8M8 of9ksb0MLTNJQ7rInCtVp8cTBeGPpfjcZGYJhQ7qsbr8efNGJXcw032rJoJQ1QODhp tW12oa7MW2LMEw9SHd8PjLE5XLuaflmmSRDp38QIXv9tfSZ7f2e5S+/JiDmEGYIXGv kwBhEfBWhd7GKkfmypkIgsbgacBfG+P8fdVjk92XboZjvfbPmBbJhrD3B709JolL0J ixZ0GZ0EVBM0t3nfWz8wLmx9802iV5VT6IH2cd2m+uhCOgZkdw2jIkNL7hTVD+RvkB Rc/qbFGpmHpjcXuXqDFQLEbDN7FnfFkFneThC9cMTbjR5ctBHlX5uLA7EK1K/Kt6SK nrPmxOlaFWrdmzsk3ZcS5TyA= Date: Fri, 26 Jun 2020 17:46:22 +0900 To: Nicolas Goaziou From: elaexuotee@wilsonb.com Subject: Re: [bug#40815] gnu: Add metamath References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> <20200426172945.7ez6i2fl3pjcoexd@gravity> <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com> <20200427121248.cga7p43flnusf7zo@gravity> <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com> <25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com> <87d06eraaf.fsf@nicolasgoaziou.fr> <23UB7VNWCB6BC.23I1T2MHNG4ZI@wilsonb.com> <878sgas38j.fsf@nicolasgoaziou.fr> In-Reply-To: <878sgas38j.fsf@nicolasgoaziou.fr> Message-Id: <2Z19F0HU7SZNL.33AMEA6BFHCFT@wilsonb.com> User-Agent: mblaze/0.7 MIME-Version: 1.0 Content-Type: multipart/signed; micalg="pgp-sha1"; protocol="application/pgp-signature"; boundary="----_=_495d421c51d8a8da7ac9a4b0_=_" 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: > Note the book could also go into another package, once texlive-amsfonts is > fixed. Interesting. Either way it's a similarly sized patch, so I'm curious why a "metamath-doc" packages would be preferable to a "metamath:doc" output. Content analysis details: (2.0 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs [URI: nixo.xyz (xyz)] -0.0 RCVD_IN_DNSWL_NONE RBL: Sender listed at https://www.dnswl.org/, no trust [69.72.42.5 listed in list.dnswl.org] 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record -0.0 SPF_PASS SPF: sender matches SPF record -0.0 RCVD_IN_MSPIKE_H2 RBL: Average reputation (+2) [69.72.42.5 listed in wl.mailspike.net] X-Debbugs-Envelope-To: 40815 Cc: Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= , 40815@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 1.0 (+) This is a multipart message in MIME format. ------_=_495d421c51d8a8da7ac9a4b0_=_ MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----_=_1defda244969b2502f62988b_=_" This is a multipart message in MIME format. ------_=_1defda244969b2502f62988b_=_ Content-Type: text/plain; charset=UTF-8 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable > Note the book could also go into another package, once texlive-amsfonts i= s > fixed. Interesting. Either way it's a similarly sized patch, so I'm curious why a "metamath-doc" packages would be preferable to a "metamath:doc" output. > Meanwhile, I think we can remove the comments in this one and apply it. >=20 > WDYT? Sure. You intuition on what is best for the repo is certainly more honed th= an mine. Would you mind sharing your reasoning for deleting the comments thoug= h? Not sure I see why. My thinking was this: want want a "doc" output if possible; the work of creating that is already done; so we might as well make that work available= =2E Are you mostly trying to avoid comment clutter? Either way, the patch I included here strips out the comments. > I don't have enough knowledge to comment LaTeX packages. I suggest to > submit them as separate issues. If still no one comments of them, I'll > apply them later. Great. I'll do that. Thanks. Cheers! ------_=_1defda244969b2502f62988b_=_ Content-Disposition: attachment; filename=0001-gnu-Add-metamath.patch Content-Type: text/x-patch Content-Transfer-Encoding: quoted-printable =46rom 4d94ad11b0e998a9510708e088a4c5eb63919b3b Mon Sep 17 00:00:00 2001 =46rom: "B. Wilson" =44ate: Mon, 11 May 2020 20:10:48 +0900 =53ubject: [PATCH] gnu: Add metamath. =54o: guix-patches@gnu.org =0A* gnu/packages/maths.scm (metamath): New variable. =2D-- =20gnu/packages/maths.scm | 37 +++++++++++++++++++++++++++++++++++++ =201 file changed, 37 insertions(+) =0Adiff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm =69ndex 45d699e39c..02109ced2d 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@ -5686,3 +5687,39 @@ and conversions, physical constants, symbolic calc= =75lations (including =20integrals and equations), arbitrary precision, uncertainity propagation,= =0A interval arithmetic, plotting.") =20 (license license:gpl2+))) =2B =2B(define-public metamath =2B ;; Upstream pushed a commit on top of v0.182 that fixes a bug in Makef= =69le.am. =2B ;; Using this commit lets us avoid directly including the patch here. = =20In the =2B ;; next version bump, we should be able to replace this and directly u= =73e the =2B ;; version tag. =2B (let ((commit "5df616efe4119ff88daf77e7041d45b6fa39c578") =2B (revision "0") =2B (book-name "metamath-book") =2B (book-version "second_edition")) =2B (package =2B (name "metamath") =2B (version (git-version "0.182" revision commit)) =2B (source =2B (origin =2B (method git-fetch) =2B (uri (git-reference =2B (url "https://github.com/metamath/metamath-exe.git") =2B (commit commit))) =2B (sha256 =2B (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"= =29) =2B (file-name (git-file-name name version)))) =2B (build-system gnu-build-system) =2B (native-inputs `(("autoconf" ,autoconf) =2B ("automake" ,automake))) =2B (home-page "http://us.metamath.org/") =2B (synopsis "Proof verifier based on a minimalistic formalism") =2B (description "Metamath is a tiny formal language and that can expr= =65ss =2Btheorems in abstract mathematics, with an accompyaning @code{metamath} =2Bexecutable that verifies databases of these proofs. There is a public =2Bdatabase, @url{https://github.com/metamath/set.mm, set.mm}, implementing= =0A+first-order logic and Zermelo-Frenkel set theory with Choice, along wit= =68 a =2Blarge swath of associated, high-level theorems, e.g.@: the Fundamental T= =68eorem =2Bof Arithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc. = =53ee the =2BMetamath book.") =2B (license license:gpl2+)))) =2D-=20 =32.27.0 =0A= ------_=_1defda244969b2502f62988b_=_-- ------_=_495d421c51d8a8da7ac9a4b0_=_ Content-Disposition: attachment; filename=signature.asc Content-Type: application/pgp-signature Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- iI0EABYIADUWIQQ7FdZn/PDWvxE6cmR2pStZ7i7CgQUCXvW13BccZWxhZXh1b3Rl ZUB3aWxzb25iLmNvbQAKCRB2pStZ7i7CgQsXAQDdp+p5qOEslcSH303tZnvUvM7s oBcAWYRjSogK4e1GegD+OInlIjcAG5HoCnpvHk54DOlrwGIzz43Oaj8IbrRBgQY= =ila0 -----END PGP SIGNATURE----- ------_=_495d421c51d8a8da7ac9a4b0_=_-- From debbugs-submit-bounces@debbugs.gnu.org Sun Jun 28 16:12:25 2020 Received: (at 40815) by debbugs.gnu.org; 28 Jun 2020 20:12:25 +0000 Received: from localhost ([127.0.0.1]:47014 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jpdf7-0004sq-2z for submit@debbugs.gnu.org; Sun, 28 Jun 2020 16:12:25 -0400 Received: from relay11.mail.gandi.net ([217.70.178.231]:50619) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jpdf1-0004sY-D4 for 40815@debbugs.gnu.org; Sun, 28 Jun 2020 16:12:23 -0400 Received: from localhost (40-67.ipv4.commingeshautdebit.fr [185.131.40.67]) (Authenticated sender: admin@nicolasgoaziou.fr) by relay11.mail.gandi.net (Postfix) with ESMTPSA id 41510100002; Sun, 28 Jun 2020 20:12:12 +0000 (UTC) From: Nicolas Goaziou To: elaexuotee@wilsonb.com Subject: Re: [bug#40815] gnu: Add metamath References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> <20200426172945.7ez6i2fl3pjcoexd@gravity> <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com> <20200427121248.cga7p43flnusf7zo@gravity> <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com> <25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com> <87d06eraaf.fsf@nicolasgoaziou.fr> <23UB7VNWCB6BC.23I1T2MHNG4ZI@wilsonb.com> <878sgas38j.fsf@nicolasgoaziou.fr> <2Z19F0HU7SZNL.33AMEA6BFHCFT@wilsonb.com> Date: Sun, 28 Jun 2020 22:12:09 +0200 In-Reply-To: <2Z19F0HU7SZNL.33AMEA6BFHCFT@wilsonb.com> (elaexuotee@wilsonb.com's message of "Fri, 26 Jun 2020 17:46:22 +0900") Message-ID: <87k0zrvtk6.fsf@nicolasgoaziou.fr> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: -0.7 (/) X-Debbugs-Envelope-To: 40815 Cc: Jakub =?utf-8?B?S8SFZHppb8WCa2E=?= , 40815@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.7 (-) Hello, elaexuotee@wilsonb.com writes: >> Note the book could also go into another package, once texlive-amsfonts is >> fixed. > > Interesting. Either way it's a similarly sized patch, so I'm curious why a > "metamath-doc" packages would be preferable to a "metamath:doc" > output. The book looks like a related project to metamath, like advanced documentation, not like a regular manual. I didn't read it, so it is just a guess. Anyway, I only suggested it as another option to consider. Feel free to ignore it. > Sure. You intuition on what is best for the repo is certainly more honed than > mine. Would you mind sharing your reasoning for deleting the comments though? > Not sure I see why. > > My thinking was this: want want a "doc" output if possible; the work of > creating that is already done; so we might as well make that work available. > Are you mostly trying to avoid comment clutter? I do. In any case, if you want to keep them, they need to start with two semicolons, not a single one. WDYT? Regards, -- Nicolas Goaziou From debbugs-submit-bounces@debbugs.gnu.org Mon Jun 29 03:10:14 2020 Received: (at 40815) by debbugs.gnu.org; 29 Jun 2020 07:10:14 +0000 Received: from localhost ([127.0.0.1]:47597 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jpnvh-0004RW-LT for submit@debbugs.gnu.org; Mon, 29 Jun 2020 03:10:14 -0400 Received: from m42-5.mailgun.net ([69.72.42.5]:59617) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jpnve-0004RB-Q6 for 40815@debbugs.gnu.org; Mon, 29 Jun 2020 03:10:11 -0400 DKIM-Signature: a=rsa-sha256; v=1; c=relaxed/relaxed; d=mg.wilsonb.com; q=dns/txt; s=krs; t=1593414611; h=Content-Type: MIME-Version: Message-Id: In-Reply-To: References: Subject: From: Cc: To: Date: Sender; bh=Fzwwx9370ga1BRrn9FP9NPi3099epSCfT63ZFkRl5nk=; b=HHy6a2vVCLoCC+yLM9jNLfCL15AX0PbRqbfH/Zkp6SjtdRwrt+kVZ0Nomz5L7qfDR4ajI7Td APVIGmFW1H6RSIUjbANbw71x+suKtaKzhZtQauC8ui9rJzYoHhnfa+pejg5WTwOJrNRVgSw6 2HUoBjY5w3uHTlq/WqYvfqAMJA2y67GBGZwP5kMFAl4K3ficEpDIjTXi3Pm3Kg0T0jSZ19P3 +UHPFZRjrNcZEBDnMHW2qsTtyl/r2JUFHj97FIe/fMHvtY7neDwMPWdAm3+kDAECGLxopajm VlNKptInOYf5RPq8zvJg9/4ES8E0HQ7GZUDG9gnFIM05zkC+1aaCZw== X-Mailgun-Sending-Ip: 69.72.42.5 X-Mailgun-Sid: WyIxOGZjZiIsICI0MDgxNUBkZWJidWdzLmdudS5vcmciLCAiMDg1NDdhIl0= Received: from wilsonb.com (wilsonb.com [104.199.203.42]) by smtp-out-n12.prod.us-west-2.postgun.com with SMTP id 5ef993cc6f2ee827da274a4c (version=TLS1.3, cipher=TLS_AES_128_GCM_SHA256); Mon, 29 Jun 2020 07:10:04 GMT Received: from localhost (KD111239210180.au-net.ne.jp [111.239.210.180]) by wilsonb.com (Postfix) with ESMTPSA id 52981A1A42; Mon, 29 Jun 2020 07:10:01 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wilsonb.com; s=201703; t=1593414601; bh=Fzwwx9370ga1BRrn9FP9NPi3099epSCfT63ZFkRl5nk=; h=Date:To:Cc:From:Subject:References:In-Reply-To:From; b=Tx0ax26grr8QPZtzknog0auvC31eWufM5UOloExJPrMqLNZ6w5LVKYKXVrvg26JKD 7iSEzMphnc2m4/GoesCIBPiIU1WbMjF67yqu0Uc7hMbnruCbUTGbjT1UURuvqt8mSL 0y/jgWO1vdHo95GiDo406PhYSl6omDGy5HHroSXLVVe391rWXdtrPl+ZR20XBHhUwZ 4vlOxym66VdZMX7HPN+UMgDst59UMPwtxCCh2GessrUNjoJ7V+yDLK9GpTURYt5VWq fFpyOc4j0uCPhjw/u1o9OWMnWiFSUATsC6PqybS8F6vY8xt2lbIh+8pwg3X6qc6DD2 dkmYYi0Zqwf7weWUdFB7f/wzg+FVoyGu9KfXbDGpor2FZ9Xhz1F3NAGYYVynalKDbf vppKRf2CeQY+kQEsz9K27VHMM8EijX9WtH00ySL+umb4VJJtcn1pMWyfE7bN2CZS3x srW6+l7j6Y/E3RF7sYVVGch+n16weSQxZo0Ck3K1Sw7skwAP0RVKWmw4AhFqwR3vpv VFWDkrDXUjoKsTW5x85QBthHgdGuYMvw8DbyeHjBdcQLKP06BpF+18GOkylqVgJL5p yt5KyI+g1Egas6cV9alcvwd4+fZSN/g/EO2cnIzKkbAekK9k1iqALSkJrp10W3n73G U8ZUBra9FbQuLJr+rVgwa7g4= Date: Mon, 29 Jun 2020 16:09:57 +0900 To: Nicolas Goaziou From: elaexuotee@wilsonb.com Subject: Re: [bug#40815] gnu: Add metamath References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> <20200426172945.7ez6i2fl3pjcoexd@gravity> <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com> <20200427121248.cga7p43flnusf7zo@gravity> <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com> <25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com> <87d06eraaf.fsf@nicolasgoaziou.fr> <23UB7VNWCB6BC.23I1T2MHNG4ZI@wilsonb.com> <878sgas38j.fsf@nicolasgoaziou.fr> <2Z19F0HU7SZNL.33AMEA6BFHCFT@wilsonb.com> <87k0zrvtk6.fsf@nicolasgoaziou.fr> In-Reply-To: <87k0zrvtk6.fsf@nicolasgoaziou.fr> Message-Id: <3DWRMY6FLHG65.2WHMN0WRGUE63@wilsonb.com> User-Agent: mblaze/0.7 MIME-Version: 1.0 Content-Type: multipart/signed; micalg="pgp-sha1"; protocol="application/pgp-signature"; boundary="----_=_325dd5287a9b06e46e7bf2ef_=_" X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 40815 Cc: Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= , 40815@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) This is a multipart message in MIME format. ------_=_325dd5287a9b06e46e7bf2ef_=_ MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----_=_38043db35e3d96bb4ac8a7c2_=_" This is a multipart message in MIME format. ------_=_38043db35e3d96bb4ac8a7c2_=_ Content-Type: text/plain; charset=UTF-8 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Hell, Thanks for the quick turnaround. > The book looks like a related project to metamath, like advanced > documentation, not like a regular manual. I didn't read it, so it is > just a guess. Oh, okay. That makes sense. PDF as official documentation is certainly stra= nge for what looks like a cli program. In this case, it just happens that this = is the only reasonable documentation, aparth from the website, for using and understanding Metamath proofs. > I do. In any case, if you want to keep them, they need to start with two > semicolons, not a single one. >=20 > WDYT? I trust your initial impression on this one. Let's use the patch from my previous email that excises the commented out code. Does it look reasonable= ? Cheers. ------_=_38043db35e3d96bb4ac8a7c2_=_-- ------_=_325dd5287a9b06e46e7bf2ef_=_ Content-Disposition: attachment; filename=signature.asc Content-Type: application/pgp-signature Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- iI0EABYIADUWIQQ7FdZn/PDWvxE6cmR2pStZ7i7CgQUCXvmTwBccZWxhZXh1b3Rl ZUB3aWxzb25iLmNvbQAKCRB2pStZ7i7CgXEYAP98w7kcM4QTASjmbGISdN+/VghL eva/Llu66KJVKut1ewD+KmNMLZtaoRTvkMVVy1wzmEhWvamDOsiNsC0YN8DrFQk= =RjJ1 -----END PGP SIGNATURE----- ------_=_325dd5287a9b06e46e7bf2ef_=_-- From debbugs-submit-bounces@debbugs.gnu.org Wed Jul 01 07:02:51 2020 Received: (at 40815-done) by debbugs.gnu.org; 1 Jul 2020 11:02:51 +0000 Received: from localhost ([127.0.0.1]:52370 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jqaVv-00043i-Gq for submit@debbugs.gnu.org; Wed, 01 Jul 2020 07:02:51 -0400 Received: from relay4-d.mail.gandi.net ([217.70.183.196]:57857) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jqaVs-00043T-JS for 40815-done@debbugs.gnu.org; Wed, 01 Jul 2020 07:02:49 -0400 X-Originating-IP: 185.131.40.67 Received: from localhost (40-67.ipv4.commingeshautdebit.fr [185.131.40.67]) (Authenticated sender: admin@nicolasgoaziou.fr) by relay4-d.mail.gandi.net (Postfix) with ESMTPSA id 75706E0006; Wed, 1 Jul 2020 11:02:41 +0000 (UTC) From: Nicolas Goaziou To: elaexuotee@wilsonb.com Subject: Re: [bug#40815] gnu: Add metamath References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> <20200426172945.7ez6i2fl3pjcoexd@gravity> <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com> <20200427121248.cga7p43flnusf7zo@gravity> <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com> <25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com> <87d06eraaf.fsf@nicolasgoaziou.fr> <23UB7VNWCB6BC.23I1T2MHNG4ZI@wilsonb.com> <878sgas38j.fsf@nicolasgoaziou.fr> <2Z19F0HU7SZNL.33AMEA6BFHCFT@wilsonb.com> <87k0zrvtk6.fsf@nicolasgoaziou.fr> <3DWRMY6FLHG65.2WHMN0WRGUE63@wilsonb.com> Date: Wed, 01 Jul 2020 13:02:37 +0200 In-Reply-To: <3DWRMY6FLHG65.2WHMN0WRGUE63@wilsonb.com> (elaexuotee@wilsonb.com's message of "Mon, 29 Jun 2020 16:09:57 +0900") Message-ID: <87a70jfqgi.fsf@nicolasgoaziou.fr> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: -0.7 (/) X-Debbugs-Envelope-To: 40815-done Cc: Jakub =?utf-8?B?S8SFZHppb8WCa2E=?= , 40815-done@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.7 (-) Hello, elaexuotee@wilsonb.com writes: > I trust your initial impression on this one. Let's use the patch from my > previous email that excises the commented out code. Does it look > reasonable? Certainly. I removed the book-revision and book-version bindings, since they were not used in the current package definition, tweaked a bit the description, and applied your patch. I hope we can have the book either as a doc output, or as a separate package, bundled at some point. Meanwhile, I'm closing this bug report. Regards, -- Nicolas Goaziou From debbugs-submit-bounces@debbugs.gnu.org Wed Jul 01 19:54:41 2020 Received: (at 40815-done) by debbugs.gnu.org; 1 Jul 2020 23:54:41 +0000 Received: from localhost ([127.0.0.1]:53957 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jqmYq-0001t7-VO for submit@debbugs.gnu.org; Wed, 01 Jul 2020 19:54:41 -0400 Received: from m42-5.mailgun.net ([69.72.42.5]:47201) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jqmYj-0001sn-Vu for 40815-done@debbugs.gnu.org; Wed, 01 Jul 2020 19:54:40 -0400 DKIM-Signature: a=rsa-sha256; v=1; c=relaxed/relaxed; d=mg.wilsonb.com; q=dns/txt; s=krs; t=1593647676; h=Content-Type: MIME-Version: Message-Id: In-Reply-To: References: From: Subject: From: Cc: To: Date: Sender; bh=cHEWuKmTP78YJy/L3LGlXr/EBiYqL8jgi/FSbT2TmfU=; b=Z50BDadBefunXlDLyTxg9TiZ8N12K7hXJ2Dd/HXs7E0eWhHKq6D1kVM6JDi2/ZzDN8hVefXo TBU4PDPtW+3gDF4Jyz9wzsxDQrymVg0VY3NB6+c2bmxfpZZ2Rpa7MBO0IQMBc0V49wzWuOpA bBUBPake8K/yH8sddqE+IY0HWBCisVxFHslcjtqTISYXOp64vyQrdistp4P/ovUNaN59/Lh0 h75GNke9ItYHg5hraivWcyUH1YwAIf9LVo/2GP1O7izTbOq0BOvtCqSYBfnXjrCI4eSDfr/6 pMKWaYvUsPIaaVO56zcxWBDqKghB/UViJb+ZXCL5NgaM597uQ9DWug== X-Mailgun-Sending-Ip: 69.72.42.5 X-Mailgun-Sid: WyIxYzVlNyIsICI0MDgxNS1kb25lQGRlYmJ1Z3MuZ251Lm9yZyIsICIwODU0N2EiXQ== Received: from wilsonb.com (wilsonb.com [104.199.203.42]) by smtp-out-n12.prod.us-east-1.postgun.com with SMTP id 5efd221ca3d8a447434a62bd (version=TLS1.3, cipher=TLS_AES_128_GCM_SHA256); Wed, 01 Jul 2020 23:54:04 GMT Received: from localhost (KD111239198085.au-net.ne.jp [111.239.198.85]) by wilsonb.com (Postfix) with ESMTPSA id 25294A2C23; Wed, 1 Jul 2020 23:54:02 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wilsonb.com; s=201703; t=1593647642; bh=cHEWuKmTP78YJy/L3LGlXr/EBiYqL8jgi/FSbT2TmfU=; h=Date:To:Cc:From:Subject:From:References:In-Reply-To:From; b=LEvajdVNw37yuSDl672NrcLXDpaDp+RRbWsUbBD8PYKAAdBuEMlqupuo7fEWSYoWJ a5HCKEgVdSFZv8Y7ItmwjQyS5n/DPCJfIywoFTRSpsQgiC6c6dpLgCkD+vPO0Spa80 EQgSaiL2yHcCeSgd5le59WcSv4fAgGZDqGPn9oF1vUPWZ6vd3QFOaHuw2gzOavF5OJ TYZCNraWKPG663VTANiweXb6hzv+RJlpXaMiAdT4tfJEeQUwlgyPK7diY5XwnpQheA csDzHvGsKCbPSH+S3iNnNL7kERDVjd96x5TK0HucDOU9NjbpPDEANaJ3dn1LGYaylB 41HXFCXdlVV9hW8BsKFqC6BrUbeIGp19i5b2tiEI3mquLMgcSct6iEf5glLxNoQm6Y ZJUfB12KEBrYK8Iy6g1xDfui2xgcw6l5hMl2CUXM33JKy2fO9BptJStGEPiWfEVSvl /LI84Gt3mOPhtaxHgDhDvKnSg2/ROVT7bq8uw3zmrDr+yy9hplKCEAJYakFh07TdXa iQKrPN+m8YKTMhiJykiHE8SWszJu0k2VOKuaWpyGSCjax3JB7U6lJqP+eZS3UV3WGm j8TmvGAE2FrSdPNcCW+mMzIpSgjxSLwhNS+VpiiiSAnFchrIGdrBxAy7GTlo4lbyhI cDOAc57F0t0ypd1jKfN5L4wI= Date: Thu, 02 Jul 2020 08:53:59 +0900 To: Nicolas Goaziou From: elaexuotee@wilsonb.com Subject: Re: [bug#40815] gnu: Add metamath From: x@wilsonb.com References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> <20200426172945.7ez6i2fl3pjcoexd@gravity> <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com> <20200427121248.cga7p43flnusf7zo@gravity> <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com> <25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com> <87d06eraaf.fsf@nicolasgoaziou.fr> <23UB7VNWCB6BC.23I1T2MHNG4ZI@wilsonb.com> <878sgas38j.fsf@nicolasgoaziou.fr> <2Z19F0HU7SZNL.33AMEA6BFHCFT@wilsonb.com> <87k0zrvtk6.fsf@nicolasgoaziou.fr> <3DWRMY6FLHG65.2WHMN0WRGUE63@wilsonb.com> <87a70jfqgi.fsf@nicolasgoaziou.fr> In-Reply-To: <87a70jfqgi.fsf@nicolasgoaziou.fr> Message-Id: <208YMDGHVVTI7.1Z7R2582RUM50@wilsonb.com> User-Agent: mblaze/0.7 MIME-Version: 1.0 Content-Type: multipart/signed; micalg="pgp-sha1"; protocol="application/pgp-signature"; boundary="----_=_2640c5e23a6557f83213f586_=_" X-Spam-Score: 0.8 (/) X-Debbugs-Envelope-To: 40815-done Cc: Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= , 40815-done@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.2 (/) This is a multipart message in MIME format. ------_=_2640c5e23a6557f83213f586_=_ MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----_=_7b5b7a001931181c325fe607_=_" This is a multipart message in MIME format. ------_=_7b5b7a001931181c325fe607_=_ Content-Type: text/plain; charset=UTF-8 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Excellent. Thanks for cleaning up the things I missed and pushing. Nicolas Goaziou wrote: > Hello, >=20 > elaexuotee@wilsonb.com writes: >=20 > > I trust your initial impression on this one. Let's use the patch from m= y > > previous email that excises the commented out code. Does it look > > reasonable? >=20 > Certainly. I removed the book-revision and book-version bindings, since > they were not used in the current package definition, tweaked a bit the > description, and applied your patch. >=20 > I hope we can have the book either as a doc output, or as a separate > package, bundled at some point. Meanwhile, I'm closing this bug report. >=20 > Regards, ------_=_7b5b7a001931181c325fe607_=_-- ------_=_2640c5e23a6557f83213f586_=_ Content-Disposition: attachment; filename=signature.asc Content-Type: application/pgp-signature Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- iI0EABYIADUWIQQ7FdZn/PDWvxE6cmR2pStZ7i7CgQUCXv0iEhccZWxhZXh1b3Rl ZUB3aWxzb25iLmNvbQAKCRB2pStZ7i7CgUNEAQCw6PT9jZVrNaM2smDtqvEN1qcU FPHx+aSFo6OZkVNw1wD+M9HYtosLfDuAvgTtVSsxMCG7Hwz40T2maSmgTsURlAw= =MGlR -----END PGP SIGNATURE----- ------_=_2640c5e23a6557f83213f586_=_-- From unknown Mon Aug 18 11:21:50 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Thu, 30 Jul 2020 11:24:04 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator