GNU bug report logs - #40815
gnu: Add metamath

Previous Next

Full log

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

Previous Next

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