[bug#40815] gnu: Add metamath

[bug#40815] gnu: Add metamath

[B. Wilson via Guix-patches via]

[-- 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 --]

[bug#40815] gnu: Add metamath

[Jakub Kądziołka]

[-- Attachment #1: Type: text/plain, Size: 4270 bytes --]

On Fri, Apr 24, 2020 at 08:48:30PM +0900, B. Wilson wrote:
> This is my first packaging attempt, so careful critiques are very
> welcome.

Welcome to Guix, then!

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

Huh, we usually don't abbreviate first names. It's fine if you prefer it
this way, though. (BTW, the LaTeX on your website is broken.)

> +(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...

> 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?

AFAIK, building from source is preferred. grep for texlive-union to see
how it can be done without pulling in gigabytes of dependencies.

The no-versioned-URL problem also applies to the documentation, and
this would let you solve two problems at once ;)

> +    (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")))))))

Let me cite an excerpt from your build log: ;)

## WARNING: phase `install-doc' returned `#<unspecified>'.  Return values other than #t
## are deprecated.  Please migrate this package so that its phase
## procedures report errors by raising an exception, and otherwise
## always return #t.

Also, consider binding the path to the /share/doc directory in a variable:
(let ((docdir (string-append ...)))
  (mkdir-p docdir)
  (copy-file (assoc-ref inputs "book")
             (string-append docdir "/metamath.pdf"))
  #t)

> 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?

Nothing comes to mind as far as other alternatives for mkdir-p +
copy-file go.

> 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

Make sure to add this new file to gnu/local.mk!

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

I suppose your not including the databases is intentional, but the
reasoning behind that seems not entirely clear to me - wouldn't the
program be more useful when packaged with its database?

Regards,
Jakub Kądziołka

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

[bug#40815] gnu: Add metamath

[x--- via Guix-patches via]

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

Jakub Kądziołka <kuba@kadziolka.net> wrote:
> On Fri, Apr 24, 2020 at 08:48:30PM +0900, B. Wilson wrote:
> > This is my first packaging attempt, so careful critiques are very
> > welcome.
> 
> Welcome to Guix, then!

Thanks!

> > 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>
> 
> Huh, we usually don't abbreviate first names. It's fine if you prefer it
> this way, though. (BTW, the LaTeX on your website is broken.)

"B. Wilson" is typically the name I use for public development. If it poses a
problem, I do not mind chosing some other alias.

Also, thank you for taking the time to audit my meagre and severely neglected
website.

> > +(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.

All in all I spent a few weeks discussing the problem, eventually resulting in
the url seen in the patch. IIRC this url did end up on the main homepage, but
for some reason it seems to be missing now.

There were other technical complications, but the current status is that
upstream is a single developer making a special effort to accomodate us here.
The rest of the (quite small) metamath community mostly just conform's
to the somewhat anachronistic workflow that the developer has in place.

Anyway, I recognize the current status makes packaging problematic and will
open a dialog with upstream again, but given the background, I am not sure how
this will go.

> > 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?
> 
> AFAIK, building from source is preferred. grep for texlive-union to see
> how it can be done without pulling in gigabytes of dependencies.
> 
> The no-versioned-URL problem also applies to the documentation, and
> this would let you solve two problems at once ;)

Thank you. I will look into this.

> > +    (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")))))))
> 
> Let me cite an excerpt from your build log: ;)
> 
> ## WARNING: phase `install-doc' returned `#<unspecified>'.  Return values other than #t
> ## are deprecated.  Please migrate this package so that its phase
> ## procedures report errors by raising an exception, and otherwise
> ## always return #t.
> 
> Also, consider binding the path to the /share/doc directory in a variable:
> (let ((docdir (string-append ...)))
>   (mkdir-p docdir)
>   (copy-file (assoc-ref inputs "book")
>              (string-append docdir "/metamath.pdf"))
>   #t)

Ew. I can't believe I missed that warning. Thank you for pointing it out.

Regarding the local bindings, I did notice that pattern used liberally in the
repo. My reasoning for using the forms directly is simply that they only get
used once. Anyway, my revised patch will include the `let' since that's indeed
more idiomatic.

> > 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?
> 
> Nothing comes to mind as far as other alternatives for mkdir-p +
> copy-file go.

Thanks. Though it is unlikely to be part of the final patch, as per the above
revisions, the confirmation is helpful.

> > 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
> 
> Make sure to add this new file to gnu/local.mk!
> 
> > @@ -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 \
> 
> I suppose your not including the databases is intentional, but the
> reasoning behind that seems not entirely clear to me - wouldn't the
> program be more useful when packaged with its database?

The package fails to build without the patch because the archive doesn't
actually include the files, which are expected to be cloned from the set.mm
repository. I don't have full insight as to why Makefile.am is like this but
will try to push the fix to upstream as well.

> Regards,
> Jakub Kądziołka

Thank you for the thorough review! I will give this package another try.


Cheers,

B. Wilson

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

[bug#40815] gnu: Add metamath

[Jakub Kądziołka]

[-- Attachment #1: Type: text/plain, Size: 1401 bytes --]

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: 833 bytes --]

[bug#40815] gnu: Add metamath

[B. Wilson via Guix-patches via]

[-- 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 --]

[bug#40815] gnu: Add metamath

[B. Wilson via Guix-patches via]

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

Updated patch for metamath, containing two fixes:

* Rename source repo checkout to match package name (fixes lint warning), and
* Consolidate pdf under share/doc/<name>-<version> with LICENSE.TXT.


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

From f7c803351c483ff0efe0e65604fec3de001f7282 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 8fbce15418..5dc600ccb5 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,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 (string-append name "-" version "-checkout"))))
+    (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.26.2


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

[bug#40815] gnu: Add metamath

[Nicolas Goaziou]

Hello,

"B. Wilson via Guix-patches" via <guix-patches@gnu.org> writes:

> Updated patch for metamath, containing two fixes:
>
> * Rename source repo checkout to match package name (fixes lint warning), and
> * Consolidate pdf under share/doc/<name>-<version> with LICENSE.TXT.

Thank you!

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.

> +(define-public metamath
> +  (package
> +    (name "metamath")
> +    (version "0.182")

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.

> +    (source
> +     (origin
> +       (method git-fetch)
> +       (uri (git-reference
> +             (url "https://github.com/metamath/metamath-exe.git")
> +             (commit "5df616efe4119ff88daf77e7041d45b6fa39c578")))
> +       (sha256
> +        (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"))
> +       (file-name (string-append name "-" version "-checkout"))))

This should be `git-file-name', but I saw you fixed it already.

> +    (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.

> +           (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"))

Nitpick: this is often located right after the source keyword.

> +    (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

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.

> +    (license license:gpl2+)))

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

Regards,

-- 
Nicolas Goaziou

[bug#40815] gnu: Add metamath

[elaexuotee--- via Guix-patches via]

[-- 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 --]

[bug#40815] gnu: Add metamath

[Nicolas Goaziou]

Hello,

laexuotee@wilsonb.com writes:

> 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.

Note the book could also go into another package, once texlive-amsfonts
is fixed. Meanwhile, I think we can remove the comments in this one and
apply it.

WDYT?

> Were you referring to CC0 for the metamath book?

Probably, yes.

> 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?

I don't have enough knowledge to comment LaTeX packages. I suggest to
submit them as separate issues. If still no one comments of them, I'll
apply them later.

Regards,
-- 
Nicolas Goaziou

[bug#40815] gnu: Add metamath

[elaexuotee--- via Guix-patches via]

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

> Note the book could also go into another package, once texlive-amsfonts is
> fixed.

Interesting. Either way it's a similarly sized patch, so I'm curious why a
"metamath-doc" packages would be preferable to a "metamath:doc" output.

> Meanwhile, I think we can remove the comments in this one and apply it.
> 
> WDYT?

Sure. You intuition on what is best for the repo is certainly more honed than
mine. Would you mind sharing your reasoning for deleting the comments though?
Not sure I see why.

My thinking was this: want want a "doc" output if possible; the work of
creating that is already done; so we might as well make that work available.
Are you mostly trying to avoid comment clutter?

Either way, the patch I included here strips out the comments.

> I don't have enough knowledge to comment LaTeX packages. I suggest to
> submit them as separate issues. If still no one comments of them, I'll
> apply them later.

Great. I'll do that. Thanks.

Cheers!


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

From 4d94ad11b0e998a9510708e088a4c5eb63919b3b 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 | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 45d699e39c..02109ced2d 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,39 @@ and conversions, physical constants, symbolic calculations (including
 integrals and equations), arbitrary precision, uncertainity propagation,
 interval arithmetic, plotting.")
     (license license:gpl2+)))
+
+(define-public metamath
+  ;; Upstream pushed a commit on top of v0.182 that fixes a bug in Makefile.am.
+  ;; Using this commit lets us avoid directly including the patch here.  In the
+  ;; next version bump, we should be able to replace this and directly use the
+  ;; version tag.
+  (let ((commit "5df616efe4119ff88daf77e7041d45b6fa39c578")
+        (revision "0")
+        (book-name "metamath-book")
+        (book-version "second_edition"))
+    (package
+      (name "metamath")
+      (version (git-version "0.182" revision commit))
+      (source
+       (origin
+         (method git-fetch)
+         (uri (git-reference
+               (url "https://github.com/metamath/metamath-exe.git")
+               (commit commit)))
+         (sha256
+          (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"))
+         (file-name (git-file-name name version))))
+      (build-system gnu-build-system)
+      (native-inputs `(("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 @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 --]

[bug#40815] gnu: Add metamath

[Nicolas Goaziou]

Hello,

elaexuotee@wilsonb.com writes:

>> Note the book could also go into another package, once texlive-amsfonts is
>> fixed.
>
> Interesting. Either way it's a similarly sized patch, so I'm curious why a
> "metamath-doc" packages would be preferable to a "metamath:doc"
> output.

The book looks like a related project to metamath, like advanced
documentation, not like a regular manual. I didn't read it, so it is
just a guess.

Anyway, I only suggested it as another option to consider. Feel free to
ignore it.

> Sure. You intuition on what is best for the repo is certainly more honed than
> mine. Would you mind sharing your reasoning for deleting the comments though?
> Not sure I see why.
>
> My thinking was this: want want a "doc" output if possible; the work of
> creating that is already done; so we might as well make that work available.
> Are you mostly trying to avoid comment clutter?

I do. In any case, if you want to keep them, they need to start with two
semicolons, not a single one.

WDYT?

Regards,
-- 
Nicolas Goaziou

[bug#40815] gnu: Add metamath

[elaexuotee--- via Guix-patches via]

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

Hell,

Thanks for the quick turnaround.

> The book looks like a related project to metamath, like advanced
> documentation, not like a regular manual. I didn't read it, so it is
> just a guess.

Oh, okay. That makes sense. PDF as official documentation is certainly strange
for what looks like a cli program. In this case, it just happens that this is
the only reasonable documentation, aparth from the website, for using and
understanding Metamath proofs.

> I do. In any case, if you want to keep them, they need to start with two
> semicolons, not a single one.
> 
> WDYT?

I trust your initial impression on this one. Let's use the patch from my
previous email that excises the commented out code. Does it look reasonable?

Cheers.

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

bug#40815: gnu: Add metamath

[Nicolas Goaziou]

Hello,

elaexuotee@wilsonb.com writes:

> I trust your initial impression on this one. Let's use the patch from my
> previous email that excises the commented out code. Does it look
> reasonable?

Certainly. I removed the book-revision and book-version bindings, since
they were not used in the current package definition, tweaked a bit the
description, and applied your patch.

I hope we can have the book either as a doc output, or as a separate
package, bundled at some point. Meanwhile, I'm closing this bug report.

Regards,
-- 
Nicolas Goaziou

[bug#40815] gnu: Add metamath

[elaexuotee--- via Guix-patches via]

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

Excellent. Thanks for cleaning up the things I missed and pushing.

Nicolas Goaziou <mail@nicolasgoaziou.fr> wrote:
> Hello,
> 
> elaexuotee@wilsonb.com writes:
> 
> > I trust your initial impression on this one. Let's use the patch from my
> > previous email that excises the commented out code. Does it look
> > reasonable?
> 
> Certainly. I removed the book-revision and book-version bindings, since
> they were not used in the current package definition, tweaked a bit the
> description, and applied your patch.
> 
> I hope we can have the book either as a doc output, or as a separate
> package, bundled at some point. Meanwhile, I'm closing this bug report.
> 
> Regards,



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

[bug#40815] gnu: Add metamath

[elaexuotee--- via Guix-patches via]

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

Oops. Looks like my previous emais's patch was for the version that *didn't*
comment out the "doc" output. The one included here should be correct.


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

From 74db38db11a7e107119362983e388cfb5ead3431 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 | 97 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 97 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 45d699e39c..e6f4cbe980 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,99 @@ and conversions, physical constants, symbolic calculations (including
 integrals and equations), arbitrary precision, uncertainity propagation,
 interval arithmetic, plotting.")
     (license license:gpl2+)))
+
+(define-public metamath
+  ;; Upstream pushed a commit on top of v0.182 that fixes a bug in Makefile.am.
+  ;; Using this commit lets us avoid directly including the patch here.  In the
+  ;; next version bump, we should be able to replace this and directly use the
+  ;; version tag.
+  (let ((commit "5df616efe4119ff88daf77e7041d45b6fa39c578")
+        (revision "0")
+        (book-name "metamath-book")
+        (book-version "second_edition"))
+    (package
+      (name "metamath")
+      (version (git-version "0.182" revision commit))
+      (source
+       (origin
+         (method git-fetch)
+         (uri (git-reference
+               (url "https://github.com/metamath/metamath-exe.git")
+               (commit commit)))
+         (sha256
+          (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"))
+         (file-name (git-file-name name version))))
+      ;; FIXME: Unfortunately, there seems to be a problem with
+      ;; texlive-amsfonts that prevents us from typsetting the "doc" output
+      ;; pdf.  Once fixed, this along with the commented out sections below,
+      ;; should be enabled.
+      ; (outputs '("out" "doc"))
+      (build-system gnu-build-system)
+      ;; FIXME: Enable for "doc" output.  See previous comment.
+      ; (inputs
+      ;  `((,book-name
+      ;     ,(origin
+      ;        (method git-fetch)
+      ;        (uri (git-reference
+      ;              (url "https://github.com/metamath/metamath-book.git")
+      ;              (commit book-version)))
+      ;        (sha256
+      ;         (base32
+      ;          "1kk9nfhs0h8qccpxp1qh072bpfis7h05rlnz3qn1z641d9i4ryyq"))
+      ;        (file-name (git-file-name book-name book-version))))))
+      (native-inputs `(("autoconf" ,autoconf)
+                       ("automake" ,automake)
+                       ;; FIXME: Required inputs to build the "doc" output.
+                       ;; See above comment.
+                       ; ("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)))
+                       ))
+      ;; FIXME: Arguments to build the "doc" output.  See above comment.
+      ; (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 (assoc-ref inputs ,book-name)))
+      ;              (mkdir-p book-builddir)
+      ;              (copy-recursively book book-builddir))))
+      ;        (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.")
+    ;; FIXME: The "doc" output requires license:cc0.  See above comment.
+    ; (license '(,license:gpl2+ ,license:cc0)))))
+    (license license:gpl2+))))
-- 
2.27.0


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

[bug#40815] gnu: Add metamath.

[elaexuotee--- via Guix-patches via]

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

Just discovered the (git-file-name ...) function. This is a simple update to
the metamath patch to use this instead of manually using string-append.


[-- 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 0e9facf67f5af44bb8e605631a0be6c90ce23000 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 d60c033dbc..5a7230cb53 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.
 ;;;
@@ -5635,3 +5636,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.26.2


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