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 6Ol4Mg+29V6DNAAA0tVLHw (envelope-from ) for ; Fri, 26 Jun 2020 08:47:11 +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 kMIVLg+29V51XQAAbx9fmQ (envelope-from ) for ; Fri, 26 Jun 2020 08:47:11 +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 27F4594066D for ; Fri, 26 Jun 2020 08:47:11 +0000 (UTC) Received: from localhost ([::1]:35280 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1jok0q-0005Ga-GV for larch@yhetil.org; Fri, 26 Jun 2020 04:47:08 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:47562) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1jok0k-0005GE-Jd for guix-patches@gnu.org; Fri, 26 Jun 2020 04:47:02 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:58491) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1jok0k-0004cT-Aq for guix-patches@gnu.org; Fri, 26 Jun 2020 04:47:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1jok0k-0004md-8F for guix-patches@gnu.org; Fri, 26 Jun 2020 04:47:02 -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: Fri, 26 Jun 2020 08:47:02 +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.159316122018376 (code B ref 40815); Fri, 26 Jun 2020 08:47:02 +0000 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 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-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=ay9btskv; dkim=fail (rsa verify failed) header.d=wilsonb.com header.s=201703 header.b=1e2H9Kiq; 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: -0.61 X-TUID: ALVMVxHvaSfy 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_=_--