GNU bug report logs - #40815
gnu: Add metamath

Previous Next

Package: guix-patches;

Reported by: "B. Wilson" <elaexuotee <at> wilsonb.com>

Date: Fri, 24 Apr 2020 11:55:01 UTC

Severity: normal

Done: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>

Bug is archived. No further changes may be made.

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 40815 in the body.
You can then email your comments to 40815 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

View this report as an mbox folder, status mbox, maintainer mbox


Report forwarded to guix-patches <at> gnu.org:
bug#40815; Package guix-patches. (Fri, 24 Apr 2020 11:55:02 GMT) Full text and rfc822 format available.

Acknowledgement sent to "B. Wilson" <elaexuotee <at> wilsonb.com>:
New bug report received and forwarded. Copy sent to guix-patches <at> gnu.org. (Fri, 24 Apr 2020 11:55:02 GMT) Full text and rfc822 format available.

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

From: "B. Wilson" <elaexuotee <at> wilsonb.com>
To: guix-patches <at> gnu.org
Subject: gnu: Add metamath
Date: Fri, 24 Apr 2020 20:48:30 +0900
[Message part 1 (text/plain, inline)]
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!

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

Information forwarded to guix-patches <at> gnu.org:
bug#40815; Package guix-patches. (Sun, 26 Apr 2020 17:31:02 GMT) Full text and rfc822 format available.

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

From: Jakub Kądziołka <kuba <at> kadziolka.net>
To: "B. Wilson" <elaexuotee <at> wilsonb.com>
Cc: guix-patches <at> gnu.org
Subject: Re: gnu: Add metamath
Date: Sun, 26 Apr 2020 19:29:45 +0200
[Message part 1 (text/plain, inline)]
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 <at> vkten.in>
>  ;;; Copyright © 2020 Vincent Legoll <vincent.legoll <at> gmail.com>
>  ;;; Copyright © 2020 Nicolò Balzarotti <nicolo <at> nixo.xyz>
> +;;; Copyright © 2020 B. Wilson <elaexuotee <at> 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
[signature.asc (application/pgp-signature, inline)]

Information forwarded to guix-patches <at> gnu.org:
bug#40815; Package guix-patches. (Mon, 27 Apr 2020 04:44:02 GMT) Full text and rfc822 format available.

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

From: x <at> wilsonb.com
To: Jakub Kądziołka <kuba <at> kadziolka.net>
Cc: "B. Wilson" <elaexuotee <at> wilsonb.com>, guix-patches <at> gnu.org
Subject: Re: gnu: Add metamath
Date: Mon, 27 Apr 2020 13:21:03 +0900
[Message part 1 (text/plain, inline)]
Jakub Kądziołka <kuba <at> 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 <at> vkten.in>
> >  ;;; Copyright © 2020 Vincent Legoll <vincent.legoll <at> gmail.com>
> >  ;;; Copyright © 2020 Nicolò Balzarotti <nicolo <at> nixo.xyz>
> > +;;; Copyright © 2020 B. Wilson <elaexuotee <at> 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
[signature.asc (application/pgp-signature, attachment)]

Information forwarded to guix-patches <at> gnu.org:
bug#40815; Package guix-patches. (Mon, 27 Apr 2020 12:14:02 GMT) Full text and rfc822 format available.

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

From: Jakub Kądziołka <kuba <at> kadziolka.net>
To: x <at> wilsonb.com
Cc: "B. Wilson" <elaexuotee <at> wilsonb.com>, guix-patches <at> gnu.org
Subject: Re: gnu: Add metamath
Date: Mon, 27 Apr 2020 14:12:48 +0200
[Message part 1 (text/plain, inline)]
On Mon, Apr 27, 2020 at 01:21:03PM +0900, x <at> 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
[signature.asc (application/pgp-signature, inline)]

Information forwarded to guix-patches <at> gnu.org:
bug#40815; Package guix-patches. (Mon, 11 May 2020 11:27:01 GMT) Full text and rfc822 format available.

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

From: "B. Wilson" <elaexuotee <at> wilsonb.com>
To: Jakub Kądziołka <kuba <at> kadziolka.net>
Cc: guix-patches <at> gnu.org
Subject: Re: gnu: Add metamath
Date: Mon, 11 May 2020 20:25:36 +0900
[Message part 1 (text/plain, inline)]
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.

[0001-gnu-Add-texlive-mathstyle.patch (text/x-patch, attachment)]
[0002-gnu-Add-texlive-flexisym.patch (text/x-patch, attachment)]
[0003-gnu-Add-texlive-breqn.patch (text/x-patch, attachment)]
[0004-gnu-Add-texlive-makecell.patch (text/x-patch, attachment)]
[0005-gnu-Add-texlive-microtype.patch (text/x-patch, attachment)]
[0006-gnu-Add-texlive-tabu.patch (text/x-patch, attachment)]
[0007-gnu-Add-metamath.patch (text/x-patch, attachment)]
[Message part 9 (text/plain, inline)]
Jakub Kądziołka <kuba <at> kadziolka.net> wrote:
> On Mon, Apr 27, 2020 at 01:21:03PM +0900, x <at> 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


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

Information forwarded to guix-patches <at> gnu.org:
bug#40815; Package guix-patches. (Mon, 11 May 2020 14:08:01 GMT) Full text and rfc822 format available.

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

