From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp1 ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms11 with LMTPS id gEBSFWmp8l4WJgAA0tVLHw (envelope-from ) for ; Wed, 24 Jun 2020 01:16:25 +0000 Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp1 with LMTPS id MDMiEWmp8l7MNQAAbx9fmQ (envelope-from ) for ; Wed, 24 Jun 2020 01:16:25 +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 7B8459403D3 for ; Wed, 24 Jun 2020 01:16:24 +0000 (UTC) Received: from localhost ([::1]:37044 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1jnu1V-0002NS-TO for larch@yhetil.org; Tue, 23 Jun 2020 21:16:21 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:48726) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1jnu1C-0002N4-4p for guix-patches@gnu.org; Tue, 23 Jun 2020 21:16:02 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:54143) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1jnu1B-0005MR-SP for guix-patches@gnu.org; Tue, 23 Jun 2020 21:16:01 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1jnu1B-00063I-NH for guix-patches@gnu.org; Tue, 23 Jun 2020 21:16: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: Wed, 24 Jun 2020 01:16: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.159296131323203 (code B ref 40815); Wed, 24 Jun 2020 01:16:01 +0000 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 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-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=PBq+mVsI; dkim=fail (rsa verify failed) header.d=wilsonb.com header.s=201703 header.b=J7TITzrL; 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: YB58JfkmcIpj 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_=_--