From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp2 ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms11 with LMTPS id 4JsZH5002V4dFQAA0tVLHw (envelope-from ) for ; Thu, 04 Jun 2020 17:51:25 +0000 Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp2 with LMTPS id wET0Gp002V5hXAAAB5/wlQ (envelope-from ) for ; Thu, 04 Jun 2020 17:51:25 +0000 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id F17AC940058 for ; Thu, 4 Jun 2020 17:51:24 +0000 (UTC) Received: from localhost ([::1]:44276 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1jgu1T-00017s-SI for larch@yhetil.org; Thu, 04 Jun 2020 13:51:23 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:33838) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1jgu0A-0008Bu-H6 for guix-patches@gnu.org; Thu, 04 Jun 2020 13:50:02 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:35881) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1jgu0A-0007u3-47 for guix-patches@gnu.org; Thu, 04 Jun 2020 13:50:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1jgu0A-0006GW-1M for guix-patches@gnu.org; Thu, 04 Jun 2020 13:50:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#40815] gnu: Add metamath Resent-From: Nicolas Goaziou Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Thu, 04 Jun 2020 17:50:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 40815 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: To: 40815@debbugs.gnu.org Cc: kuba@kadziolka.net, elaexuotee@wilsonb.com X-Debbugs-Original-To: "B. Wilson via Guix-patches" via X-Debbugs-Original-Cc: Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= , "B. Wilson" , 40815@debbugs.gnu.org Received: via spool by 40815-submit@debbugs.gnu.org id=B40815.159129297924039 (code B ref 40815); Thu, 04 Jun 2020 17:50:01 +0000 Received: (at 40815) by debbugs.gnu.org; 4 Jun 2020 17:49:39 +0000 Received: from localhost ([127.0.0.1]:47424 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jgtzn-0006Fe-AB for submit@debbugs.gnu.org; Thu, 04 Jun 2020 13:49:39 -0400 Received: from relay10.mail.gandi.net ([217.70.178.230]:54499) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jgtzl-0006FK-Cl for 40815@debbugs.gnu.org; Thu, 04 Jun 2020 13:49:37 -0400 Received: from localhost (40-67.ipv4.commingeshautdebit.fr [185.131.40.67]) (Authenticated sender: admin@nicolasgoaziou.fr) by relay10.mail.gandi.net (Postfix) with ESMTPSA id 376A5240003; Thu, 4 Jun 2020 17:49:29 +0000 (UTC) From: Nicolas Goaziou References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> <20200426172945.7ez6i2fl3pjcoexd@gravity> <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com> <20200427121248.cga7p43flnusf7zo@gravity> <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com> <25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com> Date: Thu, 04 Jun 2020 19:49:28 +0200 In-Reply-To: <25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com> (B. Wilson via Guix-patches's message of "Mon, 11 May 2020 23:05:48 +0900") Message-ID: <87d06eraaf.fsf@nicolasgoaziou.fr> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: -0.7 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-Spam-Score: -1.7 (-) X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: "Guix-patches" X-Scanner: scn0 Authentication-Results: aspmx1.migadu.com; dkim=none; dmarc=none; spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org X-Spam-Score: -1.01 X-TUID: tIBp3sVQojgE Hello, "B. Wilson via Guix-patches" via 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/- 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