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 ) 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 ) 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 ) 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 ) 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: Received: from eggs.gnu.org ([2001:470:142:3::10]:53154) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) 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 ) 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 ) 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 ; 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: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" Reply-to: "B. Wilson" , "B. Wilson via Guix-patches" From: "B. Wilson via Guix-patches" via 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/-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" =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 =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@ -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_=_--