[bug#40815] gnu: Add metamath

["B. Wilson via Guix-patches" via <guix-patches@gnu.org>]

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

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.


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

From 2f1efc596c83ae4bf63925c612b54161f55838a1 Mon Sep 17 00:00:00 2001
From: "B. Wilson" <elaexuotee@wilsonb.com>
Date: Mon, 11 May 2020 20:02:41 +0900
Subject: [PATCH 1/7] gnu: Add texlive-mathstyle.
To: guix-patches@gnu.org

* gnu/packages/tex.scm (texlive-mathstyle): New Variable.
---
 gnu/packages/tex.scm | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scm
index 683f9d7283..f6d92b5f1c 100644
--- a/gnu/packages/tex.scm
+++ b/gnu/packages/tex.scm
@@ -13,6 +13,7 @@
 ;;; Copyright © 2018 Danny Milosavljevic <dannym+a@scratchpost.org>
 ;;; Copyright © 2018 Arun Isaac <arunisaac@systemreboot.net>
 ;;; Copyright © 2020 Vincent Legoll <vincent.legoll@gmail.com>
+;;; Copyright © 2020 B. Wilson <elaexuotee@wilsonb.com>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -7322,3 +7323,19 @@ facilities designed to cope with the more specific demands of academic
 writing, especially in the humanities and the social sciences.  All quote
 styles as well as the optional active quotes are freely configurable.")
       (license license:lppl1.3c+))))
