search

digama0 / mmj2

mmj2 GUI Proof Assistant for the Metamath project
GNU General Public License v2.0
72 stars 24 forks source link

mmj2 setup for Mac OS #21

Closed ammkrn closed 4 years ago

ammkrn commented 4 years ago

I'm using Mac OS 10.12.6 and and had some issues when going through the tutorial video David Wheeler was soliciting feedback on in the user group. For anyone else who runs across this (or for the maintainers if you want to update the README), the latest version of JDK does not seem to work well with mmj2 on mac OS, but I was able to get a working setup by installing openjdk 8 via homebrew with the following two commands :

brew tap adoptopenjdk/openjdk
brew cask install adoptopenjdk8

You also need to edit mmj2/mmj2jar/MacMMJ2.command to look like this, where is replaced by a fully qualified path, and the last one points to whatever the location of the metamath executable is on your system. Also if you don't increase the value after -Xmx to at least 512, the startup script just hangs at LoadFile,set.mm.

java -Xincgc -Xms128M -Xmx512M -jar <your_prefix>/mmj2/mmj2jar/mmj2.jar "<your_prefix>/mmj2/mmj2jar/RunParms.txt" Y "<your_prefix>/mmj2/mmj2jar/" "<your_prefix>/metamath/metamath/" ""

On the off chance that the maintainers are interested, using the latest version of Java (specifically 13.0.1) produces the following error and fails to render what's seen in the video both when attempting to open a mmp file and when attempting to unify using the option from the dropdown menu :

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.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.access$19(ProofAsstGUI.java:615)
    at mmj.pa.ProofAsstGUI$19.receive(ProofAsstGUI.java:937)
    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(AccessController.java:391)
    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)
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)
digama0 commented 4 years ago

The DefaultDocumentEventUndoableWrapper bug is an incompatibility with Java 9+ that has been fixed in the master branch.

digama0 commented 4 years ago

Regarding Mac OS setup, I don't have one to test, but some people have reported that -Xincgc doesn't work any more; is that true?

Is it possible to use relative paths in the invocation? Alternatively, the path could be determined by a pwd like command, so that people don't have to edit the script.

digama0 commented 4 years ago

My shell script (on linux) looks like this (using relative paths):

java -Xms512M -Xmx1024M -jar mmj2.jar myRunParms.txt Y '' '../../metamath' ''

although people will probably want to edit the ../../metamath part as that depends on where the .mm files are being stored.

ammkrn commented 4 years ago

Yeah, constructing the paths with ../<wherever> works fine.

With Java 13, the -Xincgc flag IS NOT recognized, which causes the startup script to fail. Removing it does not seem to cause any issues and allows the script to execute. With OpenJDK8, -Xincgc IS recognized, and actually seems to be necessary; removing it allows the GUI to start, but immediately encounters an error : GC overhead limit exceeded which closes the program. The terminal output is :

GC overhead limit exceeded
java.lang.OutOfMemoryError: GC overhead limit exceeded
    at mmj.lang.ParseNodeHolder.<init>(ParseNodeHolder.java:94)
    at mmj.lang.Formula.getParseNodeHolderExpr(Formula.java:402)
    at mmj.verify.Grammar.grammaticalParseOneFormula(Grammar.java:795)
    at mmj.verify.Grammar.parseAllFormulas(Grammar.java:657)
    at mmj.util.GrammarBoss.doParse(GrammarBoss.java:250)
    at mmj.util.GrammarBoss$$Lambda$36/1128032093.run(Unknown Source)
    at mmj.util.Boss.lambda$0(Boss.java:107)
    at mmj.util.Boss$$Lambda$7/824909230.getAsBoolean(Unknown Source)
    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(BatchMMJ2.java:53)

Also I was on master when I was getting the Exception in thread "AWT-EventQueue-0" Ignoring exception: error, but again only with Java 13.

digama0 commented 4 years ago

I think you should double check that you are running the latest version (you will have to recompile it to use the bleeding edge version), as the class cast exception at CompoundUndoManager.java:110 appears to be this line. Line 110 is not a cast in the latest version.

ammkrn commented 4 years ago

In that case I'm sure you're right that recompiling would fix it. I'm way outside of my wheelhouse with Java and I wasn't able to find any compilation instructions or related files for mac OS (mmj2/compile contains directories linux, mmj2, and windows).

bryangingechen commented 4 years ago

The linux compile directions work for me in mac OS, but I had to change the last line to this:

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

because mac OS uses a different version of find. I believe this command should actually work in both mac OS and Linux.

