aboutsummaryrefslogtreecommitdiff
path: root/gnu
diff options
context:
space:
mode:
Diffstat (limited to 'gnu')
-rw-r--r--gnu/packages/maths.scm45
-rw-r--r--gnu/packages/patches/metamath-remove-missing-file-refs.patch17
2 files changed, 62 insertions, 0 deletions
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 \