branch master updated: gnu: Add metamath.

[guix-commits]

This is an automated email from the git hooks/post-receive script.

ngz pushed a commit to branch master
in repository guix.

The following commit(s) were added to refs/heads/master by this push:
     new d277c00  gnu: Add metamath.
d277c00 is described below

commit d277c00ec942b7eb52f918b5e17c043e95fef27c
Author: B. Wilson <elaexuotee@wilsonb.com>
AuthorDate: Wed Jul 1 12:56:10 2020 +0200

    gnu: Add metamath.
    
    * gnu/packages/maths.scm (metamath): New variable.
    
    Signed-off-by: Nicolas Goaziou <mail@nicolasgoaziou.fr>
---
 gnu/packages/maths.scm | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 48cffba..5ea5057 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.
 ;;;
@@ -2409,6 +2410,42 @@ message-passing communication.  @code{slepc4py} provides 
Python
 bindings to almost all functions of SLEPc.")
     (license license:bsd-3)))
 
+(define-public metamath
+  ;; Upstream pushed a commit on top of v0.182 that fixes a bug in Makefile.am.
+  ;; Using this commit lets us avoid directly including the patch here.  In the
+  ;; next version bump, we should be able to replace this and directly use the
+  ;; version tag.
+  (let ((commit "5df616efe4119ff88daf77e7041d45b6fa39c578")
+        (revision "0"))
+    (package
+      (name "metamath")
+      (version (git-version "0.182" revision commit))
+      (source
+       (origin
+         (method git-fetch)
+         (uri (git-reference
+               (url "https://github.com/metamath/metamath-exe.git";)
+               (commit commit)))
+         (file-name (git-file-name name version))
+         (sha256
+          (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"))))
+      (build-system gnu-build-system)
+      (native-inputs
+       `(("autoconf" ,autoconf)
+         ("automake" ,automake)))
+      (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 @command{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, Stirling's formula, etc.  See the Metamath
+book.")
+      (license license:gpl2+))))
+
 (define-public mumps
   (package
     (name "mumps")