Crash on startup reading iset.mm

[jkingdon]

Using b7f15d5eb748f1d8c23a76ccdbc2bd54ff6377ed of iset.mm (from the develop branch of https://github.com/metamath/set.mm ), mmj2 crashes on startup.

OpenJDK 64-Bit Server VM warning: Using incremental CMS is deprecated and will likely be removed in a future release

CommandLineArguments.displayArgumentOptionReport():

Hi! I am mmj2 v2.5.1 as of 29-Dec-2016.
Visit https://github.com/digama0/mmj2/ or
http://code.google.com/p/metamath-mmj2/
for support or bug reports.

  Command Line Arguments:
    Arg #1 = RunParms.txt
    Arg #2 = Y
    Arg #3 = /home/jkingdon/work/mmj2/mmj2jar
    Arg #4 = /home/jkingdon/work/mmj2/mmj2jar
    Arg #5 = 

  [3] mmj2Path     = /home/jkingdon/work/mmj2/mmj2jar (e.g. /home/jkingdon/work/mmj2/mmj2jar/YourFile.xyz)
  [4] metamathPath = /home/jkingdon/work/mmj2/mmj2jar (e.g. /home/jkingdon/work/mmj2/mmj2jar/YourFile.xyz)
  [5] svcPath      = null (e.g. /home/jkingdon/work/mmj2/mmj2jar/YourFile.xyz)
  [1] runParmFile  = /home/jkingdon/work/mmj2/mmj2jar/RunParms.txt
  [2] displayMMJ2FailPopupWindow 
                   = true

***END CommandLineArguments.displayArgumentOptionReport()***

I-UT-0015 **** Processing RunParmFile Command #1 = LoadFile,set.mm
I-UT-0015 **** Processing RunParmFile Command #2 = VerifyProof,*
I-UT-0015 **** Processing RunParmFile Command #3 = Parse,* 
I-UT-0015 **** Processing RunParmFile Command #4 = ProofAsstUnifySearchExclude,biigb,xxxid,dummylink
I-UT-0015 **** Processing RunParmFile Command #5 = ProofAsstProofFolder,myproofs
I-UT-0015 **** Processing RunParmFile Command #6 = TheoremLoaderMMTFolder,myproofs
I-UT-0015 **** Processing RunParmFile Command #7 = RunProofAsstGUI
I-PA-0412 Excluded these assertions from Unification search list as requested on input RunParm: [dummylink]

[digama0]

There is no error? All the console output there is normal. In particular, the first line of the RunParms file read according to that was LoadFile,set.mm so it's not even looking at iset.mm. How were you pointing it at iset.mm?

[jkingdon]

Oops, copy-pasted the wrong output, there is a NullPointerException:

OpenJDK 64-Bit Server VM warning: Using incremental CMS is deprecated and will likely be removed in a future release

CommandLineArguments.displayArgumentOptionReport():

Hi! I am mmj2 v2.5.1 as of 29-Dec-2016.
Visit https://github.com/digama0/mmj2/ or
http://code.google.com/p/metamath-mmj2/
for support or bug reports.

  Command Line Arguments:
    Arg #1 = RunParms.txt
    Arg #2 = Y
    Arg #3 = /home/jkingdon/work/mmj2/mmj2jar/
    Arg #4 = /home/jkingdon/work/metamath/metamath/
    Arg #5 = 

  [3] mmj2Path     = /home/jkingdon/work/mmj2/mmj2jar (e.g. /home/jkingdon/work/mmj2/mmj2jar/YourFile.xyz)
  [4] metamathPath = /home/jkingdon/work/metamath/metamath (e.g. /home/jkingdon/work/metamath/metamath/YourFile.xyz)
  [5] svcPath      = null (e.g. /home/jkingdon/work/mmj2/mmj2jar/YourFile.xyz)
  [1] runParmFile  = /home/jkingdon/work/mmj2/mmj2jar/RunParms.txt
  [2] displayMMJ2FailPopupWindow 
                   = true

***END CommandLineArguments.displayArgumentOptionReport()***

I-UT-0015 **** Processing RunParmFile Command #1 = LoadFile,iset.mm
I-UT-0015 **** Processing RunParmFile Command #2 = VerifyProof,*
I-UT-0015 **** Processing RunParmFile Command #3 = Parse,* 
null
java.lang.NullPointerException
    at mmj.verify.GrammarRule.buildRuleFormatExpr(GrammarRule.java:653)
    at mmj.verify.GrammarRule.add(GrammarRule.java:315)
    at mmj.verify.Grammar.initializeGrammarTables(Grammar.java:973)
    at mmj.verify.Grammar.initializeGrammar(Grammar.java:704)
    at mmj.util.GrammarBoss.initializeGrammar(GrammarBoss.java:288)
    at mmj.util.GrammarBoss.doParse(GrammarBoss.java:242)
    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(BatchMMJ2.java:53)

[digama0]

The error is occurring during the creation of grammar rules after reading wceq. The problem is that cA and cB have been removed. mmj2 doesn't like local variables. Make sure that all variables are declared in global scope (they can be declared in local scope as well, like wceq.cA, but there should be a global counterpart and they should match).

mmj2 works well with the full set.mm grammar, but this means you should keep the definition of class as well and the axioms relating to classes, not just pure predicate logic. (We should figure out what intuitionistic ZF looks like, but for now just use the original ZF axioms.)

[jkingdon]

Like this? https://github.com/metamath/set.mm/compare/develop...jkingdon:mmj2-friendly?expand=1

I'm still getting NullPointerException at mmj.verify.GrammarRule.buildRuleFormatExpr(GrammarRule.java:653) even with that change.

[digama0]

I get errors about $f declarations without $v with that version. I suggest just copying the beginning of the "class abstractions" section of set.mm verbatim and editing to taste.

[digama0]

I also get errors in the JS scripts when the mathbox theorem is missing. I suggest you put it in too.

[jkingdon]

Ah, cool, I see. With the change at https://github.com/metamath/set.mm/pull/173 mmj2 seems to be working better.