unofficial mirror of guix-patches@gnu.org 
 help / color / mirror / code / Atom feed
* [bug#40815] gnu: Add metamath
@ 2020-04-24 11:48 B. Wilson via Guix-patches via
  2020-04-26 17:29 ` Jakub Kądziołka
  2020-05-13  7:25 ` elaexuotee--- via Guix-patches via
  0 siblings, 2 replies; 16+ messages in thread
From: B. Wilson via Guix-patches via @ 2020-04-24 11:48 UTC (permalink / raw)
  To: 40815


[-- Attachment #1.1: Type: text/plain, Size: 753 bytes --]


This is my first packaging attempt, so careful critiques are very welcome.

The package definition itself is pretty bog standard, apart from how the "doc" output is supplied. Upstream provides the official documentation as a pdf offered separately from the source. I decided to include this as an input and manually copy it over. Upstream does also have a repo with the TeX sources. Would it be better to typset it directly instead?

Also, regarding my `install-doc' phase, is the way I copy over the /gnu/store/<hash>-metamath.pdf file reasonable? Unfortunately, `install-file' doesn't allow renaming the destination, so I had to mimic its effect. Is there a better, or more idiomatic way to do this kind of thing?

Anyway, cheers and guix!


[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1.2: 0001-gnu-Add-metamath.patch --]
[-- Type: text/x-patch, Size: 3939 bytes --]

From 808e8d73cb231d2fbf34b88683fb0c3fe5d631e9 Mon Sep 17 00:00:00 2001
From: "B. Wilson" <elaexuotee@wilsonb.com>
Date: Thu, 23 Apr 2020 20:28:49 +0900
Subject: [PATCH] gnu: Add metamath

* gnu/packages/maths.scm (metamath): New variable.
* gnu/packages/patches/metamath-remove-missing-file-refs.patch: New file.
---
 gnu/packages/maths.scm                        | 45 +++++++++++++++++++
 .../metamath-remove-missing-file-refs.patch   | 17 +++++++
 2 files changed, 62 insertions(+)
 create mode 100644 gnu/packages/patches/metamath-remove-missing-file-refs.patch

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 \
-- 
2.26.2


[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 260 bytes --]

^ permalink raw reply related	[flat|nested] 16+ messages in thread

end of thread, other threads:[~2020-07-01 23:55 UTC | newest]

Thread overview: 16+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-04-24 11:48 [bug#40815] gnu: Add metamath B. Wilson via Guix-patches via
2020-04-26 17:29 ` Jakub Kądziołka
2020-04-27  4:21   ` x--- via Guix-patches via
2020-04-27 12:12     ` Jakub Kądziołka
2020-05-11 11:25       ` B. Wilson via Guix-patches via
2020-05-11 14:05         ` B. Wilson via Guix-patches via
2020-06-04 17:49           ` Nicolas Goaziou
2020-06-23 11:32             ` elaexuotee--- via Guix-patches via
2020-06-26  7:19               ` Nicolas Goaziou
2020-06-26  8:46                 ` elaexuotee--- via Guix-patches via
2020-06-28 20:12                   ` Nicolas Goaziou
2020-06-29  7:09                     ` elaexuotee--- via Guix-patches via
2020-07-01 11:02                       ` bug#40815: " Nicolas Goaziou
2020-07-01 23:53                         ` [bug#40815] " elaexuotee--- via Guix-patches via
2020-06-24  1:14             ` elaexuotee--- via Guix-patches via
2020-05-13  7:25 ` elaexuotee--- via Guix-patches via

Code repositories for project(s) associated with this public inbox

	https://git.savannah.gnu.org/cgit/guix.git

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).