From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp2 ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms11 with LMTPS id YOT1AXno8V6+EgAA0tVLHw (envelope-from ) for ; Tue, 23 Jun 2020 11:33:13 +0000 Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp2 with LMTPS id 4LlyOXjo8V4kXQAAB5/wlQ (envelope-from ) for ; Tue, 23 Jun 2020 11:33:12 +0000 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id 20689940990 for ; Tue, 23 Jun 2020 11:33:12 +0000 (UTC) Received: from localhost ([::1]:53022 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1jnhAr-00018T-AE for larch@yhetil.org; Tue, 23 Jun 2020 07:33:09 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:41512) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1jnhAk-00017k-1n for guix-patches@gnu.org; Tue, 23 Jun 2020 07:33:02 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:52274) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1jnhAj-0008OC-Nt for guix-patches@gnu.org; Tue, 23 Jun 2020 07:33:01 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1jnhAj-0004yv-LF for guix-patches@gnu.org; Tue, 23 Jun 2020 07:33:01 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#40815] gnu: Add metamath Resent-From: elaexuotee@wilsonb.com Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Tue, 23 Jun 2020 11:33:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 40815 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: To: Nicolas Goaziou Cc: , Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= , 40815@debbugs.gnu.org Received: via spool by 40815-submit@debbugs.gnu.org id=B40815.159291197419136 (code B ref 40815); Tue, 23 Jun 2020 11:33:01 +0000 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 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-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-Spam-Score: 1.0 (+) X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: "Guix-patches" Reply-to: elaexuotee@wilsonb.com, elaexuotee--- via Guix-patches From: elaexuotee--- via Guix-patches via X-Scanner: scn0 Authentication-Results: aspmx1.migadu.com; dkim=fail (rsa verify failed) header.d=mg.wilsonb.com header.s=krs header.b=s8REuDcP; dkim=fail (rsa verify failed) header.d=wilsonb.com header.s=201703 header.b=0HIkxt2a; dmarc=none; spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org X-Spam-Score: -2.11 X-TUID: SSRn7RP1Aupb 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_=_--