mmj2 users on Windows processing set.mm: May need to increase memory

31 views
Skip to first unread message

David A. Wheeler

unread,
Apr 18, 2020, 4:02:25 PM4/18/20
to metamath
If you use mmj2 on Windows to process set.mm, you may need to
increase the memory settings of mmj2.

Here are the details - including how to fix it - if this situation applies to you.

The issue is that set.mm has
gotten bigger and that mmj2 includes an Early parser
(which uses nontrivial memory). I don't think splitting set.mm would help
in this case (though I haven't checked that seriously).
Changing a memory setting solves the problem.

In the long term, I've provided a proposed change to mmj2 so it
will automatically be handled by default. Hopefully Mario will merge it and
post a new version of mmj2 (hint!). You can see the pull request here:
https://github.com/digama0/mmj2/pull/34

In the meantime: If you use the mmj2 batch files, such as mmj2.bat,
you may need to edit the batch files to keep working with set.mm.
If you've made your own batch files, this will also apply.
These files provide Java a few parameters so mmj2 will work.
One option is "-Xmx", which sets the maximum (heap) memory size.
It's been 512 Mebibytes (512M), but set.mm has gotten larger and the
Earley parser uses nontrivial amounts of memory. I changed
"-Xmx512M" to "-Xmx2g" (2 Gibibytes), and all worked again.
You don't need to change "-Xms"; that's just the starting value, and as
long as the *maximum* value is large enough you're fine.

--- David A. Wheeler

Alexander van der Vekens

unread,
Apr 19, 2020, 4:26:48 AM4/19/20
to Metamath
I have been using -Xmx1024M for some month, and I never had problems so far...

Alexander
Reply all
Reply to author
Forward
0 new messages