summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorB. Wilson <elaexuotee@wilsonb.com>2020-07-01 12:56:10 +0200
committerNicolas Goaziou <mail@nicolasgoaziou.fr>2020-07-01 12:56:10 +0200
commitd277c00ec942b7eb52f918b5e17c043e95fef27c (patch)
treec81ab135d479d2e52dd9af1d307b186a827a6342
parent.guix-authorizations: Remove keys of two former contributors. (diff)
downloadguix-d277c00ec942b7eb52f918b5e17c043e95fef27c.tar.gz
guix-d277c00ec942b7eb52f918b5e17c043e95fef27c.tar.bz2
guix-d277c00ec942b7eb52f918b5e17c043e95fef27c.tar.xz
gnu: Add metamath.
* gnu/packages/maths.scm (metamath): New variable. Signed-off-by: Nicolas Goaziou <mail@nicolasgoaziou.fr>
-rw-r--r--gnu/packages/maths.scm37
1 files changed, 37 insertions, 0 deletions
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 @@
38;;; Copyright © 2020 R Veera Kumar <vkor@vkten.in> 38;;; Copyright © 2020 R Veera Kumar <vkor@vkten.in>
39;;; Copyright © 2020 Vincent Legoll <vincent.legoll@gmail.com> 39;;; Copyright © 2020 Vincent Legoll <vincent.legoll@gmail.com>
40;;; Copyright © 2020 Nicolò Balzarotti <nicolo@nixo.xyz> 40;;; Copyright © 2020 Nicolò Balzarotti <nicolo@nixo.xyz>
41;;; Copyright © 2020 B. Wilson <elaexuotee@wilsonb.com>
41;;; 42;;;
42;;; This file is part of GNU Guix. 43;;; This file is part of GNU Guix.
43;;; 44;;;
@@ -2409,6 +2410,42 @@ message-passing communication. @code{slepc4py} provides Python
2409bindings to almost all functions of SLEPc.") 2410bindings to almost all functions of SLEPc.")
2410 (license license:bsd-3))) 2411 (license license:bsd-3)))
2411 2412
2413(define-public metamath
2414 ;; Upstream pushed a commit on top of v0.182 that fixes a bug in Makefile.am.
2415 ;; Using this commit lets us avoid directly including the patch here. In the
2416 ;; next version bump, we should be able to replace this and directly use the
2417 ;; version tag.
2418 (let ((commit "5df616efe4119ff88daf77e7041d45b6fa39c578")
2419 (revision "0"))
2420 (package
2421 (name "metamath")
2422 (version (git-version "0.182" revision commit))
2423 (source
2424 (origin
2425 (method git-fetch)
2426 (uri (git-reference
2427 (url "https://github.com/metamath/metamath-exe.git")
2428 (commit commit)))
2429 (file-name (git-file-name name version))
2430 (sha256
2431 (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"))))
2432 (build-system gnu-build-system)
2433 (native-inputs
2434 `(("autoconf" ,autoconf)
2435 ("automake" ,automake)))
2436 (home-page "http://us.metamath.org/")
2437 (synopsis "Proof verifier based on a minimalistic formalism")
2438 (description
2439 "Metamath is a tiny formal language and that can express theorems in
2440abstract mathematics, with an accompyaning @command{metamath} executable that
2441verifies databases of these proofs. There is a public database,
2442@url{https://github.com/metamath/set.mm, set.mm}, implementing first-order
2443logic and Zermelo-Frenkel set theory with Choice, along with a large swath of
2444associated, high-level theorems, e.g.@: the fundamental theorem of arithmetic,
2445the Cauchy-Schwarz inequality, Stirling's formula, etc. See the Metamath
2446book.")
2447 (license license:gpl2+))))
2448
2412(define-public mumps 2449(define-public mumps
2413 (package 2450 (package
2414 (name "mumps") 2451 (name "mumps")