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