me
/
guix
Archived
1
0
Fork 0
Code

gnu: metamath: Update to 0.183. 

* gnu/packages/maths.scm (metamath): Update to 0.183.

Signed-off-by: Nicolas Goaziou <mail@nicolasgoaziou.fr>
B. Wilson 2020-07-07 13:52:30 +09:00 committed by Nicolas Goaziou
parent 675bca979e
commit 6667576b66
No known key found for this signature in database
GPG Key ID: DA00B4F048E92F2D
1 changed files with 21 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

48
gnu/packages/maths.scm
View File

@ -2411,32 +2411,26 @@ bindings to almost all functions of SLEPc.")
(license license:bsd-3))) (license license:bsd-3)))
(define-public metamath (define-public metamath
;; Upstream pushed a commit on top of v0.182 that fixes a bug in Makefile.am. (package
;; Using this commit lets us avoid directly including the patch here. In the (name "metamath")
;; next version bump, we should be able to replace this and directly use the (version "0.183")
;; version tag. (source
(let ((commit "5df616efe4119ff88daf77e7041d45b6fa39c578") (origin
(revision "0")) (method git-fetch)
(package (uri (git-reference
(name "metamath") (url "https://github.com/metamath/metamath-exe.git")
(version (git-version "0.182" revision commit)) (commit (string-append "v" version))))
(source (file-name (git-file-name name version))
(origin (sha256
(method git-fetch) (base32 "1jjf4fy6j53i40dh0yv0f9sngnw4gs24cig99vsg3q0303pwrhg7"))))
(uri (git-reference (build-system gnu-build-system)
(url "https://github.com/metamath/metamath-exe.git") (native-inputs
(commit commit))) `(("autoconf" ,autoconf)
(file-name (git-file-name name version)) ("automake" ,automake)))
(sha256 (home-page "http://us.metamath.org/")
(base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp")))) (synopsis "Proof verifier based on a minimalistic formalism")
(build-system gnu-build-system) (description
(native-inputs "Metamath is a tiny formal language and that can express theorems in
`(("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 abstract mathematics, with an accompyaning @command{metamath} executable that
verifies databases of these proofs. There is a public database, verifies databases of these proofs. There is a public database,
@url{https://github.com/metamath/set.mm, set.mm}, implementing first-order @url{https://github.com/metamath/set.mm, set.mm}, implementing first-order
@ -2444,7 +2438,7 @@ 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, associated, high-level theorems, e.g.@: the fundamental theorem of arithmetic,
the Cauchy-Schwarz inequality, Stirling's formula, etc. See the Metamath the Cauchy-Schwarz inequality, Stirling's formula, etc. See the Metamath
book.") book.")
(license license:gpl2+)))) (license license:gpl2+)))
(define-public mumps (define-public mumps
(package (package