[bug#40815] gnu: Add metamath

[elaexuotee--- via Guix-patches via <guix-patches@gnu.org>]

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

Hello Nicolas,

Thank you for taking a look at this!

> Unfortunately I cannot comment about Texlive packages, and particularly
> about the issue you're encountering there, but I can give some advice on
> this package definition.

This patch has been languishing around for quite a while, and instead of
waiting for texlive-amsfonts to get fixed, I propose nuking the "doc" output
for now so we can get this pushed.

The attached patch does just this. I commented out the parts specific to the
"doc" output and also included FIXME explanations of what's going on.

> I suggest to let-bind the commit hash around the package definition, add
> a revision number, and a comment explaining why you're not using plain
> v0.182 tag.

Done.

> > +    (build-system gnu-build-system)
> > +    (inputs
> > +     `(("book"
> > +        ,(origin
> > +           (method url-fetch)
> > +           (uri (string-append "https://github.com/metamath/"
> > +                               "metamath-book/archive/second_edition.tar.gz"))
> 
> IIRC, this URL is reliable. You could fetch "second_editon" tag instead.

This is now a commented out section, but I went ahead and updated it as you
suggested. Since this is a non-cosmetic change, I also test built it before
commenting out all the "doc" output stuff.

> Nitpick: [outputs] is often located right after the source keyword.

Moved. Not sure why I put it down there in the first place. I chock it up to
this being my first package attempt.

> You cannot use "e.g." in Texinfo syntax, because the last dot confuses
> it. It should be either "e.g.,", or "e.g.@:".
> 
> > +Arithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc.  See the
> > +Metamath book")
> 
> Missing final full stop.

Fixed. Thanks for the attention to detail.

> I think there are other licenses involved. Could you try to list them,
> too?

Were you referring to CC0 for the metamath book?

I added this license in a FIXME comment. As far as I can tell, the metamath
executable itself is just GLP2+, but if I'm missing something please let me
know.


Hopefully, in the near future I will find time to dig into the texlive-amsfonts
issue, but for now, does this look good?

If we end up pushing just the metamath patch, the other texlive package patches
obviously aren't needed for now, but would it be worth pushing these? Should I
submit separate issues for them?

Cheers,


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

From f7e7a323df50fc5c6d4aefb30f67991c367dfabc Mon Sep 17 00:00:00 2001
From: "B. Wilson" <elaexuotee@wilsonb.com>
Date: Mon, 11 May 2020 20:10:48 +0900
Subject: [PATCH] gnu: Add metamath.
To: guix-patches@gnu.org

* gnu/packages/maths.scm (metamath): New variable.
---
 gnu/packages/maths.scm | 75 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 75 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 45d699e39c..82b98d8f7d 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.
 ;;;
@@ -5686,3 +5687,77 @@ 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 git-fetch)
+       (uri (git-reference
+             (url "https://github.com/metamath/metamath-exe.git")
+             (commit "5df616efe4119ff88daf77e7041d45b6fa39c578")))
+       (sha256
+        (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"))
+       (file-name (git-file-name name version))))
+    (build-system gnu-build-system)
+    (inputs
+     `(("book"
+        ,(origin
+           (method url-fetch)
+           (uri (string-append "https://github.com/metamath/"
+                               "metamath-book/archive/second_edition.tar.gz"))
+           (sha256
+            (base32
+             "1kbgajik9dn870db1zslqyvhn2j8g7shb8d6dm6njwqfkygiliir"))))))
+    (native-inputs `(("autoconf" ,autoconf)
+                     ("automake" ,automake)
+                     ("texlive" ,(texlive-union
+                                  (list texlive-amsfonts
+                                        texlive-bibtex
+                                        texlive-breqn
+                                        texlive-makecell
+                                        texlive-microtype
+                                        texlive-tabu
+                                        texlive-latex-anysize
+                                        texlive-latex-hyperref
+                                        texlive-latex-needspace
+                                        texlive-latex-tools)))))
+    (outputs '("out" "doc"))
+    (arguments
+     `(#:phases
+       (let ((book-builddir "metamath-book-second_edition"))
+         (modify-phases %standard-phases
+           (add-after 'unpack 'unpack-doc
+             (lambda* (#:key inputs #:allow-other-keys)
+               (let ((book-tar (assoc-ref inputs "book")))
+                 (invoke "tar" "xzf" book-tar))))
+           (add-after 'build 'build-doc
+             (lambda _
+               (with-directory-excursion book-builddir
+                 (invoke "touch" "metamath.ind")
+                 (invoke "pdflatex" "metamath")
+                 (invoke "pdflatex" "metamath")
+                 (invoke "bibtex" "metamath")
+                 (invoke "makeindex" "metamath")
+                 (invoke "pdflatex" "metamath")
+                 (invoke "pdflatex" "metamath"))))
+           (add-after 'build-doc 'install-doc
+             (lambda* (#:key outputs #:allow-other-keys)
+               (let* ((pkg (strip-store-file-name (assoc-ref outputs "out")))
+                      (out-doc (assoc-ref outputs "doc")))
+                 (install-file (string-append book-builddir "/metamath.pdf")
+                               (string-append out-doc "/share/doc/" pkg))
+                 #t)))))))
+    (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+)))
-- 
2.27.0


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