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_=_--