diff mbox series

[bug#40815] gnu: Add metamath

Message ID 3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com
State Accepted
Headers show
Series [bug#40815] gnu: Add metamath | expand

Checks

Context Check Description
cbaines/comparison success View comparision
cbaines/git branch success View Git branch
cbaines/applying patch fail View Laminar job

Commit Message

guix--- via Guix-patches via May 11, 2020, 11:25 a.m. UTC 
Well, after a good bit of wrangling, here is another round.

We have URLs pointing to static sources; I got upstream to fix things so we
don't need a patch; and now we're generating the doc output's pdf from the TeX
source.

The latter is what made this take so much time and effort.

On the one hand, it required packaging up 6 texlive dependencies, which are
included in the attached patches. On the other hand, it turns out that the
texlive-amsfonts package is broken, which we need to typset the metamath doc
output. This caused me tons of grief but turns out to be a known issue:

https://debbugs.gnu.org/cgi/bugreport.cgi?bug=40558

Thus, as of commit a1f84aca, the attached patch for metamath actually breaks.
However, with the proposed patched included in issue #40558 above, it builds
just fine.

Regarding the patches for the texlive packages, I did all of them as
simple-texlive-package templates with #:trivial? #t, grabbing the files from
tex/latex and doc/latex. Is this reasonable? Looking at other packages, I
cannot tell whether it'd be preferable to directly generate everything from the
*.dtx and *.sty sources.

Also, regarding texlive-mathstyle and texlive-flexisym, their files reside
under latex/breqn, but since they have their own ctan pages, I opted to split
them into separate packages and make the dependencies explicit. Does that seem
reasonable?

Anyway, thanks for taking a look! Hopefully, these look mergeable apart from
the texlive-amsfonts issue.
Jakub Kądziołka <kuba@kadziolka.net> wrote:
> On Mon, Apr 27, 2020 at 01:21:03PM +0900, x@wilsonb.com wrote:
> > > > +(define-public metamath
> > > > +  (package
> > > > +    (name "metamath")
> > > > +    (version "0.182")
> > > > +    (source
> > > > +     (origin
> > > > +       (method url-fetch)
> > > > +       (uri "http://us2.metamath.org/downloads/metamath-program.zip")
> > > 
> > > This looks like an unversioned URL. That's not ideal, since when
> > > upstream will release a new version, it will break the hash below. I
> > > looked around on their website and couldn't find a versioned URL, but I
> > > also couldn't find the one you're using. We could fetch from GitHub
> > > instead...
> > 
> > This is a long story.
> > 
> > The official tar linked on upstream's homepage is also unversioned and gets
> > updated daily via some automatic script. The reason being that they also
> > provide snapshots of the databases from the set.mm repository.
> > 
> > To boot, the GitHub repository (https://github.com/metamath/metamath-exe) only
> > contains a single, outdated release tar, which is simply a spurious byproduct
> > of a prolonged discussion I had with upstream regarding the problems their
> > release tars pose for package maintainers.
> 
> I notice, though, that the commits in the repository are up to date. We
> could pin a specific commit ID. This practice is relatively common in
> Guix and does not pose a problem.
> 
> Regards,
> Jakub Kądziołka
diff mbox series

Patch

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

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

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 8fbce15418..2054e1ad8e 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.
 ;;;
@@ -5615,3 +5616,76 @@  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"))))
+    (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 ((docdir (assoc-ref outputs "doc")))
+                 (install-file
+                  (string-append book-builddir "/metamath.pdf")
+                  (string-append docdir "/share/doc/metamath"))
+                 #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.26.2