Problem launching mmj2

[Benoit]

Hi,

I'm having trouble launching mmj2 on Debian Bullseye.  It does not recognize the option "-Xincgc".  Should I replace it with something else, or is it safe to remove it ?  I remember that for some time there was a deprecation warning: maybe this is now deprecated ?

Thanks in advance.

Details:

benoit@ordi:~$ java -Xincgc -Xms128M -Xmx512M -jar /home/benoit/Documents/_metamath/mmj2/mmj2jar/mmj2.jar RunParms.txt Y "" /home/benoit/Documents/_metamath/mm181 ""
Unrecognized option: -Xincgc
Error: Could not create the Java Virtual Machine.
Error: A fatal exception has occurred. Program will exit.
benoit@ordi:~$ java -version
openjdk version "11.0.6" 2020-01-14
OpenJDK Runtime Environment (build 11.0.6+10-post-Debian-2)
OpenJDK 64-Bit Server VM (build 11.0.6+10-post-Debian-2, mixed mode)

[Stanislas Polu]

I had the same issue and this is what I use with JRE 1.8.0 (latest didn't work)

java -Xms1G -Xmx1G -jar ~/opt/metamath/mmj2/mmj2jar/mmj2.jar
"RunParms.txt" Y "/Users/spolu/opt/metamath/mmj2/mmj2jar/"
"/Users/spolu/opt/metamath/set.mm" ""

Hope it helps.

-stan

> --
> 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 metamath+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2db7f38e-8282-419e-9557-111b3e48d735%40googlegroups.com.

[Benoit]

Thanks Stan.  So you remove "-Xincgc" (incremental garbage colllector) altogether ?  I guess it then uses a default garbage collector ?  I also saw proposals to use -XX:+UseG1GC ("garbage first" garbage collector), while -XX:+UseConcMarkSweepGC also triggers a deprecation warning.  But I do not know how they compare and what is best for performance and stability.

Then, I have another deprecation warning:

  Warning: Nashorn engine is planned to be removed from a future JDK release

Then, running mmj2, hitting Ctrl-U or Ctrl-R often makes proofs disappear, so unfortunately mmj2 is unusable for me.

Terminal output when I click File > New Proof, enter an existing label, and get an empty statement, i.e.

  $( <MM> <PROOF_ASST> THEOREM=
 
  $)

Ignoring exception:
java.lang.ClassCastException: class javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper cannot be cast to class javax.swing.text.AbstractDocument$DefaultDocumentEvent (javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper and javax.swing.text.AbstractDocument$DefaultDocumentEvent are in module java.desktop of loader 'bootstrap')
    at mmj.pa.CompoundUndoManager.undoableEditHappened(CompoundUndoManager.java:110)
    at java.desktop/javax.swing.text.AbstractDocument.fireUndoableEditUpdate(AbstractDocument.java:293)
    at java.desktop/javax.swing.text.DefaultStyledDocument.setCharacterAttributes(DefaultStyledDocument.java:530)
    at mmj.pa.ColorThread.processEvent(ColorThread.java:266)
    at mmj.pa.ColorThread.run(ColorThread.java:170)
Ignoring exception:
java.lang.ClassCastException: class javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper cannot be cast to class javax.swing.text.AbstractDocument$DefaultDocumentEvent (javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper and javax.swing.text.AbstractDocument$DefaultDocumentEvent are in module java.desktop of loader 'bootstrap')
    at mmj.pa.CompoundUndoManager.undoableEditHappened(CompoundUndoManager.java:110)
    at java.desktop/javax.swing.text.AbstractDocument.fireUndoableEditUpdate(AbstractDocument.java:293)
    at java.desktop/javax.swing.text.DefaultStyledDocument.setCharacterAttributes(DefaultStyledDocument.java:530)
    at mmj.pa.ColorThread.processEvent(ColorThread.java:266)
    at mmj.pa.ColorThread.run(ColorThread.java:170)
Ignoring exception:
java.lang.ClassCastException: class javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper cannot be cast to class javax.swing.text.AbstractDocument$DefaultDocumentEvent (javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper and javax.swing.text.AbstractDocument$DefaultDocumentEvent are in module java.desktop of loader 'bootstrap')
    at mmj.pa.CompoundUndoManager.undoableEditHappened(CompoundUndoManager.java:110)
    at java.desktop/javax.swing.text.AbstractDocument.fireUndoableEditUpdate(AbstractDocument.java:293)
    at java.desktop/javax.swing.text.DefaultStyledDocument.setCharacterAttributes(DefaultStyledDocument.java:530)
    at mmj.pa.ColorThread.processEvent(ColorThread.java:266)
    at mmj.pa.ColorThread.run(ColorThread.java:170)
Ignoring exception:
java.lang.ClassCastException: class javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper cannot be cast to class javax.swing.text.AbstractDocument$DefaultDocumentEvent (javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper and javax.swing.text.AbstractDocument$DefaultDocumentEvent are in module java.desktop of loader 'bootstrap')
    at mmj.pa.CompoundUndoManager.undoableEditHappened(CompoundUndoManager.java:110)
    at java.desktop/javax.swing.text.AbstractDocument.fireUndoableEditUpdate(AbstractDocument.java:293)
    at java.desktop/javax.swing.text.DefaultStyledDocument.setCharacterAttributes(DefaultStyledDocument.java:530)
    at mmj.pa.ColorThread.processEvent(ColorThread.java:266)
    at mmj.pa.ColorThread.run(ColorThread.java:170)
Ignoring exception:
java.lang.ClassCastException: class javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper cannot be cast to class javax.swing.text.AbstractDocument$DefaultDocumentEvent (javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper and javax.swing.text.AbstractDocument$DefaultDocumentEvent are in module java.desktop of loader 'bootstrap')
    at mmj.pa.CompoundUndoManager.undoableEditHappened(CompoundUndoManager.java:110)
    at java.desktop/javax.swing.text.AbstractDocument.fireUndoableEditUpdate(AbstractDocument.java:293)
    at java.desktop/javax.swing.text.DefaultStyledDocument.setCharacterAttributes(DefaultStyledDocument.java:530)
    at mmj.pa.ColorThread.processEvent(ColorThread.java:266)
    at mmj.pa.ColorThread.run(ColorThread.java:170)
Exception in thread "AWT-EventQueue-0" java.lang.ClassCastException: class javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper cannot be cast to class javax.swing.text.AbstractDocument$DefaultDocumentEvent (javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper and javax.swing.text.AbstractDocument$DefaultDocumentEvent are in module java.desktop of loader 'bootstrap')
    at mmj.pa.CompoundUndoManager.undoableEditHappened(CompoundUndoManager.java:110)
    at java.desktop/javax.swing.text.AbstractDocument.fireUndoableEditUpdate(AbstractDocument.java:293)
    at java.desktop/javax.swing.text.AbstractDocument.handleRemove(AbstractDocument.java:632)
    at java.desktop/javax.swing.text.AbstractDocument.remove(AbstractDocument.java:596)
    at mmj.pa.HighlightedDocument.remove(HighlightedDocument.java:101)
    at mmj.pa.HighlightedDocument.setTextProgrammatic(HighlightedDocument.java:178)
    at mmj.pa.ProofAsstGUI.setProofTextAreaText(ProofAsstGUI.java:618)
    at mmj.pa.ProofAsstGUI.displayProofWorksheet(ProofAsstGUI.java:2354)
    at mmj.pa.ProofAsstGUI.access$3(ProofAsstGUI.java:2345)
    at mmj.pa.ProofAsstGUI$WorksheetRequest.receive(ProofAsstGUI.java:2248)
    at mmj.pa.ProofAsstGUI$RequestThreadStuff.lambda$0(ProofAsstGUI.java:2295)
    at java.desktop/java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:313)
    at java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:770)
    at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)
    at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:715)
    at java.base/java.security.AccessController.doPrivileged(Native Method)
    at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)
    at java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:740)
    at java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)
    at java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)
    at java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)
    at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)
    at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)
    at java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)

 

