Launching mmj2

[Benoit]

Hi,

I am failing to launch mmj2 when I try the following in a terminal (on Debian):

benoit@ordi:~$ java -Xincgc -Xms512M -Xmx1024M -jar /home/mmj2/mmj2jar/mmj2.jar "RunParms.txt" Y "/home/mmj2/mmj2jar/" "/home/metamath/" ""
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.3" 2019-04-16
OpenJDK Runtime Environment (build 11.0.3+1-Debian-1)
OpenJDK 64-Bit Server VM (build 11.0.3+1-Debian-1, mixed mode, sharing)

I understand the error is not due to mmj2, but since the command above is the recommended way to start mmj2, I thought someone here might have an idea.  After some searching, I learnt that the option -Xincgc (that activates the incremental garbage collector) was deprecated.

What launching command should I use ?

Also: I think I remember some modifications were made to mmj2 recently, but the downloadable mmj2.zip from http://us2.metamath.org/#mmj2 is from 26-Jan-2016 and on https://github.com/digama0/mmj2 the last commit is from 11 May 2017.  What is the recommended way to obtain the latest mmj2 ?

Thanks,

Benoît

[Jim Kingdon]

Last time I tried to use java11 (or 10, or whatever I tried), it didn't work and I went back to java8.

[Alexander van der Vekens]

-Xincgc is deprecated in Java 8, and was removed in Java 9, see https://docs.oracle.com/javase/9/migrate/toc.htm#JSMIG-GUID-977E1ED7-02BE-4A13-9B04-A719728E84BF

Removing -Xincgc from the input causes an OutOfMemoryException on starting mmj2. But using -XX:+UseConcMarkSweepGC instead of -Xincgc works. However, this GC is deprecated with Java 9 ...

Somebody should find out which GC (garbage collector) is suited best for mmj2 (and future-proof).

[Alexander van der Vekens]

Maybe -XX:+UseG1GC could be a good choice. However, running mmj2 with Java 12 I get:

Exception in thread "main" java.lang.StringIndexOutOfBoundsException: begin 2, end 3, length 2
        at java.base/java.lang.String.checkBoundsBeginEnd(String.java:3410)
        at java.base/java.lang.String.substring(String.java:1883)
        at mmj.util.BatchMMJ2.checkVersion(BatchMMJ2.java:130)
        at mmj.util.BatchMMJ2.<init>(BatchMMJ2.java:40)
        at mmj.util.BatchMMJ2.main(BatchMMJ2.java:51)

So I think there are more issues with higher Java versions.

[Alexander van der Vekens]

Issues with Java 11 were already reported in https://groups.google.com/d/topic/metamath/3kN15fc2MdY/discussion, but I could not find out if there was already a solution.

[David A. Wheeler]

Java versions after 8 from Oracle have a significantly changed license. It might be very wise to ensure that the code continues to run on 8.

--- David A.Wheeler

[Benoit]

The error Alexander reports is due to the second line in

final int maj = Integer.parseInt(javaVersion.substring(0, 1));
final int min = Integer.parseInt(javaVersion.substring(2, 3));

Maybe this is simply due to the fact that the major version now has two digits? I tried to recompile mmj2 with the trivial modifications

(0, 1) --> (2, 3)

(0, 2) --> (3, 4)

by typing

javac -cp org.json-20161124.jar `find -name *.java` -d ../classes

(I had to add the org.json-20161124.jar to the classpath since javac complained the package did not exist). This gives me 33 errors, mostly in /mmj/pa/Serializer.java.

It would be a shame to have to downgrade from java 11 to java 8 to make it work.

Benoît

[David Starner]

On Wed, Mar 27, 2019 at 6:03 PM Benoit <benoit...@gmail.com> wrote:
>
> The error Alexander reports is due to the second line in
>
> final int maj = Integer.parseInt(javaVersion.substring(0, 1));
> final int min = Integer.parseInt(javaVersion.substring(2, 3));
>
> Maybe this is simply due to the fact that the major version now has two digits? I tried to recompile mmj2 with the trivial modifications
> (0, 1) --> (2, 3)
> (0, 2) --> (3, 4)
> by typing

javaVersion in Java 12 is just "12", no minor version included. I
wrote a patch for it, but I couldn't get the whole thing to compile.

> javac -cp org.json-20161124.jar `find -name *.java` -d ../classes
>
> (I had to add the org.json-20161124.jar to the classpath since javac complained the package did not exist). This gives me 33 errors, mostly in /mmj/pa/Serializer.java.
>
> It would be a shame to have to downgrade from java 11 to java 8 to make it work.

--
Kie ekzistas vivo, ekzistas espero.

[Alexander van der Vekens]

