| Message ID | 2Z19F0HU7SZNL.33AMEA6BFHCFT@wilsonb.com |
|---|---|
| State | Accepted |
| Headers | show |
| Series | [bug#40815] gnu: Add metamath | expand |
| Context | Check | Description |
|---|---|---|
| cbaines/applying patch | fail | View Laminar job |
Hello, elaexuotee@wilsonb.com writes: >> 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 advanced documentation, not like a regular manual. I didn't read it, so it is just a guess. Anyway, I only suggested it as another option to consider. Feel free to ignore it. > 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 two semicolons, not a single one. WDYT? Regards,
Hell, Thanks for the quick turnaround. > 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 strange for what looks like a cli program. In this case, it just happens that this is the only reasonable documentation, aparth from the website, for using and understanding Metamath proofs. > 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 my previous email that excises the commented out code. Does it look reasonable? Cheers.
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,
Excellent. Thanks for cleaning up the things I missed and pushing. Nicolas Goaziou <mail@nicolasgoaziou.fr> wrote: > 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,
From 4d94ad11b0e998a9510708e088a4c5eb63919b3b Mon Sep 17 00:00:00 2001 From: "B. Wilson" <elaexuotee@wilsonb.com> Date: Mon, 11 May 2020 20:10:48 +0900 Subject: [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(+) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 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