[Stanislas Polu]

Have you tried downgrading your JRE/JDK version ?

Undo is very unstable for me as well but I was able to live without it
so far (I think mmj2 is ripe for a at least a re-build on recent
frameworks)

-stan

> --
> 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 metamath+u...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8f92f815-b70f-479f-9356-ddf0b438fa32%40googlegroups.com.

[Mario Carneiro]

That bug occurs when you try to use mmj2 on newer versions of the JDK. It has been fixed on master, but I don't think there has been a release with the bugfix. (Unfortunately the fix doesn't completely restore the original chunked undo behavior so you have to undo one character at a time now, but it should be usable.)

I don't think there are any relevant features in java that are being exploited in mmj2, so if you aren't using java for anything else it seems reasonable to just stick with java 8 and avoid the upgrade breakage.

Mario

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0wy4tzkLmF%2By-sAzfhogjiTkSJ3ibUu608L0eEtLSzDpA%40mail.gmail.com.

[Benoit]

Thanks, I'm going to try to download master and/or downgrade JDK.

Note that my problem is with Ctrl-U, which is "unify", not "undo", and with Ctrl-R (reformat).

Benoît

[Mario Carneiro]

I don't know anything about a bug in unify/reformat. Sometimes bad unify commands will throw up a console error and manifest in the UI as a unify that doesn't stop and has to be cancelled. If so, please show the error. Otherwise, I don't know what this could be, and I would be interested to hear if it is also triggered in the master version.

