From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from eggs.gnu.org ([2001:470:142:3::10]:53878)
 by lists.gnu.org with esmtp (Exim 4.90_1)
 (envelope-from <Debian-debbugs@debbugs.gnu.org>) id 1jRwv9-0001CJ-GV
 for guix-patches@gnu.org; Fri, 24 Apr 2020 07:55:08 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.90_1)
 (envelope-from <Debian-debbugs@debbugs.gnu.org>) id 1jRwv8-0002q3-N9
 for guix-patches@gnu.org; Fri, 24 Apr 2020 07:55:03 -0400
Received: from debbugs.gnu.org ([209.51.188.43]:45052)
 by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
 (Exim 4.90_1) (envelope-from <Debian-debbugs@debbugs.gnu.org>)
 id 1jRwv8-0002pY-BC
 for guix-patches@gnu.org; Fri, 24 Apr 2020 07:55:02 -0400
Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2)
 (envelope-from <Debian-debbugs@debbugs.gnu.org>) id 1jRwv8-0006hs-2H
 for guix-patches@gnu.org; Fri, 24 Apr 2020 07:55:02 -0400
Subject: [bug#40815] gnu: Add metamath
Resent-Message-ID: <handler.40815.B.158772925425721@debbugs.gnu.org>
Received: from eggs.gnu.org ([2001:470:142:3::10]:53154)
 by lists.gnu.org with esmtp (Exim 4.90_1)
 (envelope-from <bounce+686de0.08547a-guix-patches=gnu.org@mg.wilsonb.com>)
 id 1jRwty-00017X-CH
 for guix-patches@gnu.org; Fri, 24 Apr 2020 07:53:54 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.90_1)
 (envelope-from <bounce+686de0.08547a-guix-patches=gnu.org@mg.wilsonb.com>)
 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 <bounce+686de0.08547a-guix-patches=gnu.org@mg.wilsonb.com>)
 id 1jRwtw-0007ez-DH
 for guix-patches@gnu.org; Fri, 24 Apr 2020 07:53:48 -0400
Received: from localhost (KD111239206026.au-net.ne.jp [111.239.206.26])
 by wilsonb.com (Postfix) with ESMTPSA id 4E6B0A1A70
 for <guix-patches@gnu.org>; Fri, 24 Apr 2020 11:48:42 +0000 (UTC)
Date: Fri, 24 Apr 2020 20:48:30 +0900
Message-Id: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com>
MIME-Version: 1.0
Content-Type: multipart/signed; micalg="pgp-sha1";
 protocol="application/pgp-signature";
 boundary="----_=_61af54047ea067b0308e476b_=_"
List-Id: <guix-patches.gnu.org>
List-Unsubscribe: <https://lists.gnu.org/mailman/options/guix-patches>,
 <mailto:guix-patches-request@gnu.org?subject=unsubscribe>
List-Archive: <https://lists.gnu.org/archive/html/guix-patches>
List-Post: <mailto:guix-patches@gnu.org>
List-Help: <mailto:guix-patches-request@gnu.org?subject=help>
List-Subscribe: <https://lists.gnu.org/mailman/listinfo/guix-patches>,
 <mailto:guix-patches-request@gnu.org?subject=subscribe>
Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org
Sender: "Guix-patches" <guix-patches-bounces+kyle=kyleam.com@gnu.org>
Reply-to: "B. Wilson" <elaexuotee@wilsonb.com>, "B. Wilson via Guix-patches" <guix-patches@gnu.org>
From: "B. Wilson via Guix-patches" via <guix-patches@gnu.org>
To: 40815@debbugs.gnu.org

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/<hash>-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" <elaexuotee@wilsonb.com>
=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 <vkor@vkten.in>
=20;;; Copyright =C2=A9 2020 Vincent Legoll <vincent.legoll@gmail.com>
=20;;; Copyright =C2=A9 2020 Nicol=C3=B2 Balzarotti <nicolo@nixo.xyz>
=2B;;; Copyright =C2=A9 2020 B. Wilson <elaexuotee@wilsonb.com>
=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_=_--