+
+(define-public texlive-mathstyle
+  (package
+    (inherit (simple-texlive-package
+              "texlive-mathstyle"
+              (list "/tex/latex/breqn/mathstyle.sty"
+                    "/doc/latex/breqn/mathstyle.pdf")
+              (base32 "0rlnp20ns70ir0sac4qwcigr4a25s813cijvjamwm6q42y6wj8vp")
+              #:trivial? #t))
+    (propagated-inputs `(("texlive-latex-l3kernel" ,texlive-latex-l3kernel)))
+    (home-page "https://www.ctan.org/pkg/mathstyle")
+    (synopsis "Manage mathematics typesetting style")
+    (description "Flexisym converts mathematical symbol definitions to the form
+they need for breqn to work.  The package offers support for breqn and is part
+of the bundle of the same name.")
+    (license license:lppl1.3c+)))
-- 
2.26.2


[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1.3: 0002-gnu-Add-texlive-flexisym.patch --]
[-- Type: text/x-patch, Size: 1839 bytes --]

From 03068f1e5f01fde67f53aa1ea7dcb477c0ab669e Mon Sep 17 00:00:00 2001
From: "B. Wilson" <elaexuotee@wilsonb.com>
Date: Mon, 11 May 2020 20:03:54 +0900
Subject: [PATCH 2/7] gnu: Add texlive-flexisym.
To: guix-patches@gnu.org

* gnu/packages/tex.scm (texlive-flexisym): New variable.
---
 gnu/packages/tex.scm | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scm
index f6d92b5f1c..6727a2c985 100644
--- a/gnu/packages/tex.scm
+++ b/gnu/packages/tex.scm
@@ -7339,3 +7339,24 @@ styles as well as the optional active quotes are freely configurable.")
 they need for breqn to work.  The package offers support for breqn and is part
 of the bundle of the same name.")
     (license license:lppl1.3c+)))
+
+(define-public texlive-flexisym
+  (package
+    (inherit (simple-texlive-package
+              "texlive-flexisym"
+              (list "/tex/latex/breqn/flexisym.sty"
+                    "/tex/latex/breqn/cmbase.sym"
+                    "/tex/latex/breqn/mathpazo.sym"
+                    "/tex/latex/breqn/mathptmx.sym"
+                    "/tex/latex/breqn/msabm.sym"
+                    "/doc/latex/breqn/flexisym.pdf")
+              (base32 "0vjhk94s7z83wcb38ww5nzbjywvybfwm6vg7a2yy8ic2sjm0pjxj")
+              #:trivial? #t))
+    (propagated-inputs `(("texlive-latex-l3kernel" ,texlive-latex-l3kernel)
+                         ("texlive-mathstyle" ,texlive-mathstyle)))
+    (home-page "https://www.ctan.org/pkg/flexisym")
+    (synopsis "Symbol manipulation for breqn")
+    (description "Flexisym converts mathematical symbol definitions to the form
+they need for breqn to work.  The package offers support for breqn and is part
+of the bundle of the same name.")
+    (license license:lppl1.3c+)))
-- 
2.26.2


[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1.4: 0003-gnu-Add-texlive-breqn.patch --]
[-- Type: text/x-patch, Size: 2456 bytes --]

From aca179c3100bced9438c91dc25a1cafe9a9814bd Mon Sep 17 00:00:00 2001
From: "B. Wilson" <elaexuotee@wilsonb.com>
Date: Mon, 11 May 2020 20:05:58 +0900
Subject: [PATCH 3/7] gnu: Add texlive-breqn.
To: guix-patches@gnu.org

* gnu/packages/tex.scm (texlive-breqn): New variable.
---
 gnu/packages/tex.scm | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scm
index 6727a2c985..710ad2ba20 100644
--- a/gnu/packages/tex.scm
+++ b/gnu/packages/tex.scm
@@ -7360,3 +7360,31 @@ of the bundle of the same name.")
 they need for breqn to work.  The package offers support for breqn and is part
 of the bundle of the same name.")
     (license license:lppl1.3c+)))
+
+(define-public texlive-breqn
+  (package
+    (inherit (simple-texlive-package
+              "texlive-breqn"
+              (list "/tex/latex/breqn/breqn.sty"
+                    "/doc/latex/breqn/breqn.pdf")
+              (base32 "0mdm3yyimr8fv8pg2b2zv62fjbx98xy60a3dzj55djdir6hyxf6h")
+              #:trivial? #t))
+    (propagated-inputs `(("texlive-latex-amsmath" ,texlive-latex-amsmath)
+                         ("texlive-flexisym" ,texlive-flexisym)
+                         ("texlive-latex-graphics" ,texlive-latex-graphics)
+                         ("texlive-latex-l3kernel" ,texlive-latex-l3kernel)
+                         ("texlive-latex-tools" ,texlive-latex-tools)))
+    (home-page "http://wspr.io/breqn/")
+    (synopsis "Automated line breaking of displayed equations")
+    (description "The package provides solutions to a number of common
+difficulties in writing displayed equations and getting high-quality output.
+For example, it is a well-known inconvenience that if an equation must be
+broken into more than one line, @code{left...right} constructs cannot span
+lines.  The breqn package makes them work as one would expect whether or not
+there is an intervening line break.  The single most ambitious goal of the
+package, however, is to support automatic linebreaking of displayed equations.
+Such linebreaking cannot be done without substantial changes under the hood in
+the way formulae are processed; the code must be watched carefully, keeping an
+eye on possible glitches.  The bundle also contains the flexisym and mathstyle
+packages, which are both designated as support for breqn.")
+    (license license:lppl1.3c+)))
-- 
2.26.2


[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1.5: 0004-gnu-Add-texlive-makecell.patch --]
[-- Type: text/x-patch, Size: 2117 bytes --]

From f3298a40c3fe945c9dc0cbfc3f9a7fa9bfb73cb8 Mon Sep 17 00:00:00 2001
From: "B. Wilson" <elaexuotee@wilsonb.com>
Date: Mon, 11 May 2020 20:07:03 +0900
Subject: [PATCH 4/7] gnu: Add texlive-makecell.
To: guix-patches@gnu.org

* gnu/packages/tex.scm (texlive-makecell): New variable.
---
 gnu/packages/tex.scm | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scm
index 710ad2ba20..ca5b9dbb2e 100644
--- a/gnu/packages/tex.scm
+++ b/gnu/packages/tex.scm
@@ -7388,3 +7388,32 @@ the way formulae are processed; the code must be watched carefully, keeping an
 eye on possible glitches.  The bundle also contains the flexisym and mathstyle
 packages, which are both designated as support for breqn.")
     (license license:lppl1.3c+)))
+
+(define-public texlive-makecell
+  (package
+    (inherit (simple-texlive-package
+              "texlive-makecell"
+              (list "/tex/latex/makecell/"
+                    "/doc/latex/makecell/makecell.pdf")
+              (base32 "1zdcmya5dxrnjf7lf0wmnhcjlwdha5gdzdx7xrgyi61gqwj7cxin")
+              #:trivial? #t))
+    (propagated-inputs `(("texlive-latex-tools" ,texlive-latex-tools)))
+    (home-page "https://www.ctan.org/pkg/makecell")
+    (synopsis "Tabular column heads and multilined cells")
+    (description "This package supports common layouts for tabular column heads
+in whole documents, based on one-column tabular environment.  In addition, it
+can create multi-lined tabular cells.
+
+The Package also offers:
+
+@itemize
+@item a macro which changes the vertical space around all the cells in a
+      tabular environment (similar to the function of the tabls package, but
+      using the facilities of the array);
+@item macros for multirow cells, which use the facilities of the multirow
+      package;
+@item macros to number rows in tables, or to skip cells;
+@item diagonally divided cells;
+@item horizontal lines in tabular environments with defined thickness.
+@end itemize")
+    (license license:lppl)))
-- 
2.26.2


[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1.6: 0005-gnu-Add-texlive-microtype.patch --]
[-- Type: text/x-patch, Size: 2541 bytes --]

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

* gnu/packages/tex.scm (texlive-microtype): New variable.
---
 gnu/packages/tex.scm | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scm
index ca5b9dbb2e..2d290fdb82 100644
--- a/gnu/packages/tex.scm
+++ b/gnu/packages/tex.scm
@@ -7417,3 +7417,37 @@ The Package also offers:
 @item horizontal lines in tabular environments with defined thickness.
 @end itemize")
     (license license:lppl)))
+
+(define-public texlive-microtype
+  (package
+    (inherit (simple-texlive-package
+              "texlive-microtype"
+              (list "/tex/latex/microtype/"
+                    "/doc/latex/microtype/")
+              (base32 "0xmjpzbj4nqmnl5m7xx1bshdk2c8n57rmbvn0j479ypj4wdlq9iy")
+              #:trivial? #t))
+    (propagated-inputs `(("texlive-latex-graphics" ,texlive-latex-graphics)))
+    (home-page "https://www.ctan.org/pkg/microtype")
+    (synopsis "Subliminal refinements towards typographical perfection")
+    (description "The package provides a LaTeX interface to the
+micro-typographic extensions that were introduced by pdfTeX and have since also
+propagated to XeTeX and LuaTeX: most prominently, character protrusion and font
+expansion, furthermore the adjustment of interword spacing and additional
+kerning, as well as hyphenatable letterspacing (tracking) and the possibility
+to disable all or selected ligatures.
+
+These features may be applied to customisable sets of fonts, and all
+micro-typographic aspects of the fonts can be configured in a straight-forward
+and flexible way.  Settings for various fonts are provided.
+
+Note that character protrusion requires pdfTeX, LuaTeX, or XeTeX.  Font
+expansion works with pdfTeX or LuaTeX.  The package will by default enable
+protrusion and expansion if they can safely be assumed to work.  Disabling
+ligatures requires pdfTeX or LuaTeX, while the adjustment of interword spacing
+and of kerning only works with pdfTeX.  Letterspacing is available with pdfTeX
+or LuaTeX.
+
+The alternative package @code{letterspace}, which also works with plain TeX,
+provides the user commands for letterspacing only, omitting support for all
+other extensions.")
+    (license license:lppl1.3c+)))
-- 
2.26.2


[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1.7: 0006-gnu-Add-texlive-tabu.patch --]
[-- Type: text/x-patch, Size: 2807 bytes --]

From 01ce7a13c2897263e754bb8164c2472bc683d6bf Mon Sep 17 00:00:00 2001
From: "B. Wilson" <elaexuotee@wilsonb.com>
Date: Mon, 11 May 2020 20:09:31 +0900
Subject: [PATCH 6/7] gnu: Add texlive-tabu.
To: guix-patches@gnu.org

* gnu/packages/tex.scm (texlive-tabu): New variable.
---
 gnu/packages/tex.scm | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

diff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scm
index 2d290fdb82..f382330773 100644
--- a/gnu/packages/tex.scm
+++ b/gnu/packages/tex.scm
@@ -7451,3 +7451,42 @@ The alternative package @code{letterspace}, which also works with plain TeX,
 provides the user commands for letterspacing only, omitting support for all
 other extensions.")
     (license license:lppl1.3c+)))
+
+(define-public texlive-tabu
+  (package
+    (inherit (simple-texlive-package
+              "texlive-tabu"
+              (list "/tex/latex/tabu/"
+                    "/doc/latex/tabu/")
+              (base32 "156lkisyrpvn82ng2kxdlly60ny5vaz4lp9xlc66azy5ma06agvw")
+              #:trivial? #t))
+    (propagated-inputs
+     `(("texlive-latex-tools" ,texlive-latex-tools)
+       ("texlive-latex-varwidth" ,texlive-latex-varwidth)))
+    (home-page "https://www.ctan.org/pkg/tabu")
+    (synopsis "Flexible LaTeX tabulars")
+    (description "The package provides an environment, @code{tabu}, which will
+make any sort of tabular (that doesn’t need to split across pages), and an
+environment @code{longtabu} which provides the facilities of @code{tabu} in a
+modified longtable environment.  (Note that this latter offers an enhancement
+of ltxtable.)
+
+The package requires the array package, and needs e-TeX to run (since array.sty
+is present in every conforming distribution of LaTeX, and since every publicly
+available LaTeX format is built using e-TeX, the requirements are provided by
+default on any reasonable system).  The package also requires xcolor for
+coloured rules in tables, and colortbl for coloured cells.  The @code{longtabu}
+environment further requires that longtable be loaded.  The package itself does
+not load any of these packages for the user.
+
+The @code{tabu} environment may be used in place of @code{tabular},
+@code{tabular*} and @code{tabularx} environments, as well as the @code{array}
+environment in maths mode.  It overloads @code{tabularx}’s X-column
+specification, allowing a width specification, alignment (@code{l}, @code{r},
+@code{c} and @code{j}) and column type indication (@code{p}, @code{m} and
+@code{b}).
+
+@code{\begin@{tabu@}} to @code{<dimen>} specifies a target width, and
+@code{\begin@{tabu@}} spread @code{<dimen>} enlarges the environment’s
+natural width.")
+    (license license:lppl1.3c+)))
-- 
2.26.2


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

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


[-- Attachment #1.9: Type: text/plain, Size: 1520 bytes --]


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



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