forked from digama0/mmj2
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCHGLOG.TXT
3037 lines (2384 loc) · 108 KB
/
CHGLOG.TXT
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
//*****************************************************************************/
//* Copyright (C) 2005-2013 */
//* MEL O'CAT X178G243 (at) yahoo (dot) com */
//* License terms: GNU General Public License Version 2 */
//* or any later version */
//*****************************************************************************/
//*456789012345678 (80-character line to adjust editor window) 456789012345678*/
================================================================================
2-Jan-2014:
CHANGES:
* The compression format has been updated to match the new compression
default of the metamath.exe program.
* Parse tree compression is now more efficient, which means that loading
completed proof worksheets and unifying a completed proof is faster.
* Bug fix for 17-Aug change, where steps with no variables or hypotheses
(such as the example below) would not be collapsed into a single step.
================================================================================
17-Aug-2013:
CHANGES:
* New proofs loaded via 'New-Next Proof' and related functions now have a
step layout that mirrors the compressed format instead of the uncompressed
RPN. This means that if a given step is referred to twice in a proof, the
step will only be assigned one step number, rather than making copies of
the statement for each use. (Depending on the proof, this can mean a
drastic decrease in the length of proofs as seen in the main text area of
ProofAsstGUI. The length of compressed and uncompressed proofs themselves
remains unaffected.) For example:
Before: After:
1::tru |- T. 1::tru |- T.
2::tru |- T. qed:1,1:pm3.2i |- ( T. /\ T. )
qed:1,2:pm3.2i |- ( T. /\ T. )
* New menu items "Unify+Don't Convert WorkVars" and "Unify+Erase+Don't
Convert" have been added to the Unify menu. When activated, they perform
the regular unification process, but if the process completes successfully
except that work variables (i.e. &C1, &S2, etc.) are in use in the
derivation steps, it will abort the unification process and move the
cursor to the first step containing a work variable, so that you can name
it properly. (The default option "Unify" will instead replace these
variables with dummy variables that have been taken from the pool of
unused variables defined in the .mm file.)
* The "Reformat" options no longer require you to save the file.
================================================================================
13-Aug-2013:
CHANGES:
* New proofs are now output by default in "compressed" format. This behavior
can be modified by the TL > Set Proof Compression option in ProofAsstGUI
or by setting the ProofAsstProofFormat RunParm (to Compressed, Packed, or
Normal).
* The code base target has been upgraded to 1.5 compatibility, and features
of Java 1.5 (primarily generics and enhanced for loops) have been utilized
throughout the program.
* Mel O'Cat's original search enhancements have been added to the project,
although since the source was decompiled from the release jar file,
comments and local variable names are missing. Primary documentation can
be found at
mmj2/doc/Release20121225/MMJ2_Release_20121225_Proposals.html
although that source is a proposal of new features, which includes a few
that were never implemented.
* Step names are no longer required to be ints, and are now allowed to be
arbitrary strings, with a few limitations.
- Since step names are matched case-insensitively, capital letters are
allowed, but will be normalized to lowercase upon the next unify.
- The space character and , and : are not allowed, for obvious reasons.
- There are two 'keywords' for step names: if the name is
(case-insensitively) equal to 'qed', it is identified as the final step,
and if the name begins with 'h', it is a hypothesis step.
* The default renumber settings have been changed, so that the numbering on
load and on renumber go up by tens, while the steps generated by Derive go
up by ones, but have a 'd' prefix, i.e. 'd1', 'd2', etc.
* The 'Step Search' / 'General Search' and 'Step Selector Search' dialogs
now use multiline list entries, so that selecting one assertion selects
all the lines of that assertion.
* The 'Request Messages' dialog has been deprecated, as the exact same
content is available in the lower pane of ProofAsstGUI. The compile-time
constant PaConstants.REQUEST_MESSAGES_GUI_ENABLED controls this new
behavior.
* A new RunParm 'ProofAsstLookAndFeel' now controls the Swing L&F for the
whole application. The default option (and whatwe used before this update)
is 'Metal', and a list of options (which are OS-dependent) is presented if
you type an incorrect option. (I recommend 'Nimbus', if available.)
* A new RunParm 'ProofAsstMaximized' now allows ProofAsstGUI to start in
fullscreen mode.
* Added support for compound edits for undo handling. This way, undo and
redo apply to entire blocks of text, rather than individual characters as
before. Furthermore (and most importantly), the full-buffer replacements
performed by Unify now count as a single edit, so you only have to Ctrl-Z
once to undo/redo unification.
* Fixed a bug wherein the cursor is positioned at steps with LocalRefs (say
because the user just typed the LocalRef), but since the step is deleted
during processing, the cursor loses its anchor and ends up at the top of
the file. (Very annoying!) Now, the cursor is never positioned at LocalRef
steps and instead goes to the first non-LocalRef step after the cursor.
* Malformed steps with only one colon are now interpreted as step:ref
instead of step:hyp if the second field starts with # (i.e. a LocalRef) or
it is a theorem or hypothesis in the database (no unification checks are
done; it is just a heuristic).
* Steps with no ref and no formula are no longer fatal unification errors.
Instead, they simply fail to unify, and give errors just like steps with
formulas, which is to say that step:: alone on a line gives error
E-PA-0411: Unification failure in derivation proof step.
and step:?: on a line gives no error at all.
* All the supplementary dialogs like Step Selector Search, Search Options,
and the Search Results window now close on ESC (they used to close on
ALT-F4, but it is easy to make a mistake and close something you don't
want to close using that key combo).
================================================================================
1-Nov-2011:
CHANGES:
This release includes small but excellent enhancements and a minor
but important bug fix.
-----------------------------------------------------------------
1. Quick Start (see also mmj2\QuickStart.html)
-----------------------------------------------------------------
Quick Start!!!:
Windows: Double-click mmj2\mmj2jar\mmj2.bat in Windows Explorer
Mac OS-X: Double-click mmj2\mmj2jar\MacMMJ2.command in Finder
BUT...WAIT!...before running mmj2, edit, if needed:
EDIT-->Windows mmj2\mmj2jar\RunParms.txt
using mmj2\mmj2jar\mmj2.bat
Notepad: mmj2\mmj2jar\mmj2PATutorial.bat
-->Mac OS-X mmj2\mmj2jar\RunParms.txt
using mmj2\mmj2jar\MacRunParmsPATutorial.txt
TextEdit: mmj2\mmj2jar\MacMMJ2.command
mmj2\mmj2jar\MacMMJ2PATutorial.command
(Double-click works well now because the new "mmj2 Fail Popup
Window" *not only* provides start-up and "fail" error
messages, but it also forces the Windows Command Prompt (Mac
OS-X utilities\terminal.app) window to stay open, which makes
it possible to see all of the mmj2 output about the error.)
-----------------------------------------------------------------
2. RunParms.txt and The mmj2.jar Command Line Arguments Revamped.
-----------------------------------------------------------------
The new release contains a serious revamp of both RunParms.txt
and the command line arguments for mmj2.jar. It has several
features of interest to the mmj2 user!
Unless you have been using your own modified version of mmj2.bat
and/or RunParms.txt you don't need to do anything special to
take advantage of these new features. Just use the new release
versions of mmj2.bat and RunParms.txt. (If you have your own
copies of these files they will -- most likely -- require minor
adjustments.)
In brief:
- New command line arguments specify data Paths for mmj2,
Metamath and the mmj2 Service feature. These make mmj2
easier to use in Windows, Mac OS-X and Linux environments
as well as making it easier to customize your mmj2
installation.
- MMJ2 Fail Popup Window which is displayed when startup or
premature termination errors in mmj2 are encountered.
Specify 'N' on the command line to disable this feature.
- The Command Line "Argument Option" report is extremely
useful during installation, customization and testing of
mmj2! It is output to Sysout at startup and provides an
audit trail of the program version and input command line
arguments. In the event of errors in the command line
arguments, the program tries to print as much as possible
of the Argument Option report, up to the point where a
command line argument error is detected -- and the last
line of the report printed will correspond to the invalid
argument!
- RunParms.txt is now maximally concise. This represents a
philosophical change. Previously, RunParms.txt contained
every possible RunParm command with the hard-coded default
specified (or asterisked-out). This was confusing and
unhelpful in two ways: 1) there are so many commands that
it was hard to see the important RunParms; and 2) at
startup mmj2 "echoes" each RunParm as it is executed and
this resulted in a bewildering barrage of output to
Sysout. The old version of RunParms.txt is now maintained
for reference purposes as RunParmsComplete.txt.
- All of the batch unit/volume regression tests have been
modified to take advantage of the Paths Enhancement.
Hardcoding of "C:\" exists only in the top level .bat
files -- and in a few cases "C:\" is coded for testing
purposes. These tests are now much more portable (to non-
Windows environments such as OS-X and Unix/Linux.)
Additional documentation at:
mmj2\doc\mmj2CommandLineArguments.html
------------------------------------------------------------
3. New! GMFF (Graphics Mode Formula Formatting) Enhancement.
------------------------------------------------------------
What is great about this feature is that it helps users see
right away what the Metamath ASCII formulas look like when
rendered in html (or Latex, etc.) Simply press Ctrl-1 (One) on
the Proof Assistant GUI screen to generate export file(s) via
GMFF -- use Alt-Tab to switch back and forth between the Proof
Assistant GUI and your browser window.
- NOTE: default setting for GMFF Export of a Proof Worksheet
or theorem is to create both .html and .althtml
versions (.gif and Unicode), and to write these
to fileS named "general.html":
- mmj2jar\gmff\html\general.html
and
- mmj2jar\gmff\althtml\general.html
IF you prefer to use export file names composed of
the Theorem Label + ".html" and/or to disable
either the html or the althtml versions,
THEN copy the "GMFFExportParms" RunParm lines from
mmj2jar\RunParmsComplete.txt to your version
of RunParms.txt.
*GMFFExportParms,althtml,ON,althtmldef,GMFF\althtml,.html,GMFF\models\althtml,A,ISO-8859-1,general
*GMFFExportParms,html,ON,htmldef,GMFF\html,.html,GMFF\models\html,A,ISO-8859-1,general
Then un-asterisk the commands, change "ON" to "OFF"
and/or erase "general" (leaving the option blank
allows the default to be used, which is to use Theorem
Label in the export file name):
GMFFExportParms,althtml,OFF,althtmldef,GMFF\althtml,.html,GMFF\models\althtml,A,ISO-8859-1,general
GMFFExportParms,html,ON,htmldef,GMFF\html,.html,GMFF\models\html,A,ISO-8859-1,
GMFF uses the typesetting information embedded in Metamath files
such as set.mm -- see Metamath Comment statement containing "$t"
-- to export files in other formats, such as as html and Latex.
At this time only html files have been generated but the GMFF
enhancement uses "Model" files in the mmj2 release to generate
its output and the types of files output are not restricted as
long as:
a) the output formula text is based on text strings, not parse
trees (as would be the case, for example, with MathML
output). And...
b) the structure of an individual export file can be made to fit
the structure of the available Model files. At this point
only Model "A" is available, but considerable effort was made
in programming to build in flexibility in the way a Model
file is used.
Modification of mmj2 code will be necessary if new Models are
required. Modification to use parse trees instead of formula
strings is doable but will require non-trivial changes. '
Refer to mmj2\doc\GMFFDoc\* for details.
----------------------------------------------
4. Incomplete Step Cursor Positioning Bug Fix.
----------------------------------------------
After Unification (Ctrl-U) the cursor was being moved in spite
of RunParm "ProofAsstIncompleteStepCursor,AsIs". And worse, the
ViewPort output lines were being scrolled so that the first line
on the screen matched the cursor location every time. Now, with
"AsIs" the cursor is repositioned only when there are proof
errors, or when unification is successful and a Metamath RPN
proof is generated.
See: mmj2/doc/IncompleteStepCursorPositioning.html
and mmj2/doc/ProofAsstGUICursorHandling.html
NOTE: The RunParm "ProofAsstIncompleteStepCursor" default
setting is now "AsIs" instead of "Last". If you prefer the
old setting you can customize RunParms.txt by adding:
ProofAsstIncompleteStepCursor,Last
just before the "RunProofAsstGUI" RunParm (the other
option is "First").
Documentation:
New:
mmj2\QuickStart.html
mmj2\doc\GMFFDoc\
mmj2\doc\GMFFDoc\GMFFFolders.txt
mmj2\doc\GMFFDoc\GMFFModels.txt
mmj2\doc\GMFFDoc\GMFFRunParms.txt
mmj2\doc\GMFFDoc\README.html
mmj2\doc\GMFFDoc\SampleRunParms.txt
mmj2\doc\GMFFDoc\GMFF.jpg
mmj2\doc\ReleaseNotes20111101.html
mmj2\mmj2jar\PATutorial\Page413.mmp
Changed:
mmj2\CHGLOG.TXT
mmj2\doc\BottomUpProving-ByNormMegill.html
mmj2\doc\FinalizeReleaseTodos.txt
mmj2\doc\mmj2CommandLineArguments.html
mmj2\doc\RegressionTestResults.txt
mmj2\doc\RunningTheMMJ2TestSuite.html
mmj2\INSTALL.html
mmj2\LicenseEnclosure.java
mmj2\mmj2.html
mmj2\README.html
mmj2\mmj2jar\PATutorial\Page101.mmp
mmj2\mmj2jar\PATutorial\Page102.mmp
mmj2\mmj2jar\PATutorial\Page103.mmp
mmj2\mmj2jar\PATutorial\Page201.mmp
mmj2\mmj2jar\PATutorial\Page202.mmp
mmj2\mmj2jar\PATutorial\Page203.mmp
mmj2\mmj2jar\PATutorial\Page204.mmp
mmj2\mmj2jar\PATutorial\Page301.mmp
mmj2\mmj2jar\PATutorial\Page302.mmp
mmj2\mmj2jar\PATutorial\Page303.mmp
mmj2\mmj2jar\PATutorial\Page304.mmp
mmj2\mmj2jar\PATutorial\Page401.mmp
mmj2\mmj2jar\PATutorial\Page402.mmp
mmj2\mmj2jar\PATutorial\Page403.mmp
mmj2\mmj2jar\PATutorial\Page404.mmp
mmj2\mmj2jar\PATutorial\Page405.mmp
mmj2\mmj2jar\PATutorial\Page406.mmp
mmj2\mmj2jar\PATutorial\Page407.mmp
mmj2\mmj2jar\PATutorial\Page408.mmp
mmj2\mmj2jar\PATutorial\Page409.mmp
mmj2\mmj2jar\PATutorial\Page410.mmp
mmj2\mmj2jar\PATutorial\Page411.mmp
mmj2\mmj2jar\PATutorial\Page412.mmp (all new content!!!)
Deleted:
mmj2\MacOSXIssues.txt
mmj2\mmj2jar\LICENSE.TXT
mmj2\mmj2jar\LicenseEnclosure.java
mmj2\mmj2jar\SunJavaTutorialLicense.html
Source Code:
New:
mmj2\src\mmj\gmff\GMFFUserTextEscapes.java
mmj2\src\mmj\gmff\MinCommentStmt.java
mmj2\src\mmj\gmff\GMFFException.java
mmj2\src\mmj\gmff\MinDerivationStep.java
mmj2\src\mmj\gmff\GMFFExportFile.java
mmj2\src\mmj\gmff\GMFFExporterTypesetDefs.java
mmj2\src\mmj\gmff\GMFFExportParms.java
mmj2\src\mmj\gmff\GMFFFileNotFoundException.java
mmj2\src\mmj\gmff\GMFFInputFile.java
mmj2\src\mmj\gmff\GMFFExporter.java
mmj2\src\mmj\gmff\GMFFMandatoryModelNotFoundException.java
mmj2\src\mmj\gmff\GMFFFolder.java
mmj2\src\mmj\gmff\GMFFFileFilter.java
mmj2\src\mmj\gmff\GMFFManager.java
mmj2\src\mmj\gmff\GMFFUserExportChoice.java
mmj2\src\mmj\gmff\ProofWorksheetCache.java
mmj2\src\mmj\gmff\GMFFConstants.java
mmj2\src\mmj\gmff\TypesetDefCommentParser.java
mmj2\src\mmj\gmff\EscapePair.java
mmj2\src\mmj\gmff\MinDistinctVariablesStmt.java
mmj2\src\mmj\gmff\MinHeaderStmt.java
mmj2\src\mmj\gmff\MinFooterStmt.java
mmj2\src\mmj\gmff\MinGeneratedProofStmt.java
mmj2\src\mmj\gmff\MinProofStepStmt.java
mmj2\src\mmj\gmff\MinProofWorkStmt.java
mmj2\src\mmj\gmff\MinProofWorksheet.java
mmj2\src\mmj\gmff\MinHypothesisStep.java
mmj2\src\mmj\gmff\ModelAExporter.java
mmj2\src\mmj\util\GMFFBoss.java
mmj2\src\mmj\util\MMJ2FailPopupWindow.java
mmj2\src\mmj\util\CommandLineArguments.java
mmj2\src\mmj\util\Paths.java
Changed:
mmj2\src\mmj\lang\Axiom.java
mmj2\src\mmj\lang\LangConstants.java
mmj2\src\mmj\lang\LogHyp.java
mmj2\src\mmj\lang\LogicalSystem.java
mmj2\src\mmj\lang\SystemLoader.java
mmj2\src\mmj\lang\Theorem.java
mmj2\src\mmj\mmio\IncludeFile.java
mmj2\src\mmj\mmio\MMIOConstants.java
mmj2\src\mmj\mmio\Statementizer.java
mmj2\src\mmj\mmio\Systemizer.java
mmj2\src\mmj\pa\AuxFrameGUI.java
mmj2\src\mmj\pa\PaConstants.java
mmj2\src\mmj\pa\ProofAsst.java
mmj2\src\mmj\pa\ProofAsstCursor.java
mmj2\src\mmj\pa\ProofAsstGUI.java
mmj2\src\mmj\pa\ProofWorksheet.java
mmj2\src\mmj\tl\MMTFolder.java
mmj2\src\mmj\tl\TlConstants.java
mmj2\src\mmj\tl\TlPreferences.java
mmj2\src\mmj\tmff\TMFFConstants.java
mmj2\src\mmj\tmff\TMFFPreferences.java
mmj2\src\mmj\util\BatchFramework.java
mmj2\src\mmj\util\BatchMMJ2.java
mmj2\src\mmj\util\Boss.java
mmj2\src\mmj\util\Dump.java
mmj2\src\mmj\util\LogicalSystemBoss.java
mmj2\src\mmj\util\OutputBoss.java
mmj2\src\mmj\util\ProofAsstBoss.java
mmj2\src\mmj\util\RunParmFile.java
mmj2\src\mmj\util\SvcBoss.java
mmj2\src\mmj\util\TheoremLoaderBoss.java
mmj2\src\mmj\util\UtilConstants.java
mmj2\src\mmj\verify\GrammarConstants.java
mmj2\src\mmj\verify\ProofConstants.java
mmj2\src\mmj\verify\VerifyProofs.java
Data:
New:
mmj2\data\gmfftest\
mmj2\data\gmfftest\19.21adv.mmp
mmj2\data\gmfftest\a2i.mmp
mmj2\data\gmfftest\pm2.38.mmp
mmj2\data\gmfftest\syllogism.mmp
mmj2\data\gmfftest\a1i.mmt
mmj2\data\gmfftest\models\althtml\AM-file0.txt
mmj2\data\gmfftest\models\althtml\AM-file2.txt
mmj2\data\gmfftest\models\althtml\AM-step0.txt
mmj2\data\gmfftest\models\althtml\AM-step1X.txt
mmj2\data\gmfftest\models\althtml\AM-step2.txt
mmj2\data\gmfftest\models\althtml\AM-step3X.txt
mmj2\data\gmfftest\models\althtml\AM-step4.txt
mmj2\data\gmfftest\models\althtml\AO-comment0.txt
mmj2\data\gmfftest\models\althtml\AO-comment1X.txt
mmj2\data\gmfftest\models\althtml\AO-comment2.txt
mmj2\data\gmfftest\models\althtml\AO-distinctvar0.txt
mmj2\data\gmfftest\models\althtml\AO-distinctvar1X.txt
mmj2\data\gmfftest\models\althtml\AO-distinctvar2.txt
mmj2\data\gmfftest\models\althtml\AO-distinctvar3X.txt
mmj2\data\gmfftest\models\althtml\AO-distinctvar4.txt
mmj2\data\gmfftest\models\althtml\AO-footer0.txt
mmj2\data\gmfftest\models\althtml\AO-genproof0.txt
mmj2\data\gmfftest\models\althtml\AO-genproof1X.txt
mmj2\data\gmfftest\models\althtml\AO-genproof2.txt
mmj2\data\gmfftest\models\althtml\AO-header0.txt
mmj2\data\gmfftest\models\althtml\AO-header1X.txt
mmj2\data\gmfftest\models\althtml\AO-header2.txt
mmj2\data\gmfftest\models\althtml\AO-header3X.txt
mmj2\data\gmfftest\models\althtml\AO-header4.txt
mmj2\data\gmfftest\models\althtml\AO-header5X.txt
mmj2\data\gmfftest\models\althtml\AO-header6.txt
mmj2\data\gmfftest\models\althtml\AO-header7.txt
mmj2\data\gmfftest\models\html\AM-file0.txt
mmj2\data\gmfftest\models\html\AM-file2.txt
mmj2\data\gmfftest\models\html\AM-step0.txt
mmj2\data\gmfftest\models\html\AM-step1X.txt
mmj2\data\gmfftest\models\html\AM-step2.txt
mmj2\data\gmfftest\models\html\AM-step3X.txt
mmj2\data\gmfftest\models\html\AM-step4.txt
mmj2\data\gmfftest\models\html\AO-comment0.txt
mmj2\data\gmfftest\models\html\AO-comment1X.txt
mmj2\data\gmfftest\models\html\AO-comment2.txt
mmj2\data\gmfftest\models\html\AO-distinctvar0.txt
mmj2\data\gmfftest\models\html\AO-distinctvar1X.txt
mmj2\data\gmfftest\models\html\AO-distinctvar2.txt
mmj2\data\gmfftest\models\html\AO-distinctvar3X.txt
mmj2\data\gmfftest\models\html\AO-distinctvar4.txt
mmj2\data\gmfftest\models\html\AO-footer0.txt
mmj2\data\gmfftest\models\html\AO-genproof0.txt
mmj2\data\gmfftest\models\html\AO-genproof1X.txt
mmj2\data\gmfftest\models\html\AO-genproof2.txt
mmj2\data\gmfftest\models\html\AO-header0.txt
mmj2\data\gmfftest\models\html\AO-header1X.txt
mmj2\data\gmfftest\models\html\AO-header2.txt
mmj2\data\gmfftest\models\html\AO-header3X.txt
mmj2\data\gmfftest\models\html\AO-header4.txt
mmj2\data\gmfftest\models\html\AO-header5X.txt
mmj2\data\gmfftest\models\html\AO-header6.txt
mmj2\data\gmfftest\models\html\AO-header7.txt
mmj2\data\gmfftest\myproofs\a2i.mmp
mmj2\data\mm\DollarT099.mm
mmj2\data\mm\DollarT046.mm
mmj2\data\mm\DollarT033.mm
mmj2\data\mm\big-unifier.mm
mmj2\data\mm\DollarT045.mm
mmj2\data\mm\DollarT032.mm
mmj2\data\mm\DollarT022.mm
mmj2\data\mm\DollarTPreface.mm
mmj2\data\mm\DollarTFirst100.mm
mmj2\data\mm\DollarT026.mm
mmj2\data\mm\DollarT025.mm
mmj2\data\mm\DollarT024.mm
mmj2\data\mm\DollarT023.mm
mmj2\data\mm\DollarT011.mm
mmj2\data\mm\DollarT098.mm
mmj2\data\mm\DollarT012.mm
mmj2\data\mm\DollarT021.mm
mmj2\data\mm\DollarT019.mm
mmj2\data\mm\DollarT020.mm
mmj2\data\mm\DollarT017.mm
mmj2\data\mm\DollarT015.mm
mmj2\data\mm\DollarT016.mm
mmj2\data\mm\DollarT018.mm
mmj2\data\mm\DollarT013.mm
mmj2\data\mm\DollarT014.mm
mmj2\data\mm\DollarT002.mm
mmj2\data\mm\DollarT010.mm
mmj2\data\mm\DollarT001.mm
mmj2\data\mm\DollarT008.mm
mmj2\data\mm\DollarT007.mm
mmj2\data\mm\DollarT009.mm
mmj2\data\mm\DollarT006.mm
mmj2\data\mm\DollarT005.mm
mmj2\data\mm\DollarT003.mm
mmj2\data\mm\DollarT004.mm
mmj2\data\mmp\tests\esnnei.mmp
mmj2\data\runparm\windows\VT2aPA002.txt
mmj2\data\runparm\windows\UT11GMFF01.txt
mmj2\data\runparm\windows\UT11GMFF02.txt
mmj2\data\runparm\windows\UT11GMFF03.txt
mmj2\data\runparm\windows\UT11GMFF04.txt
mmj2\data\runparm\windows\UT11GMFF05.txt
mmj2\data\runparm\windows\UT11GMFF06.txt
mmj2\data\runparm\windows\UT11GMFF07.txt
mmj2\data\runparm\windows\UT11GMFF08.txt
mmj2\mmj2jar\gmff\
mmj2\mmj2jar\gmff\althtml\general.html
mmj2\mmj2jar\gmff\althtml\langle.gif (from Metamath Symbols.zip)
mmj2\mmj2jar\gmff\althtml\rangle.gif (from Metamath Symbols.zip)
mmj2\mmj2jar\gmff\html\general.html
mmj2\mmj2jar\gmff\html\*.gif (from Metamath Symbols.zip)
mmj2\mmj2jar\gmff\models\althtml\AM-file0.txt
mmj2\mmj2jar\gmff\models\althtml\AM-file2.txt
mmj2\mmj2jar\gmff\models\althtml\AM-step0.txt
mmj2\mmj2jar\gmff\models\althtml\AM-step1X.txt
mmj2\mmj2jar\gmff\models\althtml\AM-step2.txt
mmj2\mmj2jar\gmff\models\althtml\AM-step3X.txt
mmj2\mmj2jar\gmff\models\althtml\AM-step4.txt
mmj2\mmj2jar\gmff\models\althtml\AO-comment0.txt
mmj2\mmj2jar\gmff\models\althtml\AO-comment1X.txt
mmj2\mmj2jar\gmff\models\althtml\AO-comment2.txt
mmj2\mmj2jar\gmff\models\althtml\AO-distinctvar0.txt
mmj2\mmj2jar\gmff\models\althtml\AO-distinctvar1X.txt
mmj2\mmj2jar\gmff\models\althtml\AO-distinctvar2.txt
mmj2\mmj2jar\gmff\models\althtml\AO-distinctvar3X.txt
mmj2\mmj2jar\gmff\models\althtml\AO-distinctvar4.txt
mmj2\mmj2jar\gmff\models\althtml\AO-footer0.txt
mmj2\mmj2jar\gmff\models\althtml\AO-genproof0.txt
mmj2\mmj2jar\gmff\models\althtml\AO-genproof1X.txt
mmj2\mmj2jar\gmff\models\althtml\AO-genproof2.txt
mmj2\mmj2jar\gmff\models\althtml\AO-header0.txt
mmj2\mmj2jar\gmff\models\althtml\AO-header1X.txt
mmj2\mmj2jar\gmff\models\althtml\AO-header2.txt
mmj2\mmj2jar\gmff\models\althtml\AO-header3X.txt
mmj2\mmj2jar\gmff\models\althtml\AO-header4.txt
mmj2\mmj2jar\gmff\models\althtml\AO-header5X.txt
mmj2\mmj2jar\gmff\models\althtml\AO-header6.txt
mmj2\mmj2jar\gmff\models\althtml\AO-header7.txt
mmj2\mmj2jar\gmff\models\html\AM-file0.txt
mmj2\mmj2jar\gmff\models\html\AM-file2.txt
mmj2\mmj2jar\gmff\models\html\AM-step0.txt
mmj2\mmj2jar\gmff\models\html\AM-step1X.txt
mmj2\mmj2jar\gmff\models\html\AM-step2.txt
mmj2\mmj2jar\gmff\models\html\AM-step3X.txt
mmj2\mmj2jar\gmff\models\html\AM-step4.txt
mmj2\mmj2jar\gmff\models\html\AO-comment0.txt
mmj2\mmj2jar\gmff\models\html\AO-comment1X.txt
mmj2\mmj2jar\gmff\models\html\AO-comment2.txt
mmj2\mmj2jar\gmff\models\html\AO-distinctvar0.txt
mmj2\mmj2jar\gmff\models\html\AO-distinctvar1X.txt
mmj2\mmj2jar\gmff\models\html\AO-distinctvar2.txt
mmj2\mmj2jar\gmff\models\html\AO-distinctvar3X.txt
mmj2\mmj2jar\gmff\models\html\AO-distinctvar4.txt
mmj2\mmj2jar\gmff\models\html\AO-footer0.txt
mmj2\mmj2jar\gmff\models\html\AO-genproof0.txt
mmj2\mmj2jar\gmff\models\html\AO-genproof1X.txt
mmj2\mmj2jar\gmff\models\html\AO-genproof2.txt
mmj2\mmj2jar\gmff\models\html\AO-header0.txt
mmj2\mmj2jar\gmff\models\html\AO-header1X.txt
mmj2\mmj2jar\gmff\models\html\AO-header2.txt
mmj2\mmj2jar\gmff\models\html\AO-header3X.txt
mmj2\mmj2jar\gmff\models\html\AO-header4.txt
mmj2\mmj2jar\gmff\models\html\AO-header5X.txt
mmj2\mmj2jar\gmff\models\html\AO-header6.txt
mmj2\mmj2jar\gmff\models\html\AO-header7.txt
mmj2\mmj2jar\MacRunParmsPATutorial.txt
mmj2\mmj2jar\RunParmsQL.txt
mmj2\mmj2jar\RunParmsComplete.txt
Changed:
mmj2\data\runparm\windows\PTAPGc7s1p146.txt
mmj2\data\runparm\windows\PTAPGc7s1p148.txt
mmj2\data\runparm\windows\PTAPGc7s2p160.txt
mmj2\data\runparm\windows\Sample001.txt
mmj2\data\runparm\windows\Sample002.txt
mmj2\data\runparm\windows\Sample003.txt
mmj2\data\runparm\windows\UT2PA001.txt
mmj2\data\runparm\windows\UT3LA001.txt
mmj2\data\runparm\windows\UT10001.txt
mmj2\data\runparm\windows\UT4001.txt
mmj2\data\runparm\windows\UT5001.txt
mmj2\data\runparm\windows\UT6001.txt
mmj2\data\runparm\windows\UT7001.txt
mmj2\data\runparm\windows\UT9001.txt
mmj2\data\runparm\windows\UT9002.txt
mmj2\data\runparm\windows\UT9003.txt
mmj2\data\runparm\windows\UT10002.txt
mmj2\data\runparm\windows\UT10003.txt
mmj2\data\runparm\windows\UT10021.txt
mmj2\data\runparm\windows\UT10022.txt
mmj2\data\runparm\windows\UT10023.txt
mmj2\data\runparm\windows\UT10031.txt
mmj2\data\runparm\windows\UT10032.txt
mmj2\data\runparm\windows\UT10033.txt
mmj2\data\runparm\windows\UT10041.txt
mmj2\data\runparm\windows\UT10042.txt
mmj2\data\runparm\windows\UT10043.txt
mmj2\data\runparm\windows\UT10051.txt
mmj2\data\runparm\windows\UT10052.txt
mmj2\data\runparm\windows\UT10053.txt
mmj2\data\runparm\windows\UT19100.txt
mmj2\data\runparm\windows\UTGR1c01.txt
mmj2\data\runparm\windows\UTGR1c02.txt
mmj2\data\runparm\windows\UTGR1c03.txt
mmj2\data\runparm\windows\UTGR1c04.txt
mmj2\data\runparm\windows\UTGR1c05.txt
mmj2\data\runparm\windows\UTGR1c05.txt
mmj2\data\runparm\windows\UTGR1c06.txt
mmj2\data\runparm\windows\UTIO1c01.txt
mmj2\data\runparm\windows\UTIO1c02.txt
mmj2\data\runparm\windows\UTIO1c03.txt
mmj2\data\runparm\windows\UTIO1c04.txt
mmj2\data\runparm\windows\UTIO1c05.txt
mmj2\data\runparm\windows\UTIO1c06.txt
mmj2\data\runparm\windows\UTIO1c07.txt
mmj2\data\runparm\windows\UTIO1c08.txt
mmj2\data\runparm\windows\UTLA1c01.txt
mmj2\data\runparm\windows\UTLA1c02.txt
mmj2\data\runparm\windows\UTPR1c01.txt
mmj2\data\runparm\windows\VT2bPA002.txt
mmj2\data\runparm\windows\VT2cPA002.txt
mmj2\data\runparm\windows\VT2dPA002.txt
mmj2\data\runparm\windows\VT2ePA002.txt
mmj2\doc\mmj2Service\TSvcCallbackCalleeRunParms.txt
mmj2\doc\mmj2Service\TSvcCallbackCallerRunParms.txt
mmj2\mmj2jar\AnnotatedRunParms.txt
mmj2\mmj2jar\RunParms.txt
mmj2\mmj2jar\RunParmsPATutorial.txt
mmj2\mmj2jar\RunParmsPeanoInfix.txt
mmj2\mmj2jar\setFirst100.mm
Deleted:
mmj2\data\runparm\windows\VT2PA002.txt
Object Code:
Changed:
mmj2jar\mmj2.jar
Other:
New:
mmj2\compile\mmj\gmff\gmffClasses.txt
mmj2\mmj2jar\CopySymbols.bat
mmj2\mmj2jar\MacMMJ2.command
mmj2\mmj2jar\MacMMJ2PATutorial.command
mmj2\mmj2jar\mmj2QL.bat
Changed:
mmj2\compile\mmj\util\utilClasses.txt
mmj2\compile\windows\CompMMJ.bat
mmj2\compile\windows\EraseMMJObjCode.bat
mmj2\compile\windows\mkjarargs.txt
mmj2\doc\mmj2Service\TjavacTCompilePaths.txt
mmj2\doc\mmj2Service\TSvcCallbackCallee.bat
mmj2\doc\mmj2Service\TSvcCallbackCaller.bat
mmj2\doc\windows\DocPackages.txt
mmj2\mmj2jar\mmj2.bat
mmj2\mmj2jar\mmj2PATutorial.bat
mmj2\mmj2jar\mmj2PeanoInfix.bat
mmj2\test\windows\RunBatchTest.bat
mmj2\test\windows\RunSample001.bat
mmj2\test\windows\RunSample002.bat
mmj2\test\windows\RunSample003.bat
mmj2\test\windows\RunUnitTest1.bat
mmj2\test\windows\RunUnitTest2.bat
mmj2\test\windows\RunUnitTest3.bat
mmj2\test\windows\RunUnitTest4.bat
mmj2\test\windows\RunUnitTest5.bat
mmj2\test\windows\RunUnitTest6.bat
mmj2\test\windows\RunUnitTest10.bat
mmj2\test\windows\RunUnitTest11.bat
mmj2\test\windows\RunUnitTest7.bat
mmj2\test\windows\RunUnitTest8.bat
mmj2\test\windows\RunUnitTest9.bat
mmj2\test\windows\RunUT1.bat
mmj2\test\windows\RunUT2.bat
mmj2\test\windows\RunUT3.bat
mmj2\test\windows\RunUT4.bat
mmj2\test\windows\RunUT5.bat
mmj2\test\windows\RunUT6.bat
mmj2\test\windows\RunUT7.bat
mmj2\test\windows\RunUT8.bat
mmj2\test\windows\RunUT10.bat
mmj2\test\windows\RunUT11.bat
mmj2\test\windows\RunUT9.bat
mmj2\test\windows\RunVolumeTest2a.bat
mmj2\test\windows\RunVolumeTest2b.bat
mmj2\test\windows\RunVolumeTest2c.bat
mmj2\test\windows\RunVolumeTest2d.bat
mmj2\test\windows\RunVolumeTest2e.bat
mmj2\test\windows\RunVT2a.bat
mmj2\test\windows\RunVT2b.bat
mmj2\test\windows\RunVT2c.bat
mmj2\test\windows\RunVT2d.bat
mmj2\test\windows\RunVT2e.bat
mmj2\test\windows\Sample001.bat
mmj2\test\windows\Sample002.bat
mmj2\test\windows\Sample003.bat
Deleted:
mmj2\test\windows\BatchMMJ2Sample001.bat
mmj2\test\windows\BatchMMJ2Sample002.bat
mmj2\test\windows\BatchMMJ2Sample003.bat
mmj2\test\windows\RunBatchFramework.bat
mmj2\test\windows\RunPAGUI.bat
mmj2\test\windows\RunUnitTest.bat
mmj2\test\windows\RunVolumeTest2.bat
mmj2\test\windows\RunVT2.bat
==================================================================
1-Jul-2011:
CHANGES:
This is a bug fix release.
1. Miscellaneous Bug Fixes:
a) Fixed a bug in the parser which prevented construction
of a parse tree for formulas consisting of just one
constant symbol (in addition to the type code constant.)
A "pre-parse" optimization handles "Named-Typed
Constants" which appear in only one syntax axiom. In
the special case where this was the only parsing action
required, EarleyParser.java sent the affected formulas
into the regular parsing algorithm following the pre-parse
optimization. Unfortunately. the regular algoritm didn't
"see" any parsing left to do and did not construct a
parse tree. An example formula is "trutru". The relevant
(defective) unit test .mm file has been updated.
2. Added mmj2\data\mm\RegressionTest1set.mm -- which is the
Feb. 25, 2008 version of set.mm. This archived copy of
set.mm is now used for running the MMJ2 Test Suite.
Due to label and symbol changes over time the mmj2 Test
Suite suffers entropic decay! So, a fixed copy of set.mm
will be used for regression testing (excluding the volume
tests).
3. Adjusted RunParm data and code defaults for the increased
sizes of SymTbl and StmtTbl (1500 and 45000 respectively.)
Also increased memory allocations in C:\mmj2\mmj2jar\mmj2.bat
as follows: Total Memory = 128M (was 64M),
Maximum Memory = 256M (was 128M).
4. Added mmj2\doc\RegressionTestResults.txt and
mmj2\doc\RegressionTestResultsForm.txt
Documents differences between the new and old software output
when run using mmj2\data\mm\RegressionTest1set.mm.
Documentation:
New:
mmj2\doc\RegressionTestResults.txt
mmj2\doc\RegressionTestResultsForm.txt
Changed:
CHGLOG.TXT
doc\FinalizeReleaseTodos.txt
INSTALL.html
mmj2.html
README.html
doc\RunningTheMMJ2TestSuite.html
Source Code:
New:
N/A
Changed:
src\mmj\lang\LangConstants.java
src\mmj\pa\PaConstants.java
src\mmj\verify\EarleyParser.java
Data:
New:
mmj2\data\mm\RegressionTest1set.mm
Changed:
mmj2\data\mm\UTGR1c02.mm
mmj2\mmj2jar\AnnotatedRunParms.txt
mmj2\mmj2jar\RunParms.txt
mmj2\mmj2jar\RunParmsPATutorial.txt
mmj2\mmj2jar\RunParmsPeanoInfix.txt
Object Code:
Changed:
mmj2jar\mmj2.jar
Other:
New:
N/A
Changed:
mmj2\mmj2jar\mmj2.bat
==================================================================
1-Aug-2008:
CHANGES:
This is a significant release.
1. The "mmj2 Service" feature adds a new "svc" package to
mmj2 and provides a foundation for other, non-mmj2
code to access Metamath data and mmj2 facilities. The
primary use envisioned is extracting Metamath data,
as the mmj2 Service feature provides easy access to
the critical ingredient: formula parse trees!
Access to mmj2 facilities is made available for "caller"
and "callee" programs. In both scenarios the BatchMMJ2
program is used to initialize mmj2 with a loaded .mm
file which is validated, parsed, etc. Callers actually
call BatchMMJ2 passing a "SvcCallback" object which is called
by mmj2 once initialization is complete (when the "SvcCall"
RunParm is processed.) "Callee" programs simply write
a class which implements the SvcCallback interface -- just
as "caller" programs do -- but instead of directly calling
BatchMMJ2, the user specifies the name of their SvcCallback-
implementing class via a "SvcCallback" RunParm.
Whether accessing mmj2 as a "caller" or "callee", complete
access to mmj2's main facilities is provided in the
SvcCallback.go interface method. The "go()" method is passed
references to the biggie mmj2 objects, including
ProofAsst, Grammar, VerifyProofs, etc.
Within the SvcCallback.go() method the user-code can
execute calls to mmj2 methods but must single-thread
the accesses as mmj2 is not, in general, written for
total multi-threaded access throughout (some code
could be multi-threaded but not all.)
When finished accessing the mmj2 Services, the user-code
simply needs to execute a "return" from the
SvcCallback.go() method.
New RunParms added to mmj2 for use with BatchMMJ2
(see mmj.util.SvcBoss) are SvcFolder, SvcCallbackClass,
SvcArg, and SvcCall. The SrvArg RunParm provides a
way for the user-code to obtain Key-Value parameter
pairs via the input RunParms file; they are loaded by
BatchMMJ2 (with minimal validation) into a HashMap
and passed via the SvcCallback.go() method. More
information about these new RunParms is provided in
the mmj2jar\AnnotatedRunParms.txt documentation file.
2. Modified function of the LoadComments RunParm to now
pick up the descriptive comment immediately preceding
axioms (including syntax). Previously, only theorem
($p) statement descriptions were picked up. (Small
changes to Statementizer.java and Systemizer.java :-)
3. Moved ProvableLogicStmtType and LogicStmtType RunParm
processing to LogicalSystemBoss from GrammarBoss.
These RunParms must be input prior to the LoadFile
RunParm (normally the default settings are used so
don't worry about this unless you are authoring an
unorthodox new logic system).
Also note that "LoadFile" does an implicit
"Clear" of old RunParms from other facilities such
as the Grammar, so it is generally necessary to
re-input RunParms which override defaults prior
to a 2nd LoadFile command (multiple LoadFile commands
are rare -- but two in a row can be used to load
two files together.)