gnu: Add metamath

DoneSubmitted by B. Wilson.
Details
4 participants
  • B. Wilson
  • Jakub Kądziołka
  • Nicolas Goaziou
  • x
Owner
unassigned
Severity
normal
B
B
B. Wilson wrote on 24 Apr 13:48 +0200
(address . guix-patches@gnu.org)
3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com
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!
From 808e8d73cb231d2fbf34b88683fb0c3fe5d631e9 Mon Sep 17 00:00:00 2001From: "B. Wilson" <elaexuotee@wilsonb.com>Date: Thu, 23 Apr 2020 20:28:49 +0900Subject: [PATCH] gnu: Add metamath
* gnu/packages/maths.scm (metamath): New variable.* gnu/packages/patches/metamath-remove-missing-file-refs.patch: New file.--- gnu/packages/maths.scm | 45 +++++++++++++++++++ .../metamath-remove-missing-file-refs.patch | 17 +++++++ 2 files changed, 62 insertions(+) create mode 100644 gnu/packages/patches/metamath-remove-missing-file-refs.patch
Toggle diff (85 lines)diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scmindex 73ee161e81..c70557ef8f 100644--- a/gnu/packages/maths.scm+++ b/gnu/packages/maths.scm@@ -38,6 +38,7 @@ ;;; Copyright © 2020 R Veera Kumar <vkor@vkten.in> ;;; Copyright © 2020 Vincent Legoll <vincent.legoll@gmail.com> ;;; Copyright © 2020 Nicolò Balzarotti <nicolo@nixo.xyz>+;;; Copyright © 2020 B. Wilson <elaexuotee@wilsonb.com> ;;; ;;; This file is part of GNU Guix. ;;;@@ -5519,3 +5520,47 @@ and conversions, physical constants, symbolic calculations (including integrals and equations), arbitrary precision, uncertainity propagation, interval arithmetic, plotting.") (license license:gpl2+)))++(define-public metamath+ (package+ (name "metamath")+ (version "0.182")+ (source+ (origin+ (method url-fetch)+ (uri "http://us2.metamath.org/downloads/metamath-program.zip")+ (sha256+ (base32 "0k1ffd1bglkgdb6pkjnxw3dc7p697x70nx8hcpvw9cwbv3k9vf71"))+ (patches (search-patches "metamath-remove-missing-file-refs.patch"))))+ (build-system gnu-build-system)+ (inputs+ `(("book"+ ,(origin+ (method url-fetch)+ (uri "http://us2.metamath.org/downloads/metamath.pdf")+ (sha256+ (base32 "0nc0dz2zk8n2yija8qdvdgnmpqafyfl1nxf3yrr9g2hldnqvlpi4"))))))+ (native-inputs `(("autoconf" ,autoconf)+ ("automake" ,automake)+ ("unzip" ,unzip)))+ (outputs '("out" "doc"))+ (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")))))))+ (home-page "http://us.metamath.org/")+ (synopsis "Proof verifier based on a minimalistic formalism")+ (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+Arithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc. See the+Metamath book")+ (license license:gpl2+)))diff --git a/gnu/packages/patches/metamath-remove-missing-file-refs.patch b/gnu/packages/patches/metamath-remove-missing-file-refs.patchnew file mode 100644index 0000000000..bc4748de98--- /dev/null+++ b/gnu/packages/patches/metamath-remove-missing-file-refs.patch@@ -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 \-- 2.26.2
Attachment: signature.asc
J
J
Jakub Kądziołka wrote on 26 Apr 19:29 +0200
(name . B. Wilson)(address . elaexuotee@wilsonb.com)(address . guix-patches@gnu.org)
20200426172945.7ez6i2fl3pjcoexd@gravity
On Fri, Apr 24, 2020 at 08:48:30PM +0900, B. Wilson wrote:
Toggle quote (3 lines)> This is my first packaging attempt, so careful critiques are very> welcome.
Welcome to Guix, then!
Toggle quote (10 lines)> 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@vkten.in>> ;;; Copyright © 2020 Vincent Legoll <vincent.legoll@gmail.com>> ;;; Copyright © 2020 Nicolò Balzarotti <nicolo@nixo.xyz>> +;;; Copyright © 2020 B. Wilson <elaexuotee@wilsonb.com>
Huh, we usually don't abbreviate first names. It's fine if you prefer itthis way, though. (BTW, the LaTeX on your website is broken.)
Toggle quote (9 lines)> +(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 whenupstream will release a new version, it will break the hash below. Ilooked around on their website and couldn't find a versioned URL, but Ialso couldn't find the one you're using. We could fetch from GitHubinstead...
Toggle quote (7 lines)> 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 seehow it can be done without pulling in gigabytes of dependencies.
The no-versioned-URL problem also applies to the documentation, andthis would let you solve two problems at once ;)
Toggle quote (10 lines)> + (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)
Toggle quote (6 lines)> 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.
Toggle quote (6 lines)> 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!
Toggle quote (19 lines)> @@ -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 thereasoning behind that seems not entirely clear to me - wouldn't theprogram be more useful when packaged with its database?
Regards,Jakub Kądziołka
-----BEGIN PGP SIGNATURE-----
iQIzBAABCAAdFiEE5Xa/ss9usT31cTO54xWnWEYTFWQFAl6lxQUACgkQ4xWnWEYTFWTWrQ//YvS+LnMl9qyPMprweSuHNuo3ZitJ4qSwETrk3k7lXaRwW/vtL5+NTZKv0H/gRNA23yEyfZ9spUNWQPS4Q52vYNtOg24yQFvYjPXUBVHSUzlHSVaQSXwbnIz5RNY+B5orPum+plPbXxPSopuxXew1QmzSU5mqMxVbl445zlGEAv7j40TyIbnTWT0FX14mYtu/RPll2EBhxmIu+xXXr963zGsgV8RU+7sb7DzuK0DKFesZW95wZdSu+eIEJv6vHxs9Xai33rFbEmz7j3zDKpUL9jTCju2xmvkP1Jl9yUPgKIpmwaPoIz1kiB01qPTZIYXpekO5FOgaZkBsRS3pxtBLhWARDoEriyZ6LywXtlnLYS0PBqgf1fP386//Aj8ueSvBR9G5d0JW/4ggtoAPrAUDg9ndhDSs5LGnROIWSKv52HwslBNzc5BA+7KyuHxbZG5EVbC7uvDSUtBJ3YAbgydJYCng3OF90UUnpgVKKXF6hTmF+N3jrFHPtiUfXK0gKETUS2wi6PtX6nWeT5GPSTuGPF0i/MYF6QjdJPnpGkKLezNmMirnvarQNxiuOH1T+vcbzGJ4xZXPAuKZ4hu4Uq3NNZGYugOT5Mvk5CzdPmAd/AS/jw75lAwUZFYf+YXHSV8XYZDNfmA376KjikFgvuZCfHoQoYLFj/rQaN5mFS82PPQ==q6hC-----END PGP SIGNATURE-----

