[bug#40815] gnu: Add metamath

["Jakub Kądziołka" <kuba@kadziolka.net>]

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