From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:470:142:3::10]:50264) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1jSvck-0003Dw-Bs for guix-patches@gnu.org; Mon, 27 Apr 2020 00:44:10 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.90_1) (envelope-from ) id 1jSvcg-0002cn-Qe for guix-patches@gnu.org; Mon, 27 Apr 2020 00:44:06 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:52026) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1jSvcg-0002ba-Cg for guix-patches@gnu.org; Mon, 27 Apr 2020 00:44:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1jSvcg-0002t5-94 for guix-patches@gnu.org; Mon, 27 Apr 2020 00:44:02 -0400 Subject: [bug#40815] gnu: Add metamath Resent-Message-ID: Received: from eggs.gnu.org ([2001:470:142:3::10]:48408) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1jSvH0-0003Ez-7D for guix-patches@gnu.org; Mon, 27 Apr 2020 00:21:42 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.90_1) (envelope-from ) id 1jSvGw-0005qL-Gu for guix-patches@gnu.org; Mon, 27 Apr 2020 00:21:37 -0400 Received: from m42-5.mailgun.net ([69.72.42.5]:30203) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1jSvGv-0005m8-Ur for guix-patches@gnu.org; Mon, 27 Apr 2020 00:21:34 -0400 Date: Mon, 27 Apr 2020 13:21:03 +0900 References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com> <20200426172945.7ez6i2fl3pjcoexd@gravity> In-Reply-To: <20200426172945.7ez6i2fl3pjcoexd@gravity> Message-Id: <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com> MIME-Version: 1.0 Content-Type: multipart/signed; micalg="pgp-sha1"; protocol="application/pgp-signature"; boundary="----_=_066652fb3881ddd546832cb7_=_" List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" Reply-to: x@wilsonb.com, x--- via Guix-patches From: x--- via Guix-patches via To: Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= Cc: elaexuotee@wilsonb.com, 40815@debbugs.gnu.org This is a multipart message in MIME format. ------_=_066652fb3881ddd546832cb7_=_ MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----_=_4c7ce6301e5de0be6c4a9da4_=_" This is a multipart message in MIME format. ------_=_4c7ce6301e5de0be6c4a9da4_=_ Content-Type: text/plain; charset=UTF-8 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Jakub K=C4=85dzio=C5=82ka 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. >=20 > 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 =C2=A9 2020 R Veera Kumar > > ;;; Copyright =C2=A9 2020 Vincent Legoll > > ;;; Copyright =C2=A9 2020 Nicol=C3=B2 Balzarotti > > +;;; Copyright =C2=A9 2020 B. Wilson >=20 > 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 neglect= ed website. > > +(define-public metamath > > + (package > > + (name "metamath") > > + (version "0.182") > > + (source > > + (origin > > + (method url-fetch) > > + (uri "http://us2.metamath.org/downloads/metamath-program.zip") >=20 > 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) o= nly contains a single, outdated release tar, which is simply a spurious byprodu= ct 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, b= ut 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 her= e. 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? >=20 > AFAIK, building from source is preferred. grep for texlive-union to see > how it can be done without pulling in gigabytes of dependencies. >=20 > 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"))))))= ) >=20 > Let me cite an excerpt from your build log: ;) >=20 > ## WARNING: phase `install-doc' returned `#'. 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. >=20 > 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 t= he repo. My reasoning for using the forms directly is simply that they only ge= t used once. Anyway, my revised patch will include the `let' since that's ind= eed more idiomatic. > > Also, regarding my `install-doc' phase, is the way I copy over the > > /gnu/store/-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? >=20 > 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 abo= ve revisions, the confirmation is helpful. > > diff --git a/gnu/packages/patches/metamath-remove-missing-file-refs.pat= ch 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 >=20 > Make sure to add this new file to gnu/local.mk! >=20 > > @@ -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) > > +=20 > > +-dist_pkgdata_DATA =3D \ > > +- big-unifier.mm \ > > +- demo0.mm \ > > +- miu.mm \ > > +- peano.mm \ > > +- ql.mm \ > > +- set.mm > > +- > > +=20 > > + EXTRA_DIST =3D \ > > + LICENSE.TXT \ >=20 > 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 bu= t will try to push the fix to upstream as well. > Regards, > Jakub K=C4=85dzio=C5=82ka Thank you for the thorough review! I will give this package another try. Cheers, B. Wilson ------_=_4c7ce6301e5de0be6c4a9da4_=_-- ------_=_066652fb3881ddd546832cb7_=_ Content-Disposition: attachment; filename=signature.asc Content-Type: application/pgp-signature Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- iQEzBAABCAAdFiEEgkvKaje0gDM2mRnu9Mg1slJBq0oFAl6mXZ0ACgkQ9Mg1slJB q0pSbAf/SN+gzr0Nc0i7IY9ARkdh1oPWHsGxwnb56yRagqC7YIZj0xS42FmW0GUZ pvS213gfvgZ5LNEvr6nBpfvbvk9Qo1pqRF6h1VSFr1+E4HIvMrPxiRWLk3zgqMP3 WEGOQX5nbdWSHVFb+7j/WbWVAnHUOXUbmLzB3SQi3QnRA8KMgendfskS9maA4hvP DMYm+/fG7xQP9o8sPugqerrwatMTSqDtjHeBgd7FtFAyCHAT9XILEzUZqaBBOPLL B0QqvuHRsEKGlkXH1GVAYrW5MBWWDoiYrQwRTye1hkumexXXczeebXPZ10vVWH5w 52rsK2J9mnKTH9gGLIfeZOU4pf6kZA== =lU/t -----END PGP SIGNATURE----- ------_=_066652fb3881ddd546832cb7_=_--