X
(name . Jakub Kądziołka)(address . kuba@kadziolka.net)
2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com
Jakub Kądziołka <kuba@kadziolka.net> wrote:
Toggle quote (6 lines)> 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!
Toggle quote (13 lines)> > 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@vkten.in>> > ;;; Copyright © 2020 Vincent Legoll <vincent.legoll@gmail.com>> > ;;; Copyright © 2020 Nicolò Balzarotti <nicolo@nixo.xyz>> > +;;; Copyright © 2020 B. Wilson <elaexuotee@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 aproblem, I do not mind chosing some other alias.
Also, thank you for taking the time to audit my meagre and severely neglectedwebsite.
Toggle quote (15 lines)> > +(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 getsupdated daily via some automatic script. The reason being that they alsoprovide snapshots of the databases from the set.mm repository.
To boot, the GitHub repository (https://github.com/metamath/metamath-exe)onlycontains a single, outdated release tar, which is simply a spurious byproductof a prolonged discussion I had with upstream regarding the problems theirrelease tars pose for package maintainers.
All in all I spent a few weeks discussing the problem, eventually resulting inthe url seen in the patch. IIRC this url did end up on the main homepage, butfor some reason it seems to be missing now.
There were other technical complications, but the current status is thatupstream is a single developer making a special effort to accomodate us here.The rest of the (quite small) metamath community mostly just conform'sto the somewhat anachronistic workflow that the developer has in place.
Anyway, I recognize the current status makes packaging problematic and willopen a dialog with upstream again, but given the background, I am not sure howthis will go.
Toggle quote (13 lines)> > 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.
Toggle quote (24 lines)> > + (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 therepo. My reasoning for using the forms directly is simply that they only getused once. Anyway, my revised patch will include the `let' since that's indeedmore idiomatic.
Toggle quote (9 lines)> > 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 aboverevisions, the confirmation is helpful.
Toggle quote (31 lines)> > 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'tactually include the files, which are expected to be cloned from the set.mmrepository. I don't have full insight as to why Makefile.am is like this butwill try to push the fix to upstream as well.
Toggle quote (3 lines)> Regards,> Jakub Kądziołka
Thank you for the thorough review! I will give this package another try.

Cheers,
B. Wilson
Attachment: signature.asc
J
J
Jakub Kądziołka wrote on 27 Apr 14:12 +0200
(address . x@wilsonb.com)
20200427121248.cga7p43flnusf7zo@gravity
On Mon, Apr 27, 2020 at 01:21:03PM +0900, x@wilsonb.com wrote:
Toggle quote (26 lines)> > > +(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. Wecould pin a specific commit ID. This practice is relatively common inGuix and does not pose a problem.
Regards,Jakub Kądziołka
-----BEGIN PGP SIGNATURE-----
iQIzBAABCAAdFiEE5Xa/ss9usT31cTO54xWnWEYTFWQFAl6mzDoACgkQ4xWnWEYTFWSMcA//ZY1G0QDy9ZPMdTqUxb6HO2bgd20g44sU8nRZXkQYKkLCuCGpu3we4zbzvt5F1CprCZh6GkdGfZi6ROj/o42C+hW8R1uRg4Q2gWNFq1NaqyL/ie5SWL0Xoa9gU0ClJZnwK9a2dEDbEj5X6dZJUzSLBBmv9l4Dm5Sr14w0ijovZmI8vz6IGlJ8fZoEz7TMOz/XgEgGg7OMmjok9Q0FrS36xKmkiak+BNC9t1ozMbHfVI3XNKn3ba4tmktBwyCtOSKJ5T+gv5myAtIlxJn3dseOHX9T+TuUKAyYFLTwdantdNvWDMuIOy9eE4A3xTHbhTNYzAwu+WAgY5Pg6OtqUNnFfN5qb0JqEQFChUW/dY27/INdA+kgMhSdat34L1dKGobUs22cWPxrQN1JpuxMVVB7YZC48/B/O6JYC3VhS3h7Lwt+Pl9IhHM0XEUoV2hRTzrHl3J5AflC7uVFLlGxqW/fF7yHVXd2ip9koXIayj52OzyBZnc1VIXdHYX0GB/7dS/nX7bqFQ0Eoz4nsvTmFbJkObEPKJLjY5ITRjH0EWle0NuDNUiIt1Ul1L799tED8iRFbIpxGsgtS3keaK0SxcNO4dWxeFMflk8XvnEc7smqGj5uKzS5888h80ta2EAvxC2vMt4VxtRSJ6w5BKVls7diIn9/yons4OD4zv4atan91hM==f/wi-----END PGP SIGNATURE-----

B
B
B. Wilson wrote on 11 May 13:25 +0200
(name . Jakub Kądziołka)(address . kuba@kadziolka.net)(address . guix-patches@gnu.org)
3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com
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 wedon't need a patch; and now we're generating the doc output's pdf from the TeXsource.
The latter is what made this take so much time and effort.
On the one hand, it required packaging up 6 texlive dependencies, which areincluded in the attached patches. On the other hand, it turns out that thetexlive-amsfonts package is broken, which we need to typset the metamath docoutput. 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 buildsjust fine.
Regarding the patches for the texlive packages, I did all of them assimple-texlive-package templates with #:trivial? #t, grabbing the files fromtex/latex and doc/latex. Is this reasonable? Looking at other packages, Icannot 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 resideunder latex/breqn, but since they have their own ctan pages, I opted to splitthem into separate packages and make the dependencies explicit. Does that seemreasonable?
Anyway, thanks for taking a look! Hopefully, these look mergeable apart fromthe texlive-amsfonts issue.
From 2f1efc596c83ae4bf63925c612b54161f55838a1 Mon Sep 17 00:00:00 2001From: "B. Wilson" <elaexuotee@wilsonb.com>Date: Mon, 11 May 2020 20:02:41 +0900Subject: [PATCH 1/7] gnu: Add texlive-mathstyle.To: guix-patches@gnu.org
* gnu/packages/tex.scm (texlive-mathstyle): New Variable.--- gnu/packages/tex.scm | 17 +++++++++++++++++ 1 file changed, 17 insertions(+)
Toggle diff (34 lines)diff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scmindex 683f9d7283..f6d92b5f1c 100644--- a/gnu/packages/tex.scm+++ b/gnu/packages/tex.scm@@ -13,6 +13,7 @@ ;;; Copyright © 2018 Danny Milosavljevic <dannym+a@scratchpost.org> ;;; Copyright © 2018 Arun Isaac <arunisaac@systemreboot.net> ;;; Copyright © 2020 Vincent Legoll <vincent.legoll@gmail.com>+;;; Copyright © 2020 B. Wilson <elaexuotee@wilsonb.com> ;;; ;;; This file is part of GNU Guix. ;;;@@ -7322,3 +7323,19 @@ facilities designed to cope with the more specific demands of academic writing, especially in the humanities and the social sciences. All quote styles as well as the optional active quotes are freely configurable.") (license license:lppl1.3c+))))++(define-public texlive-mathstyle+ (package+ (inherit (simple-texlive-package+ "texlive-mathstyle"+ (list "/tex/latex/breqn/mathstyle.sty"+ "/doc/latex/breqn/mathstyle.pdf")+ (base32 "0rlnp20ns70ir0sac4qwcigr4a25s813cijvjamwm6q42y6wj8vp")+ #:trivial? #t))+ (propagated-inputs `(("texlive-latex-l3kernel" ,texlive-latex-l3kernel)))+ (home-page "https://www.ctan.org/pkg/mathstyle")+ (synopsis "Manage mathematics typesetting style")+ (description "Flexisym converts mathematical symbol definitions to the form+they need for breqn to work. The package offers support for breqn and is part+of the bundle of the same name.")+ (license license:lppl1.3c+)))-- 2.26.2
From 03068f1e5f01fde67f53aa1ea7dcb477c0ab669e Mon Sep 17 00:00:00 2001From: "B. Wilson" <elaexuotee@wilsonb.com>Date: Mon, 11 May 2020 20:03:54 +0900Subject: [PATCH 2/7] gnu: Add texlive-flexisym.To: guix-patches@gnu.org
* gnu/packages/tex.scm (texlive-flexisym): New variable.--- gnu/packages/tex.scm | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+)
Toggle diff (31 lines)diff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scmindex f6d92b5f1c..6727a2c985 100644--- a/gnu/packages/tex.scm+++ b/gnu/packages/tex.scm@@ -7339,3 +7339,24 @@ styles as well as the optional active quotes are freely configurable.") they need for breqn to work. The package offers support for breqn and is part of the bundle of the same name.") (license license:lppl1.3c+)))++(define-public texlive-flexisym+ (package+ (inherit (simple-texlive-package+ "texlive-flexisym"+ (list "/tex/latex/breqn/flexisym.sty"+ "/tex/latex/breqn/cmbase.sym"+ "/tex/latex/breqn/mathpazo.sym"+ "/tex/latex/breqn/mathptmx.sym"+ "/tex/latex/breqn/msabm.sym"+ "/doc/latex/breqn/flexisym.pdf")+ (base32 "0vjhk94s7z83wcb38ww5nzbjywvybfwm6vg7a2yy8ic2sjm0pjxj")+ #:trivial? #t))+ (propagated-inputs `(("texlive-latex-l3kernel" ,texlive-latex-l3kernel)+ ("texlive-mathstyle" ,texlive-mathstyle)))+ (home-page "https://www.ctan.org/pkg/flexisym")+ (synopsis "Symbol manipulation for breqn")+ (description "Flexisym converts mathematical symbol definitions to the form+they need for breqn to work. The package offers support for breqn and is part+of the bundle of the same name.")+ (license license:lppl1.3c+)))-- 2.26.2
From aca179c3100bced9438c91dc25a1cafe9a9814bd Mon Sep 17 00:00:00 2001From: "B. Wilson" <elaexuotee@wilsonb.com>Date: Mon, 11 May 2020 20:05:58 +0900Subject: [PATCH 3/7] gnu: Add texlive-breqn.To: guix-patches@gnu.org
* gnu/packages/tex.scm (texlive-breqn): New variable.--- gnu/packages/tex.scm | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+)
Toggle diff (38 lines)diff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scmindex 6727a2c985..710ad2ba20 100644--- a/gnu/packages/tex.scm+++ b/gnu/packages/tex.scm@@ -7360,3 +7360,31 @@ of the bundle of the same name.") they need for breqn to work. The package offers support for breqn and is part of the bundle of the same name.") (license license:lppl1.3c+)))++(define-public texlive-breqn+ (package+ (inherit (simple-texlive-package+ "texlive-breqn"+ (list "/tex/latex/breqn/breqn.sty"+ "/doc/latex/breqn/breqn.pdf")+ (base32 "0mdm3yyimr8fv8pg2b2zv62fjbx98xy60a3dzj55djdir6hyxf6h")+ #:trivial? #t))+ (propagated-inputs `(("texlive-latex-amsmath" ,texlive-latex-amsmath)+ ("texlive-flexisym" ,texlive-flexisym)+ ("texlive-latex-graphics" ,texlive-latex-graphics)+ ("texlive-latex-l3kernel" ,texlive-latex-l3kernel)+ ("texlive-latex-tools" ,texlive-latex-tools)))+ (home-page "http://wspr.io/breqn/")+ (synopsis "Automated line breaking of displayed equations")+ (description "The package provides solutions to a number of common+difficulties in writing displayed equations and getting high-quality output.+For example, it is a well-known inconvenience that if an equation must be+broken into more than one line, @code{left...right} constructs cannot span+lines. The breqn package makes them work as one would expect whether or not+there is an intervening line break. The single most ambitious goal of the+package, however, is to support automatic linebreaking of displayed equations.+Such linebreaking cannot be done without substantial changes under the hood in+the way formulae are processed; the code must be watched carefully, keeping an+eye on possible glitches. The bundle also contains the flexisym and mathstyle+packages, which are both designated as support for breqn.")+ (license license:lppl1.3c+)))-- 2.26.2
From f3298a40c3fe945c9dc0cbfc3f9a7fa9bfb73cb8 Mon Sep 17 00:00:00 2001From: "B. Wilson" <elaexuotee@wilsonb.com>Date: Mon, 11 May 2020 20:07:03 +0900Subject: [PATCH 4/7] gnu: Add texlive-makecell.To: guix-patches@gnu.org
* gnu/packages/tex.scm (texlive-makecell): New variable.--- gnu/packages/tex.scm | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+)
Toggle diff (39 lines)diff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scmindex 710ad2ba20..ca5b9dbb2e 100644--- a/gnu/packages/tex.scm+++ b/gnu/packages/tex.scm@@ -7388,3 +7388,32 @@ the way formulae are processed; the code must be watched carefully, keeping an eye on possible glitches. The bundle also contains the flexisym and mathstyle packages, which are both designated as support for breqn.") (license license:lppl1.3c+)))++(define-public texlive-makecell+ (package+ (inherit (simple-texlive-package+ "texlive-makecell"+ (list "/tex/latex/makecell/"+ "/doc/latex/makecell/makecell.pdf")+ (base32 "1zdcmya5dxrnjf7lf0wmnhcjlwdha5gdzdx7xrgyi61gqwj7cxin")+ #:trivial? #t))+ (propagated-inputs `(("texlive-latex-tools" ,texlive-latex-tools)))+ (home-page "https://www.ctan.org/pkg/makecell")+ (synopsis "Tabular column heads and multilined cells")+ (description "This package supports common layouts for tabular column heads+in whole documents, based on one-column tabular environment. In addition, it+can create multi-lined tabular cells.++The Package also offers:++@itemize+@item a macro which changes the vertical space around all the cells in a+ tabular environment (similar to the function of the tabls package, but+ using the facilities of the array);+@item macros for multirow cells, which use the facilities of the multirow+ package;+@item macros to number rows in tables, or to skip cells;+@item diagonally divided cells;+@item horizontal lines in tabular environments with defined thickness.+@end itemize")+ (license license:lppl)))-- 2.26.2
From c03dc294ea70b4fe210f038ff14945d0005228c3 Mon Sep 17 00:00:00 2001From: "B. Wilson" <elaexuotee@wilsonb.com>Date: Mon, 11 May 2020 20:08:10 +0900Subject: [PATCH 5/7] gnu: Add texlive-microtype.To: guix-patches@gnu.org
* gnu/packages/tex.scm (texlive-microtype): New variable.--- gnu/packages/tex.scm | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+)
Toggle diff (44 lines)diff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scmindex ca5b9dbb2e..2d290fdb82 100644--- a/gnu/packages/tex.scm+++ b/gnu/packages/tex.scm@@ -7417,3 +7417,37 @@ The Package also offers: @item horizontal lines in tabular environments with defined thickness. @end itemize") (license license:lppl)))++(define-public texlive-microtype+ (package+ (inherit (simple-texlive-package+ "texlive-microtype"+ (list "/tex/latex/microtype/"+ "/doc/latex/microtype/")+ (base32 "0xmjpzbj4nqmnl5m7xx1bshdk2c8n57rmbvn0j479ypj4wdlq9iy")+ #:trivial? #t))+ (propagated-inputs `(("texlive-latex-graphics" ,texlive-latex-graphics)))+ (home-page "https://www.ctan.org/pkg/microtype")+ (synopsis "Subliminal refinements towards typographical perfection")+ (description "The package provides a LaTeX interface to the+micro-typographic extensions that were introduced by pdfTeX and have since also+propagated to XeTeX and LuaTeX: most prominently, character protrusion and font+expansion, furthermore the adjustment of interword spacing and additional+kerning, as well as hyphenatable letterspacing (tracking) and the possibility+to disable all or selected ligatures.++These features may be applied to customisable sets of fonts, and all+micro-typographic aspects of the fonts can be configured in a straight-forward+and flexible way. Settings for various fonts are provided.++Note that character protrusion requires pdfTeX, LuaTeX, or XeTeX. Font+expansion works with pdfTeX or LuaTeX. The package will by default enable+protrusion and expansion if they can safely be assumed to work. Disabling+ligatures requires pdfTeX or LuaTeX, while the adjustment of interword spacing+and of kerning only works with pdfTeX. Letterspacing is available with pdfTeX+or LuaTeX.++The alternative package @code{letterspace}, which also works with plain TeX,+provides the user commands for letterspacing only, omitting support for all+other extensions.")+ (license license:lppl1.3c+)))-- 2.26.2
From 01ce7a13c2897263e754bb8164c2472bc683d6bf Mon Sep 17 00:00:00 2001From: "B. Wilson" <elaexuotee@wilsonb.com>Date: Mon, 11 May 2020 20:09:31 +0900Subject: [PATCH 6/7] gnu: Add texlive-tabu.To: guix-patches@gnu.org
* gnu/packages/tex.scm (texlive-tabu): New variable.--- gnu/packages/tex.scm | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+)
Toggle diff (49 lines)diff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scmindex 2d290fdb82..f382330773 100644--- a/gnu/packages/tex.scm+++ b/gnu/packages/tex.scm@@ -7451,3 +7451,42 @@ The alternative package @code{letterspace}, which also works with plain TeX, provides the user commands for letterspacing only, omitting support for all other extensions.") (license license:lppl1.3c+)))++(define-public texlive-tabu+ (package+ (inherit (simple-texlive-package+ "texlive-tabu"+ (list "/tex/latex/tabu/"+ "/doc/latex/tabu/")+ (base32 "156lkisyrpvn82ng2kxdlly60ny5vaz4lp9xlc66azy5ma06agvw")+ #:trivial? #t))+ (propagated-inputs+ `(("texlive-latex-tools" ,texlive-latex-tools)+ ("texlive-latex-varwidth" ,texlive-latex-varwidth)))+ (home-page "https://www.ctan.org/pkg/tabu")+ (synopsis "Flexible LaTeX tabulars")+ (description "The package provides an environment, @code{tabu}, which will+make any sort of tabular (that doesn’t need to split across pages), and an+environment @code{longtabu} which provides the facilities of @code{tabu} in a+modified longtable environment. (Note that this latter offers an enhancement+of ltxtable.)++The package requires the array package, and needs e-TeX to run (since array.sty+is present in every conforming distribution of LaTeX, and since every publicly+available LaTeX format is built using e-TeX, the requirements are provided by+default on any reasonable system). The package also requires xcolor for+coloured rules in tables, and colortbl for coloured cells. The @code{longtabu}+environment further requires that longtable be loaded. The package itself does+not load any of these packages for the user.++The @code{tabu} environment may be used in place of @code{tabular},+@code{tabular*} and @code{tabularx} environments, as well as the @code{array}+environment in maths mode. It overloads @code{tabularx}’s X-column+specification, allowing a width specification, alignment (@code{l}, @code{r},+@code{c} and @code{j}) and column type indication (@code{p}, @code{m} and+@code{b}).++@code{\begin@{tabu@}} to @code{<dimen>} specifies a target width, and+@code{\begin@{tabu@}} spread @code{<dimen>} enlarges the environment’s+natural width.")+ (license license:lppl1.3c+)))-- 2.26.2
From 7fd676d14283204b9f367d301293af339c8906a1 Mon Sep 17 00:00:00 2001From: "B. Wilson" <elaexuotee@wilsonb.com>Date: Mon, 11 May 2020 20:10:48 +0900Subject: [PATCH 7/7] gnu: Add metamath.To: guix-patches@gnu.org
* gnu/packages/maths.scm (metamath): New variable.--- gnu/packages/maths.scm | 74 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 74 insertions(+)
Toggle diff (91 lines)diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scmindex 8fbce15418..2054e1ad8e 100644--- a/gnu/packages/maths.scm+++ b/gnu/packages/maths.scm@@ -38,6 +38,7 @@ ;;; Copyright © 2020 R Veera Kumar <vkor@vkten.in> ;;; Copyright © 2020 Vincent Legoll <vincent.legoll@gmail.com> ;;; Copyright © 2020 Nicolò Balzarotti <nicolo@nixo.xyz>+;;; Copyright © 2020 B. Wilson <elaexuotee@wilsonb.com> ;;; ;;; This file is part of GNU Guix. ;;;@@ -5615,3 +5616,76 @@ and conversions, physical constants, symbolic calculations (including integrals and equations), arbitrary precision, uncertainity propagation, interval arithmetic, plotting.") (license license:gpl2+)))++(define-public metamath+ (package+ (name "metamath")+ (version "0.182")+ (source+ (origin+ (method git-fetch)+ (uri (git-reference+ (url "https://github.com/metamath/metamath-exe.git")+ (commit "5df616efe4119ff88daf77e7041d45b6fa39c578")))+ (sha256+ (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"))))+ (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"))+ (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"))+ (arguments+ `(#:phases+ (let ((book-builddir "metamath-book-second_edition"))+ (modify-phases %standard-phases+ (add-after 'unpack 'unpack-doc+ (lambda* (#:key inputs #:allow-other-keys)+ (let ((book-tar (assoc-ref inputs "book")))+ (invoke "tar" "xzf" book-tar))))+ (add-after 'build 'build-doc+ (lambda _+ (with-directory-excursion book-builddir+ (invoke "touch" "metamath.ind")+ (invoke "pdflatex" "metamath")+ (invoke "pdflatex" "metamath")+ (invoke "bibtex" "metamath")+ (invoke "makeindex" "metamath")+ (invoke "pdflatex" "metamath")+ (invoke "pdflatex" "metamath"))))+ (add-after 'build-doc 'install-doc+ (lambda* (#:key outputs #:allow-other-keys)+ (let ((docdir (assoc-ref outputs "doc")))+ (install-file+ (string-append book-builddir "/metamath.pdf")+ (string-append docdir "/share/doc/metamath"))+ #t)))))))+ (home-page "http://us.metamath.org/")+ (synopsis "Proof verifier based on a minimalistic formalism")+ (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+Arithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc. See the+Metamath book")+ (license license:gpl2+)))-- 2.26.2
Jakub Kądziołka <kuba@kadziolka.net> wrote:
Toggle quote (33 lines)> On Mon, Apr 27, 2020 at 01:21:03PM +0900, x@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
Attachment: signature.asc
B
B
B. Wilson wrote on 11 May 16:05 +0200
(address . guix-patches@gnu.org)(name . Jakub Kądziołka)(address . kuba@kadziolka.net)
25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com
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.
From f7c803351c483ff0efe0e65604fec3de001f7282 Mon Sep 17 00:00:00 2001From: "B. Wilson" <elaexuotee@wilsonb.com>Date: Mon, 11 May 2020 20:10:48 +0900Subject: [PATCH] gnu: Add metamath.To: guix-patches@gnu.org
* gnu/packages/maths.scm (metamath): New variable.--- gnu/packages/maths.scm | 75 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+)
Toggle diff (92 lines)diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scmindex 8fbce15418..5dc600ccb5 100644--- a/gnu/packages/maths.scm+++ b/gnu/packages/maths.scm@@ -38,6 +38,7 @@ ;;; Copyright © 2020 R Veera Kumar <vkor@vkten.in> ;;; Copyright © 2020 Vincent Legoll <vincent.legoll@gmail.com> ;;; Copyright © 2020 Nicolò Balzarotti <nicolo@nixo.xyz>+;;; Copyright © 2020 B. Wilson <elaexuotee@wilsonb.com> ;;; ;;; This file is part of GNU Guix. ;;;@@ -5615,3 +5616,77 @@ and conversions, physical constants, symbolic calculations (including integrals and equations), arbitrary precision, uncertainity propagation, interval arithmetic, plotting.") (license license:gpl2+)))++(define-public metamath+ (package+ (name "metamath")+ (version "0.182")+ (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"))))+ (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"))+ (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"))+ (arguments+ `(#:phases+ (let ((book-builddir "metamath-book-second_edition"))+ (modify-phases %standard-phases+ (add-after 'unpack 'unpack-doc+ (lambda* (#:key inputs #:allow-other-keys)+ (let ((book-tar (assoc-ref inputs "book")))+ (invoke "tar" "xzf" book-tar))))+ (add-after 'build 'build-doc+ (lambda _+ (with-directory-excursion book-builddir+ (invoke "touch" "metamath.ind")+ (invoke "pdflatex" "metamath")+ (invoke "pdflatex" "metamath")+ (invoke "bibtex" "metamath")+ (invoke "makeindex" "metamath")+ (invoke "pdflatex" "metamath")+ (invoke "pdflatex" "metamath"))))+ (add-after 'build-doc 'install-doc+ (lambda* (#:key outputs #:allow-other-keys)+ (let* ((pkg (strip-store-file-name (assoc-ref outputs "out")))+ (out-doc (assoc-ref outputs "doc")))+ (install-file (string-append book-builddir "/metamath.pdf")+ (string-append out-doc "/share/doc/" pkg))+ #t)))))))+ (home-page "http://us.metamath.org/")+ (synopsis "Proof verifier based on a minimalistic formalism")+ (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+Arithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc. See the+Metamath book")+ (license license:gpl2+)))-- 2.26.2
Attachment: signature.asc
E
E
elaexuotee wrote on 13 May 09:25 +0200
gnu: Add metamath.
(address . 40815@debbugs.gnu.org)
3A31ISRYFT791.2TFZ4E8NIDG43@wilsonb.com
Just discovered the (git-file-name ...) function. This is a simple update tothe metamath patch to use this instead of manually using string-append.
From 0e9facf67f5af44bb8e605631a0be6c90ce23000 Mon Sep 17 00:00:00 2001From: "B. Wilson" <elaexuotee@wilsonb.com>Date: Mon, 11 May 2020 20:10:48 +0900Subject: [PATCH] gnu: Add metamath.To: guix-patches@gnu.org
* gnu/packages/maths.scm (metamath): New variable.--- gnu/packages/maths.scm | 75 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+)
Toggle diff (92 lines)diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scmindex d60c033dbc..5a7230cb53 100644--- a/gnu/packages/maths.scm+++ b/gnu/packages/maths.scm@@ -38,6 +38,7 @@ ;;; Copyright © 2020 R Veera Kumar <vkor@vkten.in> ;;; Copyright © 2020 Vincent Legoll <vincent.legoll@gmail.com> ;;; Copyright © 2020 Nicolò Balzarotti <nicolo@nixo.xyz>+;;; Copyright © 2020 B. Wilson <elaexuotee@wilsonb.com> ;;; ;;; This file is part of GNU Guix. ;;;@@ -5635,3 +5636,77 @@ and conversions, physical constants, symbolic calculations (including integrals and equations), arbitrary precision, uncertainity propagation, interval arithmetic, plotting.") (license license:gpl2+)))++(define-public metamath+ (package+ (name "metamath")+ (version "0.182")+ (source+ (origin+ (method git-fetch)+ (uri (git-reference+ (url "https://github.com/metamath/metamath-exe.git")+ (commit "5df616efe4119ff88daf77e7041d45b6fa39c578")))+ (sha256+ (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"))+ (file-name (git-file-name name version))))+ (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"))+ (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"))+ (arguments+ `(#:phases+ (let ((book-builddir "metamath-book-second_edition"))+ (modify-phases %standard-phases+ (add-after 'unpack 'unpack-doc+ (lambda* (#:key inputs #:allow-other-keys)+ (let ((book-tar (assoc-ref inputs "book")))+ (invoke "tar" "xzf" book-tar))))+ (add-after 'build 'build-doc+ (lambda _+ (with-directory-excursion book-builddir+ (invoke "touch" "metamath.ind")+ (invoke "pdflatex" "metamath")+ (invoke "pdflatex" "metamath")+ (invoke "bibtex" "metamath")+ (invoke "makeindex" "metamath")+ (invoke "pdflatex" "metamath")+ (invoke "pdflatex" "metamath"))))+ (add-after 'build-doc 'install-doc+ (lambda* (#:key outputs #:allow-other-keys)+ (let* ((pkg (strip-store-file-name (assoc-ref outputs "out")))+ (out-doc (assoc-ref outputs "doc")))+ (install-file (string-append book-builddir "/metamath.pdf")+ (string-append out-doc "/share/doc/" pkg))+ #t)))))))+ (home-page "http://us.metamath.org/")+ (synopsis "Proof verifier based on a minimalistic formalism")+ (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+Arithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc. See the+Metamath book")+ (license license:gpl2+)))-- 2.26.2
Attachment: signature.asc
N
N
Nicolas Goaziou wrote on 4 Jun 19:49 +0200
Re: [bug#40815] gnu: Add metamath
(name . B. Wilson via Guix-patches via)(address . guix-patches@gnu.org)
87d06eraaf.fsf@nicolasgoaziou.fr
Hello,
"B. Wilson via Guix-patches" via <guix-patches@gnu.org> writes:
Toggle quote (5 lines)> 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 particularlyabout the issue you're encountering there, but I can give some advice onthis package definition.
Toggle quote (5 lines)> +(define-public metamath> + (package> + (name "metamath")> + (version "0.182")
I suggest to let-bind the commit hash around the package definition, adda revision number, and a comment explaining why you're not using plainv0.182 tag.
Toggle quote (10 lines)> + (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.
Toggle quote (8 lines)> + (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.
Toggle quote (18 lines)> + (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.
Toggle quote (8 lines)> + (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 confusesit. It should be either "e.g.,", or "e.g.@:".
Toggle quote (3 lines)> +Arithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc. See the> +Metamath book")
Missing final full stop.
Toggle quote (2 lines)> + (license license:gpl2+)))
I think there are other licenses involved. Could you try to list them,too?
Regards,
-- Nicolas Goaziou
E
E
elaexuotee wrote on 23 Jun 13:32 +0200
(name . Nicolas Goaziou)(address . mail@nicolasgoaziou.fr)
23UB7VNWCB6BC.23I1T2MHNG4ZI@wilsonb.com
Hello Nicolas,
Thank you for taking a look at this!
Toggle quote (4 lines)> 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 ofwaiting for texlive-amsfonts to get fixed, I propose nuking the "doc" outputfor 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.
Toggle quote (4 lines)> 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.
Toggle quote (10 lines)> > + (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 yousuggested. Since this is a non-cosmetic change, I also test built it beforecommenting out all the "doc" output stuff.
Toggle quote (2 lines)> 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 tothis being my first package attempt.
Toggle quote (8 lines)> 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.
Toggle quote (3 lines)> 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 metamathexecutable itself is just GLP2+, but if I'm missing something please let meknow.

Hopefully, in the near future I will find time to dig into the texlive-amsfontsissue, but for now, does this look good?
If we end up pushing just the metamath patch, the other texlive package patchesobviously aren't needed for now, but would it be worth pushing these? Should Isubmit separate issues for them?
Cheers,
From f7e7a323df50fc5c6d4aefb30f67991c367dfabc Mon Sep 17 00:00:00 2001From: "B. Wilson" <elaexuotee@wilsonb.com>Date: Mon, 11 May 2020 20:10:48 +0900Subject: [PATCH] gnu: Add metamath.To: guix-patches@gnu.org
* gnu/packages/maths.scm (metamath): New variable.--- gnu/packages/maths.scm | 75 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+)
Toggle diff (92 lines)diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scmindex 45d699e39c..82b98d8f7d 100644--- a/gnu/packages/maths.scm+++ b/gnu/packages/maths.scm@@ -38,6 +38,7 @@ ;;; Copyright © 2020 R Veera Kumar <vkor@vkten.in> ;;; Copyright © 2020 Vincent Legoll <vincent.legoll@gmail.com> ;;; Copyright © 2020 Nicolò Balzarotti <nicolo@nixo.xyz>+;;; Copyright © 2020 B. Wilson <elaexuotee@wilsonb.com> ;;; ;;; This file is part of GNU Guix. ;;;@@ -5686,3 +5687,77 @@ and conversions, physical constants, symbolic calculations (including integrals and equations), arbitrary precision, uncertainity propagation, interval arithmetic, plotting.") (license license:gpl2+)))++(define-public metamath+ (package+ (name "metamath")+ (version "0.182")+ (source+ (origin+ (method git-fetch)+ (uri (git-reference+ (url "https://github.com/metamath/metamath-exe.git")+ (commit "5df616efe4119ff88daf77e7041d45b6fa39c578")))+ (sha256+ (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"))+ (file-name (git-file-name name version))))+ (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"))+ (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"))+ (arguments+ `(#:phases+ (let ((book-builddir "metamath-book-second_edition"))+ (modify-phases %standard-phases+ (add-after 'unpack 'unpack-doc+ (lambda* (#:key inputs #:allow-other-keys)+ (let ((book-tar (assoc-ref inputs "book")))+ (invoke "tar" "xzf" book-tar))))+ (add-after 'build 'build-doc+ (lambda _+ (with-directory-excursion book-builddir+ (invoke "touch" "metamath.ind")+ (invoke "pdflatex" "metamath")+ (invoke "pdflatex" "metamath")+ (invoke "bibtex" "metamath")+ (invoke "makeindex" "metamath")+ (invoke "pdflatex" "metamath")+ (invoke "pdflatex" "metamath"))))+ (add-after 'build-doc 'install-doc+ (lambda* (#:key outputs #:allow-other-keys)+ (let* ((pkg (strip-store-file-name (assoc-ref outputs "out")))+ (out-doc (assoc-ref outputs "doc")))+ (install-file (string-append book-builddir "/metamath.pdf")+ (string-append out-doc "/share/doc/" pkg))+ #t)))))))+ (home-page "http://us.metamath.org/")+ (synopsis "Proof verifier based on a minimalistic formalism")+ (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+Arithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc. See the+Metamath book")+ (license license:gpl2+)))-- 2.27.0
Attachment: signature.asc
E
E
elaexuotee wrote on 24 Jun 03:14 +0200
(name . Nicolas Goaziou)(address . mail@nicolasgoaziou.fr)
31H3GR8EOYWGZ.2EEY2GE3LMLRZ@wilsonb.com
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.
From 74db38db11a7e107119362983e388cfb5ead3431 Mon Sep 17 00:00:00 2001From: "B. Wilson" <elaexuotee@wilsonb.com>Date: Mon, 11 May 2020 20:10:48 +0900Subject: [PATCH] gnu: Add metamath.To: guix-patches@gnu.org
* gnu/packages/maths.scm (metamath): New variable.--- gnu/packages/maths.scm | 97 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 97 insertions(+)
Toggle diff (114 lines)diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scmindex 45d699e39c..e6f4cbe980 100644--- a/gnu/packages/maths.scm+++ b/gnu/packages/maths.scm@@ -38,6 +38,7 @@ ;;; Copyright © 2020 R Veera Kumar <vkor@vkten.in> ;;; Copyright © 2020 Vincent Legoll <vincent.legoll@gmail.com> ;;; Copyright © 2020 Nicolò Balzarotti <nicolo@nixo.xyz>+;;; Copyright © 2020 B. Wilson <elaexuotee@wilsonb.com> ;;; ;;; This file is part of GNU Guix. ;;;@@ -5686,3 +5687,99 @@ and conversions, physical constants, symbolic calculations (including integrals and equations), arbitrary precision, uncertainity propagation, interval arithmetic, plotting.") (license license:gpl2+)))++(define-public metamath+ ;; Upstream pushed a commit on top of v0.182 that fixes a bug in Makefile.am.+ ;; Using this commit lets us avoid directly including the patch here. In the+ ;; next version bump, we should be able to replace this and directly use the+ ;; version tag.+ (let ((commit "5df616efe4119ff88daf77e7041d45b6fa39c578")+ (revision "0")+ (book-name "metamath-book")+ (book-version "second_edition"))+ (package+ (name "metamath")+ (version (git-version "0.182" revision commit))+ (source+ (origin+ (method git-fetch)+ (uri (git-reference+ (url "https://github.com/metamath/metamath-exe.git")+ (commit commit)))+ (sha256+ (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"))+ (file-name (git-file-name name version))))+ ;; FIXME: Unfortunately, there seems to be a problem with+ ;; texlive-amsfonts that prevents us from typsetting the "doc" output+ ;; pdf. Once fixed, this along with the commented out sections below,+ ;; should be enabled.+ ; (outputs '("out" "doc"))+ (build-system gnu-build-system)+ ;; FIXME: Enable for "doc" output. See previous comment.+ ; (inputs+ ; `((,book-name+ ; ,(origin+ ; (method git-fetch)+ ; (uri (git-reference+ ; (url "https://github.com/metamath/metamath-book.git")+ ; (commit book-version)))+ ; (sha256+ ; (base32+ ; "1kk9nfhs0h8qccpxp1qh072bpfis7h05rlnz3qn1z641d9i4ryyq"))+ ; (file-name (git-file-name book-name book-version))))))+ (native-inputs `(("autoconf" ,autoconf)+ ("automake" ,automake)+ ;; FIXME: Required inputs to build the "doc" output.+ ;; See above comment.+ ; ("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)))+ ))+ ;; FIXME: Arguments to build the "doc" output. See above comment.+ ; (arguments+ ; `(#:phases+ ; (let ((book-builddir "metamath-book-second_edition"))+ ; (modify-phases %standard-phases+ ; (add-after 'unpack 'unpack-doc+ ; (lambda* (#:key inputs #:allow-other-keys)+ ; (let ((book (assoc-ref inputs ,book-name)))+ ; (mkdir-p book-builddir)+ ; (copy-recursively book book-builddir))))+ ; (add-after 'build 'build-doc+ ; (lambda _+ ; (with-directory-excursion book-builddir+ ; (invoke "touch" "metamath.ind")+ ; (invoke "pdflatex" "metamath")+ ; (invoke "pdflatex" "metamath")+ ; (invoke "bibtex" "metamath")+ ; (invoke "makeindex" "metamath")+ ; (invoke "pdflatex" "metamath")+ ; (invoke "pdflatex" "metamath"))))+ ; (add-after 'build-doc 'install-doc+ ; (lambda* (#:key outputs #:allow-other-keys)+ ; (let* ((pkg (strip-store-file-name (assoc-ref outputs "out")))+ ; (out-doc (assoc-ref outputs "doc")))+ ; (install-file (string-append book-builddir "/metamath.pdf")+ ; (string-append out-doc "/share/doc/" pkg))+ ; #t)))))))+ (home-page "http://us.metamath.org/")+ (synopsis "Proof verifier based on a minimalistic formalism")+ (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 Arithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc. See the+Metamath book.")+ ;; FIXME: The "doc" output requires license:cc0. See above comment.+ ; (license '(,license:gpl2+ ,license:cc0)))))+ (license license:gpl2+))))-- 2.27.0
Attachment: signature.asc
N
N
Nicolas Goaziou wrote on 26 Jun 09:19 +0200
(address . elaexuotee@wilsonb.com)
878sgas38j.fsf@nicolasgoaziou.fr
Hello,
laexuotee@wilsonb.com writes:
Toggle quote (4 lines)> 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-amsfontsis fixed. Meanwhile, I think we can remove the comments in this one andapply it.
WDYT?
Toggle quote (2 lines)> Were you referring to CC0 for the metamath book?
Probably, yes.
Toggle quote (4 lines)> 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 tosubmit them as separate issues. If still no one comments of them, I'llapply them later.
Regards,-- Nicolas Goaziou
E
E
elaexuotee wrote on 26 Jun 10:46 +0200
(name . Nicolas Goaziou)(address . mail@nicolasgoaziou.fr)
2Z19F0HU7SZNL.33AMEA6BFHCFT@wilsonb.com
Toggle quote (3 lines)> 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.
Toggle quote (4 lines)> 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 thanmine. 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 ofcreating 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.
Toggle quote (4 lines)> 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!
From 4d94ad11b0e998a9510708e088a4c5eb63919b3b Mon Sep 17 00:00:00 2001From: "B. Wilson" <elaexuotee@wilsonb.com>Date: Mon, 11 May 2020 20:10:48 +0900Subject: [PATCH] gnu: Add metamath.To: guix-patches@gnu.org
* gnu/packages/maths.scm (metamath): New variable.--- gnu/packages/maths.scm | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+)
Toggle diff (54 lines)diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scmindex 45d699e39c..02109ced2d 100644--- a/gnu/packages/maths.scm+++ b/gnu/packages/maths.scm@@ -38,6 +38,7 @@ ;;; Copyright © 2020 R Veera Kumar <vkor@vkten.in> ;;; Copyright © 2020 Vincent Legoll <vincent.legoll@gmail.com> ;;; Copyright © 2020 Nicolò Balzarotti <nicolo@nixo.xyz>+;;; Copyright © 2020 B. Wilson <elaexuotee@wilsonb.com> ;;; ;;; This file is part of GNU Guix. ;;;@@ -5686,3 +5687,39 @@ and conversions, physical constants, symbolic calculations (including integrals and equations), arbitrary precision, uncertainity propagation, interval arithmetic, plotting.") (license license:gpl2+)))++(define-public metamath+ ;; Upstream pushed a commit on top of v0.182 that fixes a bug in Makefile.am.+ ;; Using this commit lets us avoid directly including the patch here. In the+ ;; next version bump, we should be able to replace this and directly use the+ ;; version tag.+ (let ((commit "5df616efe4119ff88daf77e7041d45b6fa39c578")+ (revision "0")+ (book-name "metamath-book")+ (book-version "second_edition"))+ (package+ (name "metamath")+ (version (git-version "0.182" revision commit))+ (source+ (origin+ (method git-fetch)+ (uri (git-reference+ (url "https://github.com/metamath/metamath-exe.git")+ (commit commit)))+ (sha256+ (base32 "0amjdgy42c7jypf6sz98iczlxcyl9bqx67ws1q8w2zdqk2izsyjp"))+ (file-name (git-file-name name version))))+ (build-system gnu-build-system)+ (native-inputs `(("autoconf" ,autoconf)+ ("automake" ,automake)))+ (home-page "http://us.metamath.org/")+ (synopsis "Proof verifier based on a minimalistic formalism")+ (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 Arithmetic, the Cauchy-Schwarz Inequality, Striling's Formula, etc. See the+Metamath book.")+ (license license:gpl2+))))-- 2.27.0
Attachment: signature.asc
N
N
Nicolas Goaziou wrote on 28 Jun 22:12 +0200
(address . elaexuotee@wilsonb.com)
87k0zrvtk6.fsf@nicolasgoaziou.fr
Hello,
elaexuotee@wilsonb.com writes:
Toggle quote (7 lines)>> 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 advanceddocumentation, not like a regular manual. I didn't read it, so it isjust a guess.
Anyway, I only suggested it as another option to consider. Feel free toignore it.
Toggle quote (8 lines)> 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 twosemicolons, not a single one.
WDYT?
Regards,-- Nicolas Goaziou
E
E
elaexuotee wrote on 29 Jun 09:09 +0200
(name . Nicolas Goaziou)(address . mail@nicolasgoaziou.fr)
3DWRMY6FLHG65.2WHMN0WRGUE63@wilsonb.com
Hell,
Thanks for the quick turnaround.
Toggle quote (4 lines)> 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 strangefor what looks like a cli program. In this case, it just happens that this isthe only reasonable documentation, aparth from the website, for using andunderstanding Metamath proofs.
Toggle quote (5 lines)> 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 myprevious email that excises the commented out code. Does it look reasonable?
Cheers.
Attachment: signature.asc
N
N
Nicolas Goaziou wrote on 1 Jul 13:02 +0200
(address . elaexuotee@wilsonb.com)
87a70jfqgi.fsf@nicolasgoaziou.fr
Hello,
elaexuotee@wilsonb.com writes:
Toggle quote (4 lines)> 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, sincethey were not used in the current package definition, tweaked a bit thedescription, and applied your patch.
I hope we can have the book either as a doc output, or as a separatepackage, bundled at some point. Meanwhile, I'm closing this bug report.
Regards,-- Nicolas Goaziou
Closed
E
E
elaexuotee wrote on 2 Jul 01:53 +0200
(name . Nicolas Goaziou)(address . mail@nicolasgoaziou.fr)
208YMDGHVVTI7.1Z7R2582RUM50@wilsonb.com
Excellent. Thanks for cleaning up the things I missed and pushing.
Nicolas Goaziou <mail@nicolasgoaziou.fr> wrote:
Toggle quote (16 lines)> Hello,> > elaexuotee@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,
Attachment: signature.asc
Closed
?