I run mmj2 using the
https://github.com/digama0/mmj2/blob/master/mmj2jar/mmj2 script. It
takes care of asking for enough memory, but from looking at the script
it seems like the relevant option is
-Xmx1280M
You'll probably also want a plain text editor capable of editing a file
that big - two that have worked for me are vim and geany but I assume
there are others.
On 1/15/25 20:14, Noam Pasman wrote:
Hi,
I've been having a few issues with setting everything up. I was able
to fork, clone, and branch the repository, but I don't know how to
actually open up the set.mm <http://set.mm> file and add a
mathbox there. I downloaded mmj2 in the hope of opening set.mm
<http://set.mm> from there, but when I followed the QuickStart
instructions I got the following error:
Processing RunParmFile Command #1 = LoadFile,set.mm <http://set.mm>
Java heap space
java.lang.OutOfMemoryError: Java heap space
Am I doing this in the wrong way? Or do I just need to find a way to
allocate more memory to mmj2?
Thanks,
Noam
On Mon, Jan 13, 2025 at 10:43 PM Noam Pasman <[email protected]>
wrote:
Thank you all! It's great to meet you.
I'll probably start setting up the github process over the next
few days, so thank you for the instructions, Glauco! I'll reply to
this thread if there's something I don't understand.
Thanks for the recommendation, Jim! It might be a bit
incomprehensible to me for now but I'll look back on it after I
have a bit more experience. I've been thinking about learning some
type theory (and category theory, for that matter), so I wouldn't
mind diving into that book and hoping I can make sense of it. I
also didn't know about the issues page - I'll probably start with
reproving some existing theorems but at some point I'll definitely
look through the list of issues and see if there's something doable.
I might take a while to familiarize myself enough with working in
Metamath to actually be able to do anything, but once I feel
comfortable with the tools I'd love to help you, Scott. The
Gonshor book looks super interesting in any case, so I'll probably
read it after Knuth.
- Noam
On Mon, Jan 13, 2025 at 3:27 PM Scott Fenton <[email protected]> wrote:
Hi Noam,
Great to see you! We always welcome new contributors. If you
want to get into surreal work, I'm mostly working off On
Numbers and Games by Conway and An Introduction to the Theory
of Surreal Numbers by Gonshor. The next step there is actually
a mix of set theory and arithmetic. There is a second type of
addition defined on ordinal numbers called "natural addition".
It gives the same results over the natural numbers but it
differs at _om and above. The next couple of proofs in the
surreal numbers depend on induction on the natural sum of the
birthdays of various surreals. I'd appreciate any help I could
get there.
-Scott
On Sun, Jan 12, 2025 at 10:47 AM Noam Pasman
<[email protected]> wrote:
Happy New Year!
I'm an undergraduate right now, and I spent much of last
year reading through most of Parts 1 through 4 of the
Metamath Theorem List. I'm hoping to do some more set
theory in the future, but there aren't any mathematical
set theorists at my college so I don't really know where
to continue from what's in Metamath. I'm planning to read
some of the set theory books referenced in the Theorem
List, particularly either Takeuti and Zaring's
/Introduction to Axiomatic Set Theory/ or Suppes's
/Axiomatic Set Theory/, but I would appreciate some advice
on which of these (and/or some other book(s)) is most
helpful. I'm also currently in the process of applying to
REUs, and I haven't found any for set theory but if there
are some I'm not aware of (or generally any way to do set
theory as an undergraduate) I'd love to hear about them.
I'm also hoping to contribute to set.mm <http://set.mm>,
and I read the two github pages on contributing but I
wanted to ask about who I should contact in case I have a
problem with setting everything up. Eventually, I'd love
to help with some project in the database if needed and if
I already somewhat understand the concepts. I've been
reading Knuth's /Surreal Numbers/ and I saw that work has
begun on moving theorems on surreal numbers from
Mathboxes to main, so I'd love to give any help I can
towards developing that further (obviously after reading
much more material on the subject). If there's another
project that I'd be more useful for, that's good too!
- Noam Pasman
--
You received this message because you are subscribed to
the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails
from it, send an email to
[email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/CABJcXbRF5BsRyNC_hf3L_EmhmuSvfdaN3EKy%2BFOs10DLRUjPOg%40mail.gmail.com
<https://groups.google.com/d/msgid/metamath/CABJcXbRF5BsRyNC_hf3L_EmhmuSvfdaN3EKy%2BFOs10DLRUjPOg%40mail.gmail.com?utm_medium=email&utm_source=footer>.
--
You received this message because you are subscribed to the
Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from
it, send an email to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/CACKrHR-d%3DC7UHPvZZq0wYru0nzUF0PiZsZ-u8WbDrv0xCAmVFg%40mail.gmail.com
<https://groups.google.com/d/msgid/metamath/CACKrHR-d%3DC7UHPvZZq0wYru0nzUF0PiZsZ-u8WbDrv0xCAmVFg%40mail.gmail.com?utm_medium=email&utm_source=footer>.
--
You received this message because you are subscribed to the Google
Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send
an email to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/CABJcXbSvK8FjiiHqg1RP8NL4tbLkqAhiVZtP291cd7xGSJZ2ww%40mail.gmail.com
<https://groups.google.com/d/msgid/metamath/CABJcXbSvK8FjiiHqg1RP8NL4tbLkqAhiVZtP291cd7xGSJZ2ww%40mail.gmail.com?utm_medium=email&utm_source=footer>.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/5606860a-2156-4262-bad8-410559207ebe%40panix.com.