Mario

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/17e931b9-e063-4167-abee-dfba744e8f04%40googlegroups.com.

[Benoit]

Thanks for the tip.  Here is a bug report.  Let me know if you need other information.

I installed mmj2-master from https://github.com/digama0/mmj2.  I'm using Debian Bullseye and here is my java version:

  benoit@ordi:~$ java -version
  openjdk version "11.0.6" 2020-01-14
  OpenJDK Runtime Environment (build 11.0.6+10-post-Debian-2)
  OpenJDK 64-Bit Server VM (build 11.0.6+10-post-Debian-2, mixed mode)

I launched mmj2 with:

  benoit@ordi:~$ java -Xms256M -Xmx512M -jar /home/benoit/Documents/_metamath/mmj2/mmj2jar/mmj2.jar /home/benoit/Documents/_metamath/mmj2/mmj2jar/RunParms.txt Y /home/benoit/Documents/_metamath/mmj2/mmj2jar/ /home/benoit/Documents/_metamath/mm181 ""

It works (even though I get the warning "Warning: Nashorn engine is planned to be removed from a future JDK release").  Then I click on File > New Proof and type "a1i", and the moment I type "Enter", mmj2 displays an almost empty window:

  $( <MM> <PROOF_ASST> THEOREM=
 
  $)

and the terminal displays what is copied below.   When I redo this operation (File > New Proof, "a1i", "Enter"), it correctly displays a1i.  Then I type "ax-mp" on the qed line, as usual, and I type Ctrl-U to unify, but it deletes the qed line, displaying "!    |- ( ps -> ph )", and the terminal displays more "Ignoring exception:" messages.

Exception in thread "AWT-EventQueue-0" Ignoring exception:

java.lang.ClassCastException: class javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper cannot be cast to class javax.swing.text.AbstractDocument$DefaultDocumentEvent (javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper and javax.swing.text.AbstractDocument$DefaultDocumentEvent are in module java.desktop of loader 'bootstrap')
    at mmj.pa.CompoundUndoManager.undoableEditHappened(CompoundUndoManager.java:110)
    at java.desktop/javax.swing.text.AbstractDocument.fireUndoableEditUpdate(AbstractDocument.java:293)
    at java.desktop/javax.swing.text.DefaultStyledDocument.setCharacterAttributes(DefaultStyledDocument.java:530)
    at mmj.pa.ColorThread.processEvent(ColorThread.java:266)
    at mmj.pa.ColorThread.run(ColorThread.java:170)

[Benoit]

