[bug#40815] gnu: Add metamath

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

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