GNU bug report logs - #40815
gnu: Add metamath

Previous Next

Full log

View this message in rfc822 format

From: help-debbugs <at> gnu.org (GNU bug Tracking System)
To: "B. Wilson" <elaexuotee <at> wilsonb.com>
Subject: bug#40815: closed (Re: [bug#40815] gnu: Add metamath)
Date: Wed, 01 Jul 2020 11:03:01 +0000

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

Your bug report

#40815: gnu: Add metamath

which was filed against the guix-patches package, has been closed.

The explanation is attached below, along with your original report.
If you require more details, please reply to 40815 <at> debbugs.gnu.org.

-- 
40815: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=40815
GNU Bug Tracking System
Contact help-debbugs <at> gnu.org with problems

[Message part 2 (message/rfc822, inline)]

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

[Message part 3 (message/rfc822, inline)]

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

Previous Next

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