[bug#40815] gnu: Add metamath

["B. Wilson via Guix-patches" via <guix-patches@gnu.org>]

[-- Attachment #1.1: Type: text/plain, Size: 753 bytes --]


This is my first packaging attempt, so careful critiques are very welcome.

The package definition itself is pretty bog standard, apart from how the "doc" output is supplied. Upstream provides the official documentation as a pdf offered separately from the source. I decided to include this as an input and manually copy it over. Upstream does also have a repo with the TeX sources. Would it be better to typset it directly instead?

Also, regarding my `install-doc' phase, is the way I copy over the /gnu/store/<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!


[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1.2: 0001-gnu-Add-metamath.patch --]
[-- Type: text/x-patch, Size: 3939 bytes --]

From 808e8d73cb231d2fbf34b88683fb0c3fe5d631e9 Mon Sep 17 00:00:00 2001
From: "B. Wilson" <elaexuotee@wilsonb.com>
Date: Thu, 23 Apr 2020 20:28:49 +0900
Subject: [PATCH] gnu: Add metamath

* gnu/packages/maths.scm (metamath): New variable.
* gnu/packages/patches/metamath-remove-missing-file-refs.patch: New file.
---
 gnu/packages/maths.scm                        | 45 +++++++++++++++++++
 .../metamath-remove-missing-file-refs.patch   | 17 +++++++
 2 files changed, 62 insertions(+)
 create mode 100644 gnu/packages/patches/metamath-remove-missing-file-refs.patch

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 73ee161e81..c70557ef8f 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -38,6 +38,7 @@
 ;;; Copyright © 2020 R Veera Kumar <vkor@vkten.in>
 ;;; Copyright © 2020 Vincent Legoll <vincent.legoll@gmail.com>
 ;;; Copyright © 2020 Nicolò Balzarotti <nicolo@nixo.xyz>
+;;; Copyright © 2020 B. Wilson <elaexuotee@wilsonb.com>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -5519,3 +5520,47 @@ and conversions, physical constants, symbolic calculations (including
 integrals and equations), arbitrary precision, uncertainity propagation,
 interval arithmetic, plotting.")
     (license license:gpl2+)))
+
+(define-public metamath
+  (package
+    (name "metamath")
+    (version "0.182")
+    (source
+     (origin
+       (method url-fetch)
+       (uri "http://us2.metamath.org/downloads/metamath-program.zip")
+       (sha256
+        (base32 "0k1ffd1bglkgdb6pkjnxw3dc7p697x70nx8hcpvw9cwbv3k9vf71"))
+       (patches (search-patches "metamath-remove-missing-file-refs.patch"))))
+    (build-system gnu-build-system)
+    (inputs
+     `(("book"
+        ,(origin
+           (method url-fetch)
+           (uri "http://us2.metamath.org/downloads/metamath.pdf")
+           (sha256
+            (base32 "0nc0dz2zk8n2yija8qdvdgnmpqafyfl1nxf3yrr9g2hldnqvlpi4"))))))
+    (native-inputs `(("autoconf" ,autoconf)
+                     ("automake" ,automake)
+                     ("unzip" ,unzip)))
+    (outputs '("out" "doc"))
+    (arguments
+     `(#:phases
+       (modify-phases %standard-phases
+         (add-after 'install 'install-doc
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             (mkdir-p (string-append (assoc-ref outputs "doc") "/share/doc"))
+             (copy-file (assoc-ref inputs "book")
+                        (string-append (assoc-ref outputs "doc")
+                                       "/share/doc/metamath.pdf")))))))
+    (home-page "http://us.metamath.org/")
+    (synopsis "Proof verifier based on a minimalistic formalism")
+    (description "Metamath is a tiny formal language and that can express
+theorems in abstract mathematics, with an accompyaning @code{metamath}
+executable that verifies databases of these proofs.  There is a public
+database, @url{https://github.com/metamath/set.mm, set.mm}, implementing
+first-order logic and Zermelo-Frenkel set theory with Choice, along with a
+large swath of associated, high-level theorems, e.g. the Fundamental Theorem of
+Arithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc.  See the
+Metamath book")
+    (license license:gpl2+)))
diff --git a/gnu/packages/patches/metamath-remove-missing-file-refs.patch b/gnu/packages/patches/metamath-remove-missing-file-refs.patch
new file mode 100644
index 0000000000..bc4748de98
--- /dev/null
+++ b/gnu/packages/patches/metamath-remove-missing-file-refs.patch
@@ -0,0 +1,17 @@
+--- metamath.orig/Makefile.am	2020-01-27 20:43:55.650195602 +0900
++++ metamath/Makefile.am	2020-01-27 20:44:18.876578014 +0900
+@@ -36,14 +36,6 @@
+ 	mmwtex.c \
+ 	$(noinst_HEADERS)
+ 
+-dist_pkgdata_DATA = \
+-	big-unifier.mm \
+-	demo0.mm \
+-	miu.mm \
+-	peano.mm \
+-	ql.mm \
+-	set.mm
+-
+ 
+ EXTRA_DIST = \
+ 	LICENSE.TXT \
-- 
2.26.2


[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 260 bytes --]