I enhanced checkVersion by the following (as hotfix)

    public static void checkVersion() throws IllegalArgumentException {
        final String javaVersion = System
            .getProperty(UtilConstants.JAVA_VERSION_PROPERTY_NAME);

        if (javaVersion.length() ==2)
            return;

       ....

With that, I could run mmj2 (with Java 12), but it crashes with the following error:

Warning: Nashorn engine is planned to be removed from a future JDK release
I-PA-0412 Excluded these assertions from Unification search list as requested on input RunParm: [dummylink]
I-UT-0015 **** Processing RunParmFile Command #11 = SetMMDefinitionsCheckWithExclusions,ax-*,df-bi,df-clab,df-cleq,df-clel,df-sbc
mmj/lang/LogicalSystem (wrong name: mmj/lang/logicalSystem)
java.lang.NoClassDefFoundError: mmj/lang/LogicalSystem (wrong name: mmj/lang/logicalSystem)
    at java.base/java.lang.ClassLoader.defineClass1(Native Method)
    at java.base/java.lang.ClassLoader.defineClass(ClassLoader.java:1016)
    at java.base/java.security.SecureClassLoader.defineClass(SecureClassLoader.java:151)
    at java.base/jdk.internal.loader.BuiltinClassLoader.defineClass(BuiltinClassLoader.java:802)
    at java.base/jdk.internal.loader.BuiltinClassLoader.findClassOnClassPathOrNull(BuiltinClassLoader.java:700)
    at java.base/jdk.internal.loader.BuiltinClassLoader.loadClassOrNull(BuiltinClassLoader.java:623)
    at java.base/jdk.internal.loader.BuiltinClassLoader.loadClass(BuiltinClassLoader.java:581)
    at java.base/jdk.internal.loader.ClassLoaders$AppClassLoader.loadClass(ClassLoaders.java:178)
    at java.base/java.lang.ClassLoader.loadClass(ClassLoader.java:521)
    at java.base/java.lang.Class.forName0(Native Method)
    at java.base/java.lang.Class.forName(Class.java:415)
    at jdk.scripting.nashorn/jdk.nashorn.internal.runtime.Context.findClass(Context.java:1180)
    at jdk.scripting.nashorn/jdk.nashorn.internal.objects.NativeJavaImporter.createProperty(NativeJavaImporter.java:119)
    at jdk.scripting.nashorn/jdk.nashorn.internal.objects.NativeJavaImporter.findProperty(NativeJavaImporter.java:94)
    at jdk.scripting.nashorn/jdk.nashorn.internal.runtime.ScriptObject.findProperty(ScriptObject.java:787)
    at jdk.scripting.nashorn/jdk.nashorn.internal.runtime.WithObject.lookup(WithObject.java:106)
    at jdk.scripting.nashorn/jdk.nashorn.internal.runtime.linker.NashornLinker.getGuardedInvocation(NashornLinker.java:104)
    at jdk.scripting.nashorn/jdk.nashorn.internal.runtime.linker.NashornLinker.getGuardedInvocation(NashornLinker.java:96)
    at jdk.dynalink/jdk.dynalink.linker.support.CompositeTypeBasedGuardingDynamicLinker.getGuardedInvocation(CompositeTypeBasedGuardingDynamicLinker.java:161)
    at jdk.dynalink/jdk.dynalink.linker.support.CompositeGuardingDynamicLinker.getGuardedInvocation(CompositeGuardingDynamicLinker.java:109)
    at jdk.dynalink/jdk.dynalink.LinkerServicesImpl.lambda$getGuardedInvocation$0(LinkerServicesImpl.java:137)
    at jdk.dynalink/jdk.dynalink.LinkerServicesImpl.getWithLookupInternal(LinkerServicesImpl.java:168)
    at jdk.dynalink/jdk.dynalink.LinkerServicesImpl.getGuardedInvocation(LinkerServicesImpl.java:135)
    at jdk.dynalink/jdk.dynalink.DynamicLinker.relink(DynamicLinker.java:242)
    at jdk.scripting.nashorn.scripts/jdk.nashorn.internal.scripts.Script$Recompilation$66$definitionCheck$cu1$restOf.:program(definitionCheck.js:439)
    at jdk.scripting.nashorn/jdk.nashorn.internal.runtime.ScriptFunctionData.invoke(ScriptFunctionData.java:655)
    at jdk.scripting.nashorn/jdk.nashorn.internal.runtime.ScriptFunction.invoke(ScriptFunction.java:513)
    at jdk.scripting.nashorn/jdk.nashorn.internal.runtime.ScriptRuntime.apply(ScriptRuntime.java:527)
    at jdk.scripting.nashorn/jdk.nashorn.api.scripting.NashornScriptEngine.evalImpl(NashornScriptEngine.java:456)
    at jdk.scripting.nashorn/jdk.nashorn.api.scripting.NashornScriptEngine.evalImpl(NashornScriptEngine.java:413)
    at jdk.scripting.nashorn/jdk.nashorn.api.scripting.NashornScriptEngine.evalImpl(NashornScriptEngine.java:409)
    at jdk.scripting.nashorn/jdk.nashorn.api.scripting.NashornScriptEngine.eval(NashornScriptEngine.java:157)
    at java.scripting/javax.script.AbstractScriptEngine.eval(AbstractScriptEngine.java:249)
    at mmj.pa.MacroManager.runMacroRaw(MacroManager.java:217)
    at mmj.pa.MacroManager.runMacro(MacroManager.java:154)
    at mmj.util.ProofAsstBoss.doSetMMDefinitionsCheck(ProofAsstBoss.java:850)
    at mmj.util.Boss.lambda$0(Boss.java:107)
    at mmj.util.Boss.doRunParmCommand(Boss.java:121)
    at mmj.util.BatchFramework.executeRunParmCommand(BatchFramework.java:281)
    at mmj.util.BatchFramework.runIt(BatchFramework.java:223)
    at mmj.util.BatchMMJ2.main(Unknown Source)

[Benoit]

Alexander, regarding my previous message, can you tell me how you recompiled mmj2 ?  Have you had to type something like

javac -cp org.json-20161124.jar `find -name *.java` -d ../classes

(as in the compilescript.txt that comes with mmj2).  Did it produce errors ?

Thanks,
Benoît

[Alexander van der Vekens]

I imported the source code into eclipse and compiled it there. Regarding the JSON library, I extracted the package org.json from the mmj2.jar file, because I didn't find such a library within the mmj2.zip which I downloaded from the metamath web site (the folder ...\mmj2\lib\JSON-java\org\json is empty!).  Where did you find the org.json-20161124.jar? I remember that I also got errors when trying to use other (versions of) JSON libraries.

Alexander

[Benoit]

On Thursday, March 28, 2019 at 6:00:11 PM UTC+1, Alexander van der Vekens wrote:

I imported the source code into eclipse and compiled it there. Regarding the JSON library, I extracted the package org.json from the mmj2.jar file, because I didn't find such a library within the mmj2.zip which I downloaded from the metamath web site (the folder ...\mmj2\lib\JSON-java\org\json is empty!).  Where did you find the org.json-20161124.jar? I remember that I also got errors when trying to use other (versions of) JSON libraries.

Googling, I found https://stackoverflow.com/questions/2611834/latest-org-json which points to https://github.com/stleary/JSON-java .  There, I got json-20180813.jar.  Typing " javac -cp json-20180813.jar `find -name *.java` -d ../classes " in mmj2/src, I got 32 errors (with org.json-20161124.jar, it was 33 errors).  Which version are you using, since apparently it compiles with your version ?  (The info at https://stackoverflow.com/questions/9153571/is-there-a-way-to-get-version-from-package-json-in-nodejs-code might be useful.)

Thanks,

Benoît

[Alexander van der Vekens]

... as I said before, I extracted the package org.json from the mmj2.jar file and used this as JSON library (in Eclipse it was sufficient to store the class file in a lib folder). Unfortunately, there is no hint from which  jar-Version these class files were taken/generated, so I have no clue which version I am using. Your link only describes how the version can be obtained in nodejs. Maybe you can also extract the package org.json from the mmj2.jar file, store it in a local folder and use this folder as argument for -cp.

[Benoit]

On Saturday, March 30, 2019 at 5:01:01 PM UTC+1, Alexander van der Vekens wrote:

... as I said before, I extracted the package org.json from the mmj2.jar file and used this as JSON library

Sorry, I had missed that.  I extracted the files org/json/* from the existing mmj2.jar file, and then typed

  javac `find -name *.java` -d ../classes

which compiled with no error (but 5 deprecation warnings when used with the option -Xlint:deprecation)

Then, I typed (as recommended in compile/linux/compilescript.txt)

  `find -name "*.class"` | sed -e "s/^\.\///"

(I added a missing backquote, hopefully at the right place), but got the error

  bash: ./mmj/pa/Serializer$1.class: Permission non accordée

which means "permission denied", so I typed

  chmod u+x ./mmj/pa/*
  `find -name "*.class"` | sed -e "s/^\.\///"

and got

  bash: ./mmj/pa/Serializer$1.class : impossible d'exécuter le fichier binaire : Erreur de format pour exec()

(cannot execute binary file, format error with exec()) and I'm stuck...

[Filip Cernatescu]

Hey guys!
Why do not try milgame0.8?
It can downloaded from: http://us.metamath.org/other/milpgame/milpgame.html

Regards Filip

[Benoit]

I will temporarily downgrade to java 8.  For the record, I typed

$ sudo apt install openjdk-8-jdk
$ sudo update-alternatives --config java
and selected java-8 as the default, and now I can launch and use mmj2.  I hope to be able to use mmj2 with java 11 in the future, and I would welcome any help.  Java 11 is the next LTS version of java after java 8, so it might be worthwhile to make mmj2 work with it.

Filip: thanks!  I might try milpgame.  What are the comparative advantages of milpgame and mmj2?  I see that both are in java; wouldn't it be more useful that both teams join efforts around one project?

--

Benoît

[Filip Cernatescu]

Hi Benoit!

Although both mmj2 and milpgame have similarities like:
both  are written in java,
in both we can enter proof backward and forward,
both have a syntactic parser(do not hesitate at unification(matching) ),
but milpgame is build from another perspective:
statements are shown using html definition,
the proof  is  shown as a  tree(like folders in windows ),
we can save partial proofs without the use of dummylink,etc.

Regards Filip