GNU bug report logs - #40815
gnu: Add metamath

Previous Next

Full log

Message #32 received at 40815 <at> debbugs.gnu.org (full text, mbox):

From: elaexuotee <at> wilsonb.com
To: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
Cc: , Jakub Kądziołka <kuba <at> kadziolka.net>,
 40815 <at> debbugs.gnu.org
Subject: Re: [bug#40815] gnu: Add metamath
Date: Tue, 23 Jun 2020 20:32:15 +0900

[Message part 1 (text/plain, inline)]

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,

[0001-gnu-Add-metamath.patch (text/x-patch, attachment)]

[signature.asc (application/pgp-signature, attachment)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.