I also made the following note for running the tutorial; I guess this is consistent with the linux shell script above:

# run tutorial from project root with:
# java -Xms512M -Xmx1024M -jar mmj2.jar "MacRunParmsPATutorial.txt" Y "mmj2jar/" "mmj2jar/" ""
ammkrn commented 4 years ago

@bryangingechen Executing the linux script on my machine (and JDK 13) with the change you mentioned returns a bunch of errors about not finding stuff :

./mmj/pa/PaConstants.java:121: error: package org.json does not exist
import org.json.JSONArray;
               ^
./mmj/pa/PaConstants.java:122: error: package org.json does not exist
import org.json.JSONObject;
               ^
./mmj/tmff/TMFFPreferences.java:49: error: package org.json does not exist
import org.json.JSONArray;
               ^
./mmj/tmff/TMFFPreferences.java:50: error: package org.json does not exist
import org.json.JSONObject;
               ^
./mmj/lang/Stmt.java:47: error: package org.json does not exist
import org.json.JSONObject;
               ^
./mmj/lang/Stmt.java:48: error: package org.json does not exist
import org.json.JSONString;
               ^
./mmj/lang/Stmt.java:88: error: cannot find symbol
public abstract class Stmt extends MObj implements JSONString {
                                                   ^
  symbol: class JSONString
./mmj/pa/BaseSetting.java:71: error: cannot find symbol
        extends BaseSetting<T>, JSONSerializable, JSONString
                                                  ^
  symbol:   class JSONString
  location: interface BaseSetting<T>
  where T is a type-variable:
    T extends Object declared in interface BaseSetting
./mmj/pa/BaseSetting.java:136: error: cannot find symbol
        default Object write() throws JSONException {
                                      ^
  symbol:   class JSONException
  location: interface JSONSetting<T>
  where T is a type-variable:
    T extends Object declared in interface JSONSetting
./mmj/tmff/TMFFMethod.java:18: error: package org.json does not exist
import org.json.JSONArray;
               ^
./mmj/tmff/TMFFMethod.java:54: error: cannot find symbol
    public abstract JSONArray asArray();
                    ^
  symbol:   class JSONArray
  location: class TMFFMethod
./mmj/pa/SessionStore.java:61: error: cannot find symbol
    public JSONObject load(final boolean intoSettings) throws IOException {
           ^
  symbol:   class JSONObject
  location: class SessionStore
./mmj/pa/SessionStore.java:76: error: cannot find symbol
    public JSONObject load(final boolean intoSettings,
           ^
  symbol:   class JSONObject
  location: class SessionStore
./mmj/pa/SessionStore.java:95: error: cannot find symbol
    public JSONObject load(final boolean intoSettings,
           ^
  symbol:   class JSONObject
  location: class SessionStore
./mmj/pa/SessionStore.java:126: error: cannot find symbol
    private void merge(final boolean intoSettings, final JSONObject store,
                                                         ^
  symbol:   class JSONObject
  location: class SessionStore
./mmj/pa/SessionStore.java:139: error: cannot find symbol
    private void mergeOne(final boolean intoSettings, final JSONObject store,
                                                            ^
  symbol:   class JSONObject
  location: class SessionStore
./mmj/pa/PaConstants.java:2940: error: cannot find symbol
    public static final JSONObject JSON_INTRODUCTION = new JSONObject()
                        ^
  symbol:   class JSONObject
  location: class PaConstants
./mmj/pa/Serializer.java:23: error: package org.json does not exist
import org.json.*;
^
./mmj/pa/SessionStore.java:22: error: package org.json does not exist
import org.json.*;
^
./mmj/pa/BaseSetting.java:6: error: package org.json does not exist
import org.json.*;
^
./mmj/tmff/TMFFAlignColumn.java:24: error: package org.json does not exist
import org.json.JSONArray;
               ^
./mmj/tmff/TMFFAlignColumn.java:221: error: cannot find symbol
    public JSONArray asArray() {
           ^
  symbol:   class JSONArray
  location: class TMFFAlignColumn
./mmj/tmff/TMFFFlat.java:18: error: package org.json does not exist
import org.json.JSONArray;
               ^
./mmj/tmff/TMFFFlat.java:47: error: cannot find symbol
    public JSONArray asArray() {
           ^
  symbol:   class JSONArray
  location: class TMFFFlat
./mmj/tmff/TMFFTwoColumnAlignment.java:25: error: package org.json does not exist
import org.json.JSONArray;
               ^
./mmj/tmff/TMFFTwoColumnAlignment.java:106: error: cannot find symbol
    public JSONArray asArray() {
           ^
  symbol:   class JSONArray
  location: class TMFFTwoColumnAlignment
./mmj/tmff/TMFFUnformatted.java:24: error: package org.json does not exist
import org.json.JSONArray;
               ^
./mmj/tmff/TMFFUnformatted.java:45: error: cannot find symbol
    public JSONArray asArray() {
           ^
  symbol:   class JSONArray
  location: class TMFFUnformatted
./mmj/verify/LRParser.java:20: error: package org.json does not exist
import org.json.JSONArray;
               ^
./mmj/verify/LRParser.java:21: error: package org.json does not exist
import org.json.JSONObject;
               ^
./mmj/verify/LRParser.java:667: error: cannot find symbol
        public JSONObject transitions;
               ^
  symbol:   class JSONObject
  location: class ParseTableRow
./mmj/pa/PaConstants.java:2944: error: cannot find symbol
        .put("-comments", new JSONArray(
                              ^
  symbol:   class JSONArray
  location: class PaConstants
./mmj/pa/PaConstants.java:2943: error: cannot find symbol
        .put(SessionStore.KEY_REMOVE, new JSONArray())
                                          ^
  symbol:   class JSONArray
  location: class PaConstants
./mmj/pa/PaConstants.java:2942: error: cannot find symbol
        .put(SessionStore.KEY_OVERRIDE, new JSONObject())
                                            ^
  symbol:   class JSONObject
  location: class PaConstants
./mmj/pa/PaConstants.java:2941: error: cannot find symbol
        .put(SessionStore.KEY_STORE, new JSONObject())
                                         ^
  symbol:   class JSONObject
  location: class PaConstants
./mmj/pa/PaConstants.java:2940: error: cannot find symbol
    public static final JSONObject JSON_INTRODUCTION = new JSONObject()
                                                           ^
  symbol:   class JSONObject
  location: class PaConstants
./mmj/pa/BaseSetting.java:136: error: write() in JSONSetting clashes with write() in JSONSerializable
        default Object write() throws JSONException {
                       ^
  overridden method does not throw JSONException
./mmj/pa/BaseSetting.java:116: error: cannot find symbol
            return setSerialT(new JSONTokener(newValue).nextValue());
                                  ^
  symbol:   class JSONTokener
  location: interface JSONSetting<T>
  where T is a type-variable:
    T extends Object declared in interface JSONSetting
./mmj/pa/BaseSetting.java:142: error: cannot find symbol
                return JSONObject.valueToString(getSerial());
                       ^
  symbol:   variable JSONObject
  location: interface JSONSetting<T>
  where T is a type-variable:
    T extends Object declared in interface JSONSetting
./mmj/pa/BaseSetting.java:143: error: cannot find symbol
            } catch (final JSONException e) {
                           ^
  symbol:   class JSONException
  location: interface JSONSetting<T>
  where T is a type-variable:
    T extends Object declared in interface JSONSetting
./mmj/pa/SessionStore.java:103: error: cannot find symbol
                    dat = new JSONTokener(r).nextValue();
                              ^
  symbol:   class JSONTokener
  location: class SessionStore
./mmj/pa/SessionStore.java:107: error: cannot find symbol
            final JSONObject o = dat instanceof JSONObject ? (JSONObject)dat
                  ^
  symbol:   class JSONObject
  location: class SessionStore
./mmj/pa/SessionStore.java:107: error: cannot find symbol
            final JSONObject o = dat instanceof JSONObject ? (JSONObject)dat
                                                ^
  symbol:   class JSONObject
  location: class SessionStore
./mmj/pa/SessionStore.java:107: error: cannot find symbol
            final JSONObject o = dat instanceof JSONObject ? (JSONObject)dat
                                                              ^
  symbol:   class JSONObject
  location: class SessionStore
./mmj/pa/SessionStore.java:108: error: cannot find symbol
                : new JSONObject();
                      ^
  symbol:   class JSONObject
  location: class SessionStore
./mmj/pa/SessionStore.java:109: error: cannot find symbol
            JSONObject store = o.optJSONObject(KEY_STORE);
            ^
  symbol:   class JSONObject
  location: class SessionStore
./mmj/pa/SessionStore.java:111: error: cannot find symbol
                o.put(KEY_STORE, store = new JSONObject());
                                             ^
  symbol:   class JSONObject
  location: class SessionStore
./mmj/pa/SessionStore.java:112: error: cannot find symbol
            JSONArray remove = o.optJSONArray(KEY_REMOVE);
            ^
  symbol:   class JSONArray
  location: class SessionStore
./mmj/pa/SessionStore.java:114: error: cannot find symbol
                o.put(KEY_REMOVE, remove = new JSONArray());
                                               ^
  symbol:   class JSONArray
  location: class SessionStore
./mmj/pa/SessionStore.java:121: error: cannot find symbol
        } catch (final JSONException e) {
                       ^
  symbol:   class JSONException
  location: class SessionStore
./mmj/tmff/TMFFPreferences.java:212: error: cannot find symbol
            (final JSONObject o) -> o.entrySet().parallelStream()
                   ^
  symbol:   class JSONObject
  location: class TMFFPreferences
./mmj/tmff/TMFFPreferences.java:219: error: cannot find symbol
                    JSONObject::new)));
                    ^
  symbol:   class JSONObject
  location: class TMFFPreferences
./mmj/tmff/TMFFPreferences.java:221: error: cannot find symbol
        store.addSerializable("~" + PFX + "schemeMap", (final JSONObject o) -> {
                                                              ^
  symbol:   class JSONObject
  location: class TMFFPreferences
./mmj/tmff/TMFFPreferences.java:224: error: cannot find symbol
                    (JSONArray)e.getValue());
                     ^
  symbol:   class JSONArray
  location: class TMFFPreferences
./mmj/tmff/TMFFPreferences.java:232: error: cannot find symbol
                JSONObject::new)));
                ^
  symbol:   class JSONObject
  location: class TMFFPreferences
./mmj/lang/Stmt.java:422: error: method does not override or implement a method from a supertype
    @Override
    ^
./mmj/lang/Stmt.java:424: error: cannot find symbol
        return JSONObject.quote(label);
               ^
  symbol:   variable JSONObject
  location: class Stmt
./mmj/pa/Serializer.java:75: error: cannot find symbol
            o -> ((JSONArray)o).stream().map(this::deserialize)
                   ^
  symbol:   class JSONArray
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:78: error: cannot find symbol
                .collect(Collectors.toCollection(JSONArray::new)));
                                                 ^
  symbol:   class JSONArray
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:89: error: cannot find symbol
            o -> ((JSONArray)o).stream().map(this::deserialize)
                   ^
  symbol:   class JSONArray
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:92: error: cannot find symbol
                .collect(Collectors.toCollection(JSONArray::new)));
                                                 ^
  symbol:   class JSONArray
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:103: error: cannot find symbol
            o -> ((JSONArray)o).stream().map(this::deserialize)
                   ^
  symbol:   class JSONArray
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:106: error: cannot find symbol
                .collect(Collectors.toCollection(JSONArray::new)));
                                                 ^
  symbol:   class JSONArray
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:117: error: cannot find symbol
            o -> ((JSONObject)o).entrySet().stream()
                   ^
  symbol:   class JSONObject
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:118: error: incompatible types: cannot infer type-variable(s) T,K#1,U
                .collect(Collectors.toMap(Map.Entry::getKey,
                                         ^
    (argument mismatch; invalid method reference
      method getKey in interface Entry<K#2,V> cannot be applied to given types
        required: no arguments
        found:    Object
        reason: actual and formal argument lists differ in length)
  where T,K#1,U,K#2,V are type-variables:
    T extends Object declared in method <T,K#1,U>toMap(Function<? super T,? extends K#1>,Function<? super T,? extends U>)
    K#1 extends Object declared in method <T,K#1,U>toMap(Function<? super T,? extends K#1>,Function<? super T,? extends U>)
    U extends Object declared in method <T,K#1,U>toMap(Function<? super T,? extends K#1>,Function<? super T,? extends U>)
    K#2 extends Object declared in interface Entry
    V extends Object declared in interface Entry
./mmj/pa/Serializer.java:123: error: cannot find symbol
                    JSONObject::new)));
                    ^
  symbol:   class JSONObject
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:134: error: cannot find symbol
            o -> (o == JSONObject.NULL ? Optional.empty()
                       ^
  symbol:   variable JSONObject
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:136: error: cannot find symbol
            v -> v.map(this::serialize).orElse(JSONObject.NULL));
                                               ^
  symbol:   variable JSONObject
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:156: error: cannot find symbol
            final JSONArray a = (JSONArray)o;
                  ^
  symbol:   class JSONArray
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:156: error: cannot find symbol
            final JSONArray a = (JSONArray)o;
                                 ^
  symbol:   class JSONArray
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:160: error: cannot find symbol
            } catch (final JSONException e) {
                           ^
  symbol:   class JSONException
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:164: error: cannot find symbol
            final JSONArray a = new JSONArray(value.getRed(), value.getGreen(),
                  ^
  symbol:   class JSONArray
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:164: error: cannot find symbol
            final JSONArray a = new JSONArray(value.getRed(), value.getGreen(),
                                    ^
  symbol:   class JSONArray
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:171: error: cannot find symbol
            final JSONArray a = (JSONArray)o;
                  ^
  symbol:   class JSONArray
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:171: error: cannot find symbol
            final JSONArray a = (JSONArray)o;
                                 ^
  symbol:   class JSONArray
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:175: error: cannot find symbol
            } catch (final JSONException e) {
                           ^
  symbol:   class JSONException
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/pa/Serializer.java:178: error: cannot find symbol
        }, r -> new JSONArray(r.x, r.y, r.width, r.height));
                    ^
  symbol:   class JSONArray
  location: interface Serializer<T>
  where T is a type-variable:
    T extends Object declared in interface Serializer
./mmj/tmff/TMFFAlignColumn.java:222: error: cannot find symbol
        return new JSONArray(TMFFConstants.TMFF_METHOD_USER_NAME_ALIGN_COLUMN,
                   ^
  symbol:   class JSONArray
  location: class TMFFAlignColumn
./mmj/tmff/TMFFFlat.java:48: error: cannot find symbol
        return new JSONArray().put(TMFFConstants.TMFF_METHOD_USER_NAME_FLAT);
                   ^
  symbol:   class JSONArray
  location: class TMFFFlat
./mmj/tmff/TMFFTwoColumnAlignment.java:107: error: cannot find symbol
        return new JSONArray(
                   ^
  symbol:   class JSONArray
  location: class TMFFTwoColumnAlignment
./mmj/tmff/TMFFUnformatted.java:46: error: cannot find symbol
        return new JSONArray()
                   ^
  symbol:   class JSONArray
  location: class TMFFUnformatted
./mmj/verify/LRParser.java:76: error: cannot find symbol
        final Map<String, Integer> startDef = (Map<String, Integer>)(Object)new JSONObject();
                                                                                ^
  symbol:   class JSONObject
  location: class LRParser
./mmj/verify/LRParser.java:674: error: cannot find symbol
            transitions = new JSONObject();
                              ^
  symbol:   class JSONObject
  location: class ParseTableRow
./mmj/verify/LRParser.java:699: error: cannot find symbol
                final JSONArray map = (JSONArray)o;
                      ^
  symbol:   class JSONArray
  location: class ParseTableRow
./mmj/verify/LRParser.java:699: error: cannot find symbol
                final JSONArray map = (JSONArray)o;
                                       ^
  symbol:   class JSONArray
  location: class ParseTableRow
./mmj/verify/LRParser.java:709: error: cannot find symbol
                final JSONArray a = new JSONArray()
                      ^
  symbol:   class JSONArray
  location: class ParseTableRow
./mmj/verify/LRParser.java:709: error: cannot find symbol
                final JSONArray a = new JSONArray()
                                        ^
  symbol:   class JSONArray
  location: class ParseTableRow
./mmj/verify/LRParser.java:710: error: cannot find symbol
                    .put(row.transitions == null ? JSONObject.NULL
                                                   ^
  symbol:   variable JSONObject
  location: class ParseTableRow
Note: Some input files use or override a deprecated API.
Note: Recompile with -Xlint:deprecation for details.
88 errors
bryangingechen commented 4 years ago

@ammkrn Looks like you may might not have pulled the lib/JSON-java/org/ submodule in your local mmj2 repository.

Try running git submodule update --init --recursive.

ammkrn commented 4 years ago

That did it, thanks. So just for the record, the jar produced by recompiling on MacOS using the linux script seems to work fine with Java 13, and for MacOS users, you the steps to get started are:

  1. Clone mmj2 repo and its submodules
  2. Install JDK if you don't have it (you can get it via homebrew using brew cask install java
  3. Change the line in the /compile/linux/ script to look like the line below and recompile using said script 
    `find . -name "*.class" | sed -e "s/^\.\///"`
  4. Edit the file /mmj2jar/MacMMJ2.command, increasing the memory threshold, IE -Xms512M -Xmx1024M
  5. Change the placeholder paths in MacMMJ2.command to point to the mmj2.jar file, the file RunParms.txt, the directory mmj2jar, and the Metamath executable.

Example :

java -Xms512M -Xmx1024M -jar ./mmj2.jar "./RunParms.txt" Y "../mmj2jar/" "../../metamath/metamath/" ""