Unfortunately I cannot downgrade JDK: the earliest JDK release I can get with "apt" is JDK 11.

I tried to reinstall mmj2, but I get:

  ........./mmj2/src$ javac `find . ../lib -name *.java` -d ../classes
  ./mmj/pa/PaConstants.java:121: error: package org.json does not exist

So I downloaded json-20190722.jar but I do not know how to make javac understand that it has to use it...

Would it be possible to include the package org.json in the mmj2 distribution, so that it is integrated ?

Benoît

[Mario Carneiro]

I think it is used as a submodule, meaning that it gets compiled from source together with the rest of mmj2 and bundled into mmj2.jar. It is not an external jar file.

Aren't there .deb downloads for earlier versions of the JDK?

Mario

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/ce397d63-f6ec-4c90-8de1-48a3669c1c61%40googlegroups.com.

[Benoit]

I think it is used as a submodule, meaning that it gets compiled from source together with the rest of mmj2 and bundled into mmj2.jar. It is not an external jar file.

So how do I make javac "understand" that it should use org.json ?  I get the error:

  ./mmj/pa/PaConstants.java:121: error: package org.json does not exist

  import org.json.JSONArray;

                 ^

when I type the command: $ javac `find . ../lib -name *.java` -d ../classes

Aren't there .deb downloads for earlier versions of the JDK?

There probably are.  My skills in this domain are limited, but I will try that.

 

Benoît

[Mario Carneiro]

You have to have the .java files on your computer, inside the org/json directory. "git submodule" should put the files in the right place.

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/27d50942-7058-46d9-bf9a-7350a2b6d960%40googlegroups.com.

[Benoit]

Not sure I did it correctly, but I still get the same error:

benoit@ordi:~/Documents/_metamath/git$ git clone --depth 1 --no-single-branch https://github.com/digama0/mmj2.git
Cloning into 'mmj2'...
remote: Enumerating objects: 5002, done.
remote: Counting objects: 100% (5002/5002), done.
remote: Compressing objects: 100% (2971/2971), done.
remote: Total 5002 (delta 2357), reused 4459 (delta 1948), pack-reused 0
Receiving objects: 100% (5002/5002), 16.03 MiB | 8.07 MiB/s, done.
Resolving deltas: 100% (2357/2357), done.
benoit@ordi:~/Documents/_metamath/git$ cd mmj2
benoit@ordi:~/Documents/_metamath/git/mmj2 (master)$ git submodule
-edfb0c57d5619bc7444364451a6d6201457136e7 lib/JSON-java/org/json
benoit@ordi:~/Documents/_metamath/git/mmj2 (master)$ echo "Manifest-Version: 1.0" >MANIFEST.MF
benoit@ordi:~/Documents/_metamath/git/mmj2 (master)$ echo "Main-Class: mmj.util.BatchMMJ2" >>MANIFEST.MF
benoit@ordi:~/Documents/_metamath/git/mmj2 (master)$ cd src
benoit@ordi:~/Documents/_metamath/git/mmj2/src (master)$ javac `find . ../lib -name *.java` -d ../classes

[Mario Carneiro]

Where did you find those build instructions? I have to admit it's a bit out of my depth, and I haven't touched this in a while. I usually use an ant build, in the build.xml file. You may be able to find the commands you need there.

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/ee1100b6-720b-480a-bbe7-8014bd949c49%40googlegroups.com.

[Benoit]

On Monday, March 23, 2020 at 1:09:25 PM UTC+1, Mario Carneiro wrote:

Where did you find those build instructions? I have to admit it's a bit out of my depth, and I haven't touched this in a while. I usually use an ant build, in the build.xml file. You may be able to find the commands you need there.

I was using mmj2/compile/linux/compilescript.txt

I will try your method, thanks.

[Benoit]

I reverted to JDK 8 using the instructions at https://linuxize.com/post/install-java-on-debian-10/  adapting them since I'm using Debian 11 (Bullseye) and not Debian 10 (Buster).  It now seems that mmj2 works correctly.  The above errors remain mysterious...

Benoît