Errors with set.mm because of setvar?

[avekens]

(copied from metamath/set.mm#966)
I installed the plugin as described in http://emetamath.tirix.org/, but loading the current set.mm produces errors:

It seems that the recent change of "set" to "setvar" (see issue #759 in https://github.com/metamath/set.mm) causes problems.

[tirix]

Hi Alexander,

Sorry I did not answer earlier!
Yes, I had to adapt to the change from "set" to "setvar" to follow with the change in set.mm.
The setting is in your project properties under Metamath properties:

[glacode]

Configuring the "Other Types" as in the picture, fixed the errors.

But when I ctrl+u it , it seems that Eclipse crashes (after a while). I'm trying under Ubuntu.

I've already added

-Xms256m
-Xmx2048m

to eclipse.ini

[glacode]

Linux warned me that the crash was due to a request for memory, larger than what my VM can provide.

It's a 4 GB virtual machine, where mmj2 runs really fast.

@tirix If I had to take a wild guess, the Proof Explorer could be the part that slows down the start-up process and runs my machine out of memory: is there an option to try Emetamath, without the Proof Explorer part?

Thanks in advance
Glauco

[tirix]

Hi Glauco,

Thanks for your interest in the plugin!
I've checked again just now and confirm that I'm running with these options in eclipse.ini:

-Xms256m
-Xmx2048m

However I'm surprised to see Eclipse seems to use 2.35 GB.
So if it fails for you with 2 GB, can you maybe try to increase them? If your MMJ2 works with 4 GB, you could try

-Xms256m
-Xmx4096m

You might even try bigger numbers, to find out what is the limit!

The Proof Explorer works with lazy object creation and will only create the entries if you open them in the view. Commenting it out might not be so easy...