diff options
Diffstat (limited to 'gnu/packages')
| -rw-r--r-- | gnu/packages/maths.scm | 45 | ||||
| -rw-r--r-- | gnu/packages/patches/metamath-remove-missing-file-refs.patch | 17 |
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 \ |