Lots of little things to fix. I'm just copying my notes so there are no surprises later...
`===
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
mmj2 :PA GUI Help needs updating:
Proof Worksheet -> proof step numbers out of date
File -> missing items
Edit / Undo -> out of date
===
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
- mmj2 : TL Menu Items:
- Unable to set Theorem Loader Store Formulas ASIS to false
- Unable to set Theorem Loader Audit Messages to false
- Many problems setting Theorem Loader mmt folder, including
showing an error message with a getYesNoAnswer() dialog!
===
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
- mmj2 : File/Save Proof File
File/Save As
File/Open Proof File show default directory
of user2, not the mmj2Path or the already given
ProofAsstProofFolder.
===
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
- mmj2 : File/New Proof asked for Theorem Label, accepted invalid
label (see Proof Worksheet below):
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
- mmj2 : Ctrl-U causes abort with following proof worksheet
(and note that Highlighting is off, the dump just shows
method/object names.) It is stored in blablah/mytemp/assdfsadf.mmp
and all that is need to create the abort is to open proof file and
hit ctrl-u.
Exception in thread "Thread-1" java.lang.NullPointerException
at mmj.pa.ProofAsst.unifyProofWorksheet(ProofAsst.java:1691)
at mmj.pa.ProofAsst.unify(ProofAsst.java:660)
at mmj.pa.ProofAsstGUI$44.send(ProofAsstGUI.java:2145)
at mmj.pa.ProofAsstGUI$RequestThreadStuff.run(ProofAsstGUI.java:2315)
at java.lang.Thread.run(Thread.java:748)
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
- mmj2 : runparm TheoremLoaderMMTFolder,myproofs/mmt
causes abort.
Attempting first batch test of UT19100updated.txt
END CommandLineArguments.displayArgumentOptionReport()
I-UT-0015 Processing RunParmFile Command #1 = ProofAsstHighlightingEnabled,no
I-UT-0015 Processing RunParmFile Command #2 = MacrosEnabled,no
I-UT-0015 Processing RunParmFile Command #3 = ProofAsstProofFolder,myproofs/mmp
I-UT-0015 Processing RunParmFile Command #4 = TheoremLoaderMMTFolder,myproofs/mmt
mmj.pa.MMJException: A-UT-0200 Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line.
Review previous error messages to find the error.
java.lang.IllegalArgumentException: mmj.pa.MMJException: A-UT-0200 Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line.
Review previous error messages to find the error.
at mmj.util.Boss.error(Boss.java:755)
at mmj.util.Boss.error(Boss.java:746)
at mmj.util.Boss.error(Boss.java:740)
at mmj.util.LogicalSystemBoss.getLogicalSystem(LogicalSystemBoss.java:164)
at mmj.util.TheoremLoaderBoss.getTlPreferences(TheoremLoaderBoss.java:105)
at mmj.util.TheoremLoaderBoss.editTheoremLoaderMMTFolder(TheoremLoaderBoss.java:158)
at mmj.util.Boss.lambda$0(Boss.java:107)
at mmj.util.Boss.doRunParmCommand(Boss.java:121)
at mmj.util.BatchFramework.executeRunParmCommand(BatchFramework.java:290)
at mmj.util.BatchFramework.runIt(BatchFramework.java:231)
at mmj.util.BatchMMJ2.main(BatchMMJ2.java:55)
Caused by: mmj.pa.MMJException: A-UT-0200 Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line.
Review previous error messages to find the error.
... 10 more
mmj.pa.MMJException: A-UT-0200 Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line.
Review previous error messages to find the error.
logout
Saving session...
...copying shared history...
...saving history...truncating history files...
...completed.
[Process completed]
RESOLVED: The RunParm cannot be input before LoadFile:
TheoremLoaderMMTFolder,myproofs/mmt.
(I did not know that.)
====
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
- mmj2 : runparm file paths with '\' in RunParm causing
problems on Mac, but '/' ok. These are supposed
to be system independent (in the code measures
are required.)
====
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
- mmj2 : Theorem Loader exports csbima12g to mmt folder
with ANY proof format "normal", "packed" or "compressed"
and gibberish? is the result?
NEGATIVE: output in .mmt always packed format,
which is not recognized when loaded by TL...
${
$d x y z $. $d A y $. $d A z $. $d B y $. $d B z $. $d C y $. $d C z $.
$d F y $. $d F z $.
$( Move class substitution in and out of the image of a function.
(Contributed by FL, 15-Dec-2006.) $)
csbima12g $p |- ( A e. C -> [ A / x ] ( F " B ) = ( [ A / x ] F " [ A
/ x ] B ) ) $=
cA cC 1:wcel vy cA vx vy 2:cv cF cB 3:cima 4:csb csb vy cA vx 2 cF 5:csb
6:csb vy cA vx 2 cB 7:csb 8:csb 9:cima vx cA 3 csb vx cA cF 10:csb vx cA
cB 11:csb 12:cima vy vz cA 4 9 cC 1 vy vz 6 8 1 vy ax-17 vy vz cA 5 cC vz
13:cv cA wcel vy 14:ax-17 hbcsb1g vy vz cA 7 cC 14 hbcsb1g hbimad 2 cA
15:wceq 4 5 7 16:cima 6 7 cima 9 4 16 17:wceq 15 vx cv 2 18:wceq vx wex
17 vx vy a9e 18 17 vx vx vz vz 4 16 vx vz 2 3 vy 19:visset 13 2 wcel vx
20:ax-17 hbcsb1 vx vz 5 7 vx vz 2 cF 19 20 hbcsb1 vx vz 2 cB 19 20 hbcsb1
hbima hbeq 18 3 5 cB cima 4 16 18 cF 5 cB vx 2 cF csbeq1a imaeq1d vx 2 3
csbeq1a 18 cB 7 5 vx 2 cB csbeq1a imaeq2d 3eqtr3d 19.23ai ax-mp a1i 15 5
6 7 vy cA 5 csbeq1a imaeq1d 15 7 8 6 vy cA 7 csbeq1a imaeq2d 3eqtrd
csbiegf vx vy cA 3 cC csbcog 1 9 10 8 cima 12 1 6 10 8 vx vy cA cF cC
csbcog imaeq1d 1 8 11 10 vx vy cA cB cC csbcog imaeq2d eqtrd 3eqtr3d $.
$}
====
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
- mmj2 : Edit/Set Soft DJ Vars Error Handling = 2, Report is
being processed exactly like 1, Ignore. There are
supposed to be output error messages in the messages
window.
Lots of little things to fix. I'm just copying my notes so there are no surprises later...
`===
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
===
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
===
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
===
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
$( THEOREM=as;dfkljasdjklf;laaldfsjl;aadjksf;laadjksfl;adjksfl;adjksflk;ajsdkfl;jaskdlfjkl;aadksjflasjdfjlasdfasldfjklasdjfk;a;fdl;agjl;akgj LOC_AFTER=?
h1:: |- ? 2:?: |- ? qed:?: |- ?
$)
===
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
Exception in thread "Thread-1" java.lang.NullPointerException at mmj.pa.ProofAsst.unifyProofWorksheet(ProofAsst.java:1691) at mmj.pa.ProofAsst.unify(ProofAsst.java:660) at mmj.pa.ProofAsstGUI$44.send(ProofAsstGUI.java:2145) at mmj.pa.ProofAsstGUI$RequestThreadStuff.run(ProofAsstGUI.java:2315) at java.lang.Thread.run(Thread.java:748)
$( THEOREM=aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa LOC_AFTER=?
qed:?: |- ph
$)
====
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
END CommandLineArguments.displayArgumentOptionReport()
I-UT-0015 Processing RunParmFile Command #1 = ProofAsstHighlightingEnabled,no I-UT-0015 Processing RunParmFile Command #2 = MacrosEnabled,no I-UT-0015 Processing RunParmFile Command #3 = ProofAsstProofFolder,myproofs/mmp I-UT-0015 Processing RunParmFile Command #4 = TheoremLoaderMMTFolder,myproofs/mmt mmj.pa.MMJException: A-UT-0200 Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line. Review previous error messages to find the error. java.lang.IllegalArgumentException: mmj.pa.MMJException: A-UT-0200 Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line. Review previous error messages to find the error. at mmj.util.Boss.error(Boss.java:755) at mmj.util.Boss.error(Boss.java:746) at mmj.util.Boss.error(Boss.java:740) at mmj.util.LogicalSystemBoss.getLogicalSystem(LogicalSystemBoss.java:164) at mmj.util.TheoremLoaderBoss.getTlPreferences(TheoremLoaderBoss.java:105) at mmj.util.TheoremLoaderBoss.editTheoremLoaderMMTFolder(TheoremLoaderBoss.java:158) at mmj.util.Boss.lambda$0(Boss.java:107) at mmj.util.Boss.doRunParmCommand(Boss.java:121) at mmj.util.BatchFramework.executeRunParmCommand(BatchFramework.java:290) at mmj.util.BatchFramework.runIt(BatchFramework.java:231) at mmj.util.BatchMMJ2.main(BatchMMJ2.java:55) Caused by: mmj.pa.MMJException: A-UT-0200 Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line. Review previous error messages to find the error. ... 10 more mmj.pa.MMJException: A-UT-0200 Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line. Review previous error messages to find the error. logout Saving session... ...copying shared history... ...saving history...truncating history files... ...completed.
[Process completed]
====
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
====
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
ProofAsstHighlightingEnabled,no MacrosEnabled,no LoadFile,RegressionTest1set.mm VerifyProof, Parse, ProofAsstUnifySearchExclude,biigb,xxxid,dummylink ProofAsstProofFolder,myproofs/mmp/ TheoremLoaderMMTFolder,myproofs/mmt/temp ExtractTheoremToMMTFolder,csbima12g
${ $d x y z $. $d A y $. $d A z $. $d B y $. $d B z $. $d C y $. $d C z $. $d F y $. $d F z $. $( Move class substitution in and out of the image of a function. (Contributed by FL, 15-Dec-2006.) $) csbima12g $p |- ( A e. C -> [ A / x ] ( F " B ) = ( [ A / x ] F " [ A / x ] B ) ) $= cA cC 1:wcel vy cA vx vy 2:cv cF cB 3:cima 4:csb csb vy cA vx 2 cF 5:csb 6:csb vy cA vx 2 cB 7:csb 8:csb 9:cima vx cA 3 csb vx cA cF 10:csb vx cA cB 11:csb 12:cima vy vz cA 4 9 cC 1 vy vz 6 8 1 vy ax-17 vy vz cA 5 cC vz 13:cv cA wcel vy 14:ax-17 hbcsb1g vy vz cA 7 cC 14 hbcsb1g hbimad 2 cA 15:wceq 4 5 7 16:cima 6 7 cima 9 4 16 17:wceq 15 vx cv 2 18:wceq vx wex 17 vx vy a9e 18 17 vx vx vz vz 4 16 vx vz 2 3 vy 19:visset 13 2 wcel vx 20:ax-17 hbcsb1 vx vz 5 7 vx vz 2 cF 19 20 hbcsb1 vx vz 2 cB 19 20 hbcsb1 hbima hbeq 18 3 5 cB cima 4 16 18 cF 5 cB vx 2 cF csbeq1a imaeq1d vx 2 3 csbeq1a 18 cB 7 5 vx 2 cB csbeq1a imaeq2d 3eqtr3d 19.23ai ax-mp a1i 15 5 6 7 vy cA 5 csbeq1a imaeq1d 15 7 8 6 vy cA 7 csbeq1a imaeq2d 3eqtrd csbiegf vx vy cA 3 cC csbcog 1 9 10 8 cima 12 1 6 10 8 vx vy cA cF cC csbcog imaeq1d 1 8 11 10 vx vy cA cB cC csbcog imaeq2d eqtrd 3eqtr3d $. $}
====
2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
==== `