From: "B. Wilson" <elaexuotee <at> wilsonb.com>
To: guix-patches <at> gnu.org
Cc: Jakub Kądziołka <kuba <at> kadziolka.net>
Subject: Re: gnu: Add metamath
Date: Mon, 11 May 2020 23:05:48 +0900
[Message part 1 (text/plain, inline)]
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.

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

Information forwarded to guix-patches <at> gnu.org:
bug#40815; Package guix-patches. (Wed, 13 May 2020 07:26:02 GMT) Full text and rfc822 format available.

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

From: elaexuotee <at> wilsonb.com
To: 40815 <at> debbugs.gnu.org
Subject: gnu: Add metamath.
Date: Wed, 13 May 2020 16:25:11 +0900
[Message part 1 (text/plain, inline)]
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.

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

Information forwarded to guix-patches <at> gnu.org:
bug#40815; Package guix-patches. (Thu, 04 Jun 2020 17:50:01 GMT) Full text and rfc822 format available.

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

From: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
To: "B. Wilson via Guix-patches" via <guix-patches <at> gnu.org>
Cc: Jakub Kądziołka <kuba <at> kadziolka.net>,
 "B. Wilson" <elaexuotee <at> wilsonb.com>, 40815 <at> debbugs.gnu.org
Subject: Re: [bug#40815] gnu: Add metamath
Date: Thu, 04 Jun 2020 19:49:28 +0200
Hello,

"B. Wilson via Guix-patches" via <guix-patches <at> 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




Information forwarded to guix-patches <at> gnu.org:
bug#40815; Package guix-patches. (Thu, 04 Jun 2020 17:50:02 GMT) Full text and rfc822 format available.

Information forwarded to guix-patches <at> gnu.org:
bug#40815; Package guix-patches. (Tue, 23 Jun 2020 11:33:01 GMT) Full text and rfc822 format available.

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

Information forwarded to guix-patches <at> gnu.org:
bug#40815; Package guix-patches. (Wed, 24 Jun 2020 01:16:01 GMT) Full text and rfc822 format available.

Message #35 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: Wed, 24 Jun 2020 10:14:39 +0900
[Message part 1 (text/plain, inline)]
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.

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

Information forwarded to guix-patches <at> gnu.org:
bug#40815; Package guix-patches. (Fri, 26 Jun 2020 07:20:01 GMT) Full text and rfc822 format available.

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

From: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
To: elaexuotee <at> wilsonb.com
Cc: Jakub Kądziołka <kuba <at> kadziolka.net>,
 40815 <at> debbugs.gnu.org
Subject: Re: [bug#40815] gnu: Add metamath
Date: Fri, 26 Jun 2020 09:19:56 +0200
Hello,

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




Information forwarded to guix-patches <at> gnu.org:
bug#40815; Package guix-patches. (Fri, 26 Jun 2020 08:47:02 GMT) Full text and rfc822 format available.

Message #41 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: Fri, 26 Jun 2020 17:46:22 +0900
[Message part 1 (text/plain, inline)]
> 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!

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

Information forwarded to guix-patches <at> gnu.org:
bug#40815; Package guix-patches. (Sun, 28 Jun 2020 20:13:01 GMT) Full text and rfc822 format available.

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

From: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
To: elaexuotee <at> wilsonb.com
Cc: Jakub Kądziołka <kuba <at> kadziolka.net>,
 40815 <at> debbugs.gnu.org
Subject: Re: [bug#40815] gnu: Add metamath
Date: Sun, 28 Jun 2020 22:12:09 +0200
Hello,

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




Information forwarded to guix-patches <at> gnu.org:
bug#40815; Package guix-patches. (Mon, 29 Jun 2020 07:11:02 GMT) Full text and rfc822 format available.

Message #47 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: Mon, 29 Jun 2020 16:09:57 +0900
[Message part 1 (text/plain, inline)]
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.
[signature.asc (application/pgp-signature, attachment)]

Reply sent to Nicolas Goaziou <mail <at> nicolasgoaziou.fr>:
You have taken responsibility. (Wed, 01 Jul 2020 11:03:01 GMT) Full text and rfc822 format available.

Notification sent to "B. Wilson" <elaexuotee <at> wilsonb.com>:
bug acknowledged by developer. (Wed, 01 Jul 2020 11:03:01 GMT) Full text and rfc822 format available.

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

From: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
To: elaexuotee <at> wilsonb.com
Cc: Jakub Kądziołka <kuba <at> kadziolka.net>,
 40815-done <at> debbugs.gnu.org
Subject: Re: [bug#40815] gnu: Add metamath
Date: Wed, 01 Jul 2020 13:02:37 +0200
Hello,

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




Information forwarded to guix-patches <at> gnu.org:
bug#40815; Package guix-patches. (Wed, 01 Jul 2020 23:55:01 GMT) Full text and rfc822 format available.

Message #55 received at 40815-done <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-done <at> debbugs.gnu.org
Subject: Re: [bug#40815] gnu: Add metamath
Date: Thu, 02 Jul 2020 08:53:59 +0900
[Message part 1 (text/plain, inline)]
Excellent. Thanks for cleaning up the things I missed and pushing.

Nicolas Goaziou <mail <at> nicolasgoaziou.fr> wrote:
> Hello,
> 
> elaexuotee <at> 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,


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

bug archived. Request was from Debbugs Internal Request <help-debbugs <at> gnu.org> to internal_control <at> debbugs.gnu.org. (Thu, 30 Jul 2020 11:24:04 GMT) Full text and rfc822 format available.

This bug report was last modified 3 years and 242 days ago.

Previous Next


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