diff options
Diffstat (limited to 'gnu/packages/maths.scm')
| -rw-r--r-- | gnu/packages/maths.scm | 45 |
1 files changed, 45 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+))) |