[bug#40815] gnu: Add metamath
diff mbox series

Message ID 2Z19F0HU7SZNL.33AMEA6BFHCFT@wilsonb.com
State New
Headers show
Series
  • [bug#40815] gnu: Add metamath
Related show

Checks

Context Check Description
cbaines/applying patch fail View Laminar job

Commit Message

Joshua Branson via Guix-patches via June 26, 2020, 8:46 a.m. UTC
> 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.

> 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 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?

Either way, the patch I included here strips out the comments.

> 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!

Comments

Nicolas Goaziou June 28, 2020, 8:12 p.m. UTC | #1
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,
Joshua Branson via Guix-patches via June 29, 2020, 7:09 a.m. UTC | #2
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.
Nicolas Goaziou July 1, 2020, 11:02 a.m. UTC | #3
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,
Joshua Branson via Guix-patches via July 1, 2020, 11:53 p.m. UTC | #4
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,

Patch
diff mbox series

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