search

digama0 / mmj2

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

What is the minimum from set.mm for mmj2 to start up #14

Closed htzh closed 5 years ago

htzh commented 5 years ago

I tried to get mmj2 to start on a small file (proved and saved from metamath) and it failed with:

I-UT-0015 **** Processing RunParmFile Command #7 = RunProofAsstGUI
mmj.pa.ProofAsstException: A-PA-0902 Input list of assertions (for unification)empty!
java.lang.IllegalArgumentException: mmj.pa.ProofAsstException: A-PA-0902 Input list of assertions (for unification) empty!
        at mmj.pa.StepSelectorSearch.<init>(StepSelectorSearch.java:83)
        at mmj.pa.ProofUnifier.initializeLookupTables(ProofUnifier.java:292)
        at mmj.pa.ProofAsst.initializeLookupTables(ProofAsst.java:255)
        at mmj.util.ProofAsstBoss.getProofAsst(ProofAsstBoss.java:316)
        at mmj.util.ProofAsstBoss.doRunProofAsstGUI(ProofAsstBoss.java:1009)
        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)
Caused by: mmj.pa.ProofAsstException: A-PA-0902 Input list of assertions (for unification) empty!
        at mmj.pa.StepSelectorSearch.<init>(StepSelectorSearch.java:84)
        ... 9 more
mmj.pa.ProofAsstException: A-PA-0902 Input list of assertions (for unification)empty!

I had noticed earlier that I had to add the constants $c wff |- set class $. from set.mm to even get this far. The content is very minimal right now:

  $c wff |- set class $. $( Keep mmj2 happy $)

  $c cat term cj $.
  $v C C1 C2 D D1 D2 $.
  cC $f cat C $.
  cC1 $f cat C1 $.

  ${
    $( PLEASE PUT DESCRIPTION HERE. $)
    cat-term $a term C $.
  $}

  ${
    $( PLEASE PUT DESCRIPTION HERE. $)
    cat-term2 $p term C1 $=
    cC1 cat-term $.
  $}

And RunParms look like

LoadFile,../../metamath/ct.mm
VerifyProof,*
Parse,*
ProofAsstUnifySearchExclude,biigb,xxxid,dummylink
ProofAsstProofFolder,myproofs
TheoremLoaderMMTFolder,myproofs
RunProofAsstGUI
digama0 commented 5 years ago

mmj2 expects to be proving theorems of the form |- thing to prove. I think you have to declare your "logical typecode" to be term if you want your theorems to have the form term bla instead of |- bla, but mmj2 assumes there is only one logical typecode. (I made some attempts to generalize this but I forget how far I got.)

You will also want to disable macros if you are getting an error in transformations.js; this file assumes you are working on set.mm or one of its derivatives, and there is no good way to detect if this is actually the case.

digama0 commented 5 years ago

You need to set ProvableLogicStmtType and LogicStmtType if you want to change the default logical typecodes.

htzh commented 5 years ago

That makes sense. I added a turnstile assertion and the exception did go away. I don't have a problem with using the turnstile. I saw your message at the Google group as well. Thanks a lot for the help! I will close the issue now and ask further questions over at the group.