-
Notifications
You must be signed in to change notification settings - Fork 25
/
AnnotatedRunParms.txt
2964 lines (2466 loc) · 131 KB
/
AnnotatedRunParms.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
LoadFile,set.mm
VerifyProof,*
Parse,*
ProofAsstUnifySearchExclude,biigb,xxxid,dummylink
ProofAsstProofFolder,myproofs
TheoremLoaderMMTFolder,myproofs
RunProofAsstGUI
AnnotatedRunParms.txt, revised 01-Aug-2008
==========================================
CONTENTS:
=========
- PREVIEW
- RUNPARM FILE PURPOSE
- RUNPARM FILE FORMAT -- KEY CONCEPTS
- RUNPARM FILE USAGE -- KEY CONCEPTS
- EXAMPLE RUNPARM FILE 1
- EXAMPLE RUNPARM FILE 2
- RUNPARM Commands for mmj.util.BatchMMJ.java
- RUNPARM Commands for mmj.util.OutputBoss.java
- RUNPARM Commands for mmj.lang.Messages.java
- RUNPARM Commands for mmj.util.Dump.java
- RUNPARM Commands for mmj.lang.SeqAssigner.java
- RUNPARM Commands for mmj.lang.BookManager.java
- RUNPARM Commands for mmj.lang.LogicalSystem.java
- RUNPARM Commands for mmj.mmio.Systemizer.java
- RUNPARM Commands for mmj.lang.ProofVerifier.java interface
- RUNPARM Commands for mmj.verify.Grammar.java
- RUNPARM Commands for mmj.lang.SyntaxVerifier.java interface
- RUNPARM Commands for mmj.lang.WorkVarManager.java
- RUNPARM Commands for mmj.tmff.Preferences.java
- RUNPARM Commands for mmj.pa.StepSelectorDialog.java
- RUNPARM Commands for mmj.pa.StepSelectorSearch.java
- RUNPARM Commands for mmj.tl.TheoremLoader.java
- RUNPARM Commands for mmj.svc.SvcCallback.java interface
- RUNPARM Commands for mmj.pa.ProofAsst.java
- RUNPARM Commands for mmj.util.GMFFBoss.java
------------------------------------------------------------------
PREVIEW:
========
This RunParm file contains documentation about RunParm files.
It is a perfectly valid RunParm file (see first 7 lines)
containing the standard executable RunParms needed to run the mmj2
Proof Assistant GUI using input Metamath .mm database file
set.mm (the default values are fine for the other RunParm
commands).
------------------------------------------------------------------
RUNPARM FILE PURPOSE:
=====================
The RunParm file provides mmj2 (via mmj.util.BatchMMJ2.java)
a command *language*. It is a language, even though it has
no branching or looping constructs; just sequential execution.
The RunParm language makes mmj2 easy to extend and enhance,
and of course, RunParms provide necessary flexibility so that
processing can be customized for different Metamath databases
as well as different users.
New features and new utilities can be added without impacting
existing features. As an example, the mmj2 Proof Assistant GUI
was one of the last features programmed. Implementing it
within the existing framework required just adding a few
new preference-setting RunParm commands and the executable
RunParm Command "RunProofAsstGUI". Likewise, in the future a
different Proof Assistant could be implemented without affecting
existing users by simply add RunParm Command "RunProofAsstGUIv2"!
------------------------------------------------------------------
RUNPARM FILE FORMAT -- KEY CONCEPTS:
====================================
- COMMENT LINES: contain an "*" (asterisk), " " (blank), or
"/" (slash) in column 1 of a RunParm line (like this line).
- RUNPARM COMMAND LINES (non-comment lines) consist of
- 1 Name field and
- 0 -> n Value fields
- Use "," (comma) as field separators and '"' (double-quote)
as field quoters (Use of Comma and Double-quote can be
changed via command line arguments to
mmj.util.BatchMMJ2.java)
- A null value field (zero length) is input thus: ",,"
or as a "," at the end of the RunParm line (followed by
a carriage return).
- RunParm names and values are not case-sensitive.
- Almost every RunParm value has a default which is designed
to be "optimal" for use with set.mm. If you accept the
defaults then do not even input the RunParm command. If
you do input put in the RunParm command then every
"required" value must be input too.
- NOTE: Use of '"' (double-quote) is only necessary if a
value contains a ',' (comma). Embedded spaces are
not a problem -- you don't need to quote values containing
spaces. And, you can even embed a '"' in an unquoted field
as long as the '"' is not the first or last character in the
field.
- EXAMPLES: each RunParm line below has SIX value fields!!!
* 1 2 3
*23456789012345678901234567890...
name1,value11,"value12",value13, " ,value15," , "
name2,,value22,,value24,,
------------------------------------------------------------------
RUNPARM FILE USAGE -- KEY CONCEPTS:
===================================
- The only mandatory RunParm Command is "LoadFile", and even that
is not required if no processing is desired. All other RunParms
have defaults or invoke processing that is optional. For
example proof verification is done only if RunParm Command
"VerifyProof" is input.
- There are two kinds of RunParm Commands: executable commands
and non-executable commands.
- Non-executable RunParm commands typically specify a
"preference" parameter or setting, such as "ProofAsstFontSize".
It is simplest to input non-executable RunParm lines first
in a RunParm file because these setting affect subsequent
processing and stay in effect until superceded or "Clear"ed.
- Executable RunParm commands are action-oriented verbs for mmj2.
The order of input of executable RunParm commands is important!
RunParms form a *language* for mmj2 and are processed in
sequence.
- These are the mmj2 Executable RunParm Commands:
Clear : Erases and deletes all previous
RunParms and processing state --
a clean start for new commands!
GarbageCollection : Runs Java "gc" to free up memory.
LoadFile : Loads 1 Metamath .mm Database file
(you can load more than one; order
is important; load all needed files
at once, before doing other
executable commands!)
VerifyProof : Runs mmj2 Proof Verification Engine
for one Theorem (label) or all ("*").
InitializeGrammar : Builds (or rebuilds) the Grammar
object and associated state variables
for the loaded Metamath .mm database
file(s). (Grammar initialization
happens automatically if this command
is not input and a "Parse" command
is input -- so "InitializeGrammar"
is not commonly used.
Parse : Build syntax Parse Tree for one
Metamath statement (label) or all
("*").
VerifyParse : Double-check accuracy of Parse(s)
for one statement (label) or all
("*") by converting Parse Trees into
RPN lists and feeding them into the
Proof Verification Engine (this is
cool but unnecessary unless you are
really paranoid!)
PrintSyntaxDetails : Dumps to the Sysout file or
PrintStream all information about
the Grammar object constructed for the
input Metamath .mm database file(s).
PrintStatementDetails : Dumps to the Sysout file or
Printstream -- in an ugly format --
almost all information about a single
Metamath statement (label) or all
statements ("*").
ProofAsstExportToFile : Exports one Theorem proof (label)
or all Theorems ("*") to a file in
Proof Worksheet format. Invalid or
incomplete proofs are not handled.
Other RunParm values available -- see
details below.
ProofAsstBatchTest : Reads and Unifies either one Theorem
Proof Worksheet (label) or all ("*").
Input is either memory (via an
in-memory "export") or an input file.
Other RunParm values available -- see
details below.
GMFFInitialize : Forces immediate initialization of the
GMFF facility, with an option to
"PrintTypesettingDefinitions".
GMFFExportFromFolder : Exports Proof Worksheeet files from a
folder, generating the designated type
of export file(s) -- normally html.
GMFFExportTheorem : Exports one or more theorems from the
loaded Logical System, generating the
designated type of export file(s) -- normally
html.
GMFFParseMetamathTypesetComment
: Parses a Metamath .mm file $t comment
statement, with an option to "PRINT".
StepSelectorBatchTest : Exercises the Unify\Step Selector Search
and selection logic for a single Proof
Worksheet in an input file. Also prints
various data items for use in regression
testing.
PreprocessRequestBatchTest
: Exercises the Unify/Erase And Rederive
Formulas code for a single Proof
Worksheet in an input file. Also prints
before/after images of the Proof Worksheet.
RunProofAsstGUI : Triggers the mmj2 Proof Assistant GUI.
Requires that the input Metamath .mm
database files be successfully parsed
prior to this command!
StartInstrumentationTimer
: Records current time and memory
stats for use with
StopInstrumentationTimer. Multiple
Instrumentation Timers can be used,
distinguished by "TimerID" strings
on the input RunParms.
StopInstrumentationTimer
: Records current time and memory
stats and produces and informational
message providing elapsed time
and memory utilization for the
given "TimerID".
LoadTheoremsFromMMTFolder
: The Theorem Loader function runs
after the "LoadFile" and updates
the Logical System in memory with
the contents of either one or all
".mmt" file-type theorem files in
the MMT Folder.
UnifyPlusStoreInMMTFolder
: Attempts unification of a Proof
Worksheet text file and stores the
theorem in the MMT Folder if
unification is successful.
UnifyPlusStoreInLogSysAndMMTFolder
: Attempts unification of a Proof
Worksheet text file, stores the
theorem in the MMT Folder if
unification is successful, and then
updates the Logical System in memory.
ExtractTheoremToMMTFolder
: Exports the theorem named by the input
label from the Logical System to the
MMT Folder, storing the theorem
as a Metamath .mm format file with
file type ".mmt".
SvcCall : Triggers a call by the mmj2 Service
feature to the user application. (This
is used when the mmj2 Service is being
used in "caller" and "callee" mode.)
------------------------------------------------------------------
EXAMPLE RUNPARM FILE 1
======================
* 1 2 3 4
*234567890123456789012345678901234567890
OutputVerbosity,0
MaxStatementPrintCount,99
Caption,Example #1
MaxErrorMessages,500
MaxInfoMessages,500
LoadFile,c:\metamath\set.mm
VerifyProof,*
Parse,*
PrintSyntaxDetails
PrintStatementDetails,*
------------------------------------------------------------------
EXAMPLE RUNPARM FILE 2
======================
* 1 2 3 4
*234567890123456789012345678901234567890
*CommentLine: Example #2 - default charsets="" and
* new/update parameter
OutputVerbosity,9999
SystemErrorFile,c:\my\mmjSyserrTest001.txt,new,""
SystemOutputFile,c:\my\mmjSysoutTest001.txt,new,""
MaxErrorMessages,15000
MaxInfoMessages,15000
SymbolTableInitialSize,1500
StatementTableInitialSize,45000
LoadEndpointStmtNbr,999999999
LoadEndpointStmtLabel,FermatsNextToLastTheorem
LoadComments,yes
LoadProofs,yes
ProvableLogicStmtType,|-
LogicStmtType,wff
BookManagerEnabled,yes
SeqAssignerIntervalSize,1000
GrammarAmbiguityEdits,basic
StatementAmbiguityEdits,basic
MaxStatementPrintCount,99999
Caption,Example #2
LoadFile,c:\metamath\set.mm
LoadFile,c:\my\MySetTheorems2.mm
*=== Optional Pre-Verification/Parse Theorem Loader stuff===
TheoremLoaderDjVarsOption,NoUpdate
TheoremLoaderMMTFolder,c:\my\proofs
TheoremLoaderAuditMessages,Yes
TheoremLoaderStoreFormulasAsIs,Yes
TheoremLoaderStoreMMIndentAmt,2
TheoremLoaderStoreMMRightCol,79
UnifyPlusStoreInMMTFolder,c:\myproofs\syl.mmp
UnifyPlusStoreInLogSysAndMMTFolder,c:\myproofs\syl.mmp
ExtractTheoremToMMTFolder,syl
LoadTheoremsFromMMTFolder,syl
LoadTheoremsFromMMTFolder,*
VerifyProof,*
Parse,*
VerifyParse,*
PrintSyntaxDetails
PrintStatementDetails,*
*===Work Variable stuff follows===
DefineWorkVarType,wff,&W,200
DefineWorkVarType,set,&S,200
DefineWorkVarType,class,&C,200
DeclareWorkVars
*===TMFF stuff follows===
TMFFDefineScheme,AlignVarDepth1,AlignColumn,1,Var,1,Var
TMFFDefineScheme,AlignVarDepth2,AlignColumn,2,Var,1,Var
TMFFDefineScheme,AlignVarDepth3,AlignColumn,3,Var,1,Var
TMFFDefineScheme,AlignVarDepth4,AlignColumn,4,Var,1,Var
TMFFDefineScheme,AlignVarDepth5,AlignColumn,5,Var,1,Var
TMFFDefineScheme,AlignVarDepth99,AlignColumn,99,Var,1,Var
TMFFDefineScheme,Flat,Flat
TMFFDefineScheme,PrefixDepth3,AlignColumn,3,Sym,2,Sym
TMFFDefineScheme,PostfixDepth3,AlignColumn,3,Sym,1,Sym
TMFFDefineScheme,TwoColumnAlignmentDepth1,TwoColumnAlignment,1
TMFFDefineScheme,TwoColumnAlignmentDepth2,TwoColumnAlignment,2
TMFFDefineScheme,TwoColumnAlignmentDepth3,TwoColumnAlignment,3
TMFFDefineScheme,TwoColumnAlignmentDepth4,TwoColumnAlignment,4
TMFFDefineScheme,TwoColumnAlignmentDepth5,TwoColumnAlignment,5
TMFFDefineScheme,TwoColumnAlignmentDepth99,TwoColumnAlignment,99
*Note: "Unformatted" and Format 0 are hardcoded --
*they cannot be redefined via RunParms.
TMFFDefineScheme,Unformatted,Unformatted
TMFFDefineFormat,1,AlignVarDepth1
TMFFDefineFormat,2,AlignVarDepth2
TMFFDefineFormat,3,AlignVarDepth3
TMFFDefineFormat,4,AlignVarDepth4
TMFFDefineFormat,5,AlignVarDepth5
TMFFDefineFormat,6,AlignVarDepth99
TMFFDefineFormat,7,Flat
TMFFDefineFormat,8,PrefixDepth3
TMFFDefineFormat,9,PostfixDepth3
TMFFDefineFormat,10,TwoColumnAlignmentDepth99
TMFFDefineFormat,11,TwoColumnAlignmentDepth1
TMFFDefineFormat,12,TwoColumnAlignmentDepth2
TMFFDefineFormat,13,TwoColumnAlignmentDepth3
TMFFDefineFormat,14,TwoColumnAlignmentDepth4
TMFFDefineFormat,15,TwoColumnAlignmentDepth5
TMFFUseFormat,13
* Default AltFormat = 7, Flat
TMFFAltFormat,7
* Default Indent amount = 0 columns per proof step level
TMFFUseIndent,0
* Default Alt Indent amount = 1 column per proof step level
TMFFAltIndent,1
*=== Proof Assistant Step Selector stuff follows ===
StepSelectorDialogPaneWidth,720
StepSelectorDialogPaneHeight,440
StepSelectorMaxResults,50
StepSelectorShowSubstitutions,true
*===Proof Assistant stuff follows===
ProofAsstFontSize,14
ProofAsstFontBold,yes
ProofAsstFontFamily,Monospaced
ProofAsstForegroundColorRGB,0,0,0
ProofAsstBackgroundColorRGB,255,255,255
ProofAsstFormulaLeftCol,20
ProofAsstFormulaRightCol,79
ProofAsstTextAtTop,yes
ProofAsstTextColumns,80
ProofAsstTextRows,21
ProofAsstErrorMessageColumns,80
ProofAsstErrorMessageRows,4
ProofAsstRPNProofLeftCol,6
ProofAsstRPNProofRightCol,79
ProofAsstIncompleteStepCursor,Last
ProofAsstOutputCursorInstrumentation,no
ProofAsstAutoReformat,yes
ProofAsstMaxUnifyAlternates,10
ProofAsstDummyVarPrefix,$
ProofAsstDefaultFileNameSuffix,.mmp
ProofAsstProofFolder,c:\my\proofs
RecheckProofAsstUsingProofVerifier,no
ProofAsstUndoRedoEnabled,yes
ProofAsstUnifySearchExclude,biigb,xxxid
ProofAsstExportToFile,*,c:\my\export.mmp,new,un-unified,Randomized,Print,NoDeriveFormulas
ProofAsstBatchTest,*,c:\my\export.mmp,un-unified,NotRandomized,NoPrint,DeriveFormulas,NoCompareDJs,NoUpdateDJs,NoAsciiRetest
StepSelectorBatchTest,c:\mmj2\UT7000.mmp,326,6
PreprocessRequestBatchTest,UT7001.mmp,EraseAndRederiveFormulas
ProofAsstStartupProofWorksheet,c:\mmj2\data\mmp\PATutorial\Page101.mmp
*=== Optional Pre-Proof Asst GUI Theorem Loader stuff===
TheoremLoaderDjVarsOption,NoUpdate
TheoremLoaderMMTFolder,c:\my\proofs
TheoremLoaderAuditMessages,Yes
TheoremLoaderStoreFormulasAsIs,Yes
TheoremLoaderStoreMMIndentAmt,2
TheoremLoaderStoreMMRightCol,79
UnifyPlusStoreInMMTFolder,syl.mmp
UnifyPlusStoreInLogSysAndMMTFolder,syl.mmp
ExtractTheoremToMMTFolder,syl
LoadTheoremsFromMMTFolder,syl
LoadTheoremsFromMMTFolder,*
*===Now run the Proof Asst GUI===
RunProofAsstGUI
*===Sample mmj2 Service RunParms, "callee" mode, commented out===
*SvcFolder,c:\my\java\test\mmj\svc
*SvcCallbackClass,TSvcCallbackCallee
*SvcArg,key1,value1
*SvcCall
*===Sample mmj2 Service RunParms, "caller" mode, commented out===
*SvcFolder,c:\my\java\test\mmj\svc
*SvcArg,key1,value1
*SvcCall
*===Now Load And Process Another .mm File===
clear
GarbageCollection
LoadFile,c:\metamath\ql.mm
VerifyProof,*
Parse,*
*RunProofAsstGUI
------------------------------------------------------------------
// ----------------------------------------------------------
// RUNPARM Commands for mmj.util.BatchMMJ.java
// ----------------------------------------------------------
Clear : - Optional.
- Default: existing state values retained.
- Clear loaded/derived mm data (files/grammar,etc) and
all RunParm values except for SystemErrorFile and
SystemOutputFile (you can re-enter these explicitly).
GarbageCollection
: - Optional
- Tells Java to free up unused memory items.
// ----------------------------------------------------------
// RUNPARM Commands for mmj.util.OutputBoss.java
// ----------------------------------------------------------
OutputVerbosity
: - Optional. May appear anywhere within the input
RunParm file, to take effect when the
next RunParm command is processed.
- Default = 9999 (highly verbose...)
- Value1 = verbosity number. Low values mean
fewer info/logging message type output.
Set to 0 to turn off logging of input
RunParm commands (set to 9 or higher
to see them.)
- Examples
* 1 2 3 4
*234567890123456789012345678901234567890
OutputVerbosity,99999
OutputVerbosity,0
SystemErrorFile
: - Optional
- Default = output to Command Window System.err
- Value1 = filename, absolute or relative path name.
- Value2 = "new" (default) or "update".
The system will NOT touch an existing file
unless given "update". If "new" is specified
an error is reported, halting processing ASAP
if the file already exists. If the file does
exist and "update" is specified, then it is
overwritten (not appended); however, no error
is reported for "update" if the file does not
already exist.
- Value3 = charset.
Input null ("") for system default charset.
* info on charsets:
file:///C:/Program%20Files/Java/jdk1.5.0_02/docs/api/java/nio/charset/Charset.html
* Valid charset names on all Java Platforms:
US-ASCII
ISO-8859-1
UTF-8
UTF-16BE
UTF-16LE
UTF-16
- Examples
* 1 2 3 4
*234567890123456789012345678901234567890
SystemErrorFile,c:\my\errtest.txt,new,"UTF-8"
SystemErrorFile,c:\my\errtest.txt,update,""
SystemOutputFile
: - Optional
- Default = output to Command Window System.out
- Value1 = filename, absolute or relative path name.
- Value2 = "new" (default) or "update".
The system will NOT touch an existing file
unless given "update". If "new" is specified
processing halts ASAP if the file already
exists. If the file does exist and "update"
is specified, then it is overwritten (not
appended); however, no error is reported for
"update" if the file does not already exist.
- Value3 = charset.
Input null ("") for system default charset.
* info on charsets:
file:///C:/Program%20Files/Java/jdk1.5.0_02/docs/api/java/nio/charset/Charset.html
* Valid charset names on all Java Platforms:
US-ASCII
ISO-8859-1
UTF-8
UTF-16BE
UTF-16LE
UTF-16
- Examples
* 1 2 3 4
*234567890123456789012345678901234567890
SystemOutputFile,c:\my\outtest.txt,new,"UTF-8"
SystemOutputFile,c:\my\outtest.txt,update,""
StartInstrumentationTimer
: - Optional. May appear anywhere within the input
RunParm file, to take effect immediately.
- Default = N/A
- Value1 = TimerID, a string (e.g. "VerifyProofs")
that identifies a particular Instrumentation
Timer. The value must match the TimerID
on the StopInstrumentationTimer RunParm.
Input strings are automatically trimmed
of left and right whitespace. A blank
or zero length String is acceptable.
If the input TimerID matches a previously
input TimerID, the existing Timer is
reset (i.e. a duplicate overwrites an
existing Instrumentation Timer).
- Examples
* 1 2 3 4
*234567890123456789012345678901234567890
StartInstrumentationTimer,Timer1
StartInstrumentationTimer,
StopInstrumentationTimer
: - Optional. Must follow a StartInstrumentationTimer
RunParm with matching TimerID. Produced
an informational message detailing
elapsed wall-clock time in milliseconds
and memory utilization. Multiple
"stops" can be input for a single TimerID.
- Default = N/A
- Value1 = TimerID, a string (e.g. "VerifyProofs")
that identifies a particular Instrumentation
Timer. The value must match the TimerID
on a StartInstrumentationTimer RunParm.
Input strings are automatically trimmed
of left and right whitespace. A blank
or zero length String is acceptable.
- Examples
* 1 2 3 4
*234567890123456789012345678901234567890
StopInstrumentationTimer,Timer1
StopInstrumentationTimer,
------------------------------------------------------------------
// ----------------------------------------------------------
// RUNPARM Commands for mmj.lang.Messages.java
// ----------------------------------------------------------
MaxErrorMessages
: - Optional
- Default = 15000
- Value1 = Positive integer. Specifies the maximum
number of error messages in mmj.lang.Messages.java.
If this number is exceeded, no additional error
messages are accumulated. (Individual processes may
print and clear the Messages object.)
- Example:
* 1 2 3 4
*234567890123456789012345678901234567890
MaxErrorMessages,15000
MaxInfoMessages
: - Optional
- Default = 15000
- Value1 = Positive integer. Specifies the maximum
number of info messages in mmj.lang.Messages.java.
If this number is exceeded, no additional info
messages are accumulated. (Individual processes may
print and clear the Messages object.)
- Example:
* 1 2 3 4
*234567890123456789012345678901234567890
MaxInfoMessages,15000
------------------------------------------------------------------
// ----------------------------------------------------------
// RUNPARM Commands for mmj.util.Dump.java
// ----------------------------------------------------------
MaxStatementPrintCount
: - Optional
- Default = 99999.
- Value1 = Positive Integer. Provides a governor for
the "PrintStatementDetails,*" RunParm command.
- Example:
* 1 2 3 4
*234567890123456789012345678901234567890
MaxStatementPrintCount,99999
Caption
: - Optional
- Default = " ".
- Value1 = Any character string. Will be printed on
output reports, like output from the
"PrintStatementDetails,*" RunParm command.
- Example:
* 1 2 3 4
*234567890123456789012345678901234567890
Caption,"set.mm Statement Dump"
PrintSyntaxDetails
: - Optional
- Default: syntax/grammar report not printed.
- Prints a report with a variety of information about
Syntax Axioms, the input grammar, etc.
- Example:
* 1 2 3 4
*234567890123456789012345678901234567890
PrintSyntaxDetails
PrintStatementDetails
: - Optional
- Default: statements not printed.
- Prints a report for one statement (label) or all ("*")
containing (almost) all information about a statement.
Note: if "Parse,*" has been run already then the TMFF
Format in use will be used to format the statement's
formula (otherwise the Default, Format "0" is used).
Note: at some point the computed data used in the
Proof Unifier may be printed -- interesting stuff. - Example:
- Value1: "*" (all) or a statement label (print 1)
- Examples:
* 1 2 3 4
*234567890123456789012345678901234567890
PrintSyntaxDetails,a1i
PrintSyntaxDetails,*
------------------------------------------------------------------
// ----------------------------------------------------------
// RUNPARM Commands for mmj.lang.SeqAssigner.java
// --------------------------------------------------------
SeqAssignerIntervalSize
: - Optional
- Default = 1000
- Specifies the numbering interval used to assign
sequence numbers to Metamath objects (MObj's).
Thus, during LoadFile processing MObj's are assigned
sequence numbers 1000, 2000, .... etc. if the
default interval size is not overridden. Note: the
interval size must be greater than one in order for
Theorem Loader to be able to insert loaded theorems
into the sequence numbering "gaps" left over from
the initial file load. The restriction on maximum
size is that the MObj.seq field is a 4 byte integer
with a maximum positive value of 2**31 - 1; thus,
with interval size = 1000, approximately 2 million
MObj.seq numbers could be assigned during the
initial file load.
- Value1 = Positive integer in the range of 1 through
10000 (inclusive).
- Example:
* 1 2 3 4
*234567890123456789012345678901234567890
SeqAssignerIntervalSize,1000
------------------------------------------------------------------
// ----------------------------------------------------------
// RUNPARM Commands for mmj.lang.BookManager.java
// ----------------------------------------------------------
BookManagerEnabled
: - Optional
- Default = 'yes', enabled.
- Value1 = "yes" (default) or "no". "yes" means that
the mmj2 "Book Manager" function keeps track of
the Metamath objects (MObj's) loaded into the Logical
System and assigns each MObj a Chapter, Section
and MObjNbr. RunParm commands are provided to print
BookManager data, but the primary use of the BookManager
data is likely to be in conjunction with the
"mmj2 Service" feature.
- Example:
* 1 2 3 4
*234567890123456789012345678901234567890
BookManagerEnabled,yes
------------------------------------------------------------------
// ----------------------------------------------------------
// RUNPARM Commands for mmj.lang.LogicalSystem.java
// ----------------------------------------------------------
SymbolTableInitialSize
: - Optional
- Default = 1500
- Value1 = Integer >= 10. Specifies the initial
size of the Symbol (hash) Table. A good size is about
1.5 times the number of constants and variables in
the input Metamath .mm database file(s).
- Example:
* 1 2 3 4
*234567890123456789012345678901234567890
SymbolTableInitialSize,600
StatementTableInitialSize
: - Optional
- Default = 45000
- Value1 = Integer >= 100. Specifies the initial
size of the Symbol (hash) Table. A good size is about
1.5 times the number of $f + $e + $a + $p statements
in the input Metamath .mm database file(s).
- Example:
* 1 2 3 4
*234567890123456789012345678901234567890
StatementTableInitialSize,30000
ProvableLogicStmtType
: - Optional
- Default = "|-"
- Value1 = A valid Constant defined in the input Metamath
.mm database file. By convention this occurs at the
first symbol of *logical* formulas and means "It is
provable that..." or "It is true that...", and then
the expression that follows must parse to a
be a LogicStmtType, which is normally "wff" (see
below.) In theory you can use a different symbol,
and it could even mean "It is provably false that ...",
but regardless, the ProvableLogicStmtType cannot
be used in an mmj2 Grammar anywhere other than the
first symbol of a logical formula (or an error message
is produced and the ProofAsstGUI will not run.)
Also, in theory there can be multiples of these, but
for simplicity mmj2 allows only 1.
- Example:
* 1 2 3 4
*234567890123456789012345678901234567890
ProvableLogicStmtType,|-
LogicStmtType
: - Optional
- Default = "wff"
- Value1 = A valid Constant defined in the input Metamath
.mm database file. By convention this occurs at the
first symbol of syntax axioms and means "well-formed
formula". mmj2 expects that statements with a
ProvableLogicStmtType (i.e. "|-") will parse to a
LogicStmtType (i.e. "wff") -- or else an error message
results and the ProofAsstGUI will not run. Also, in
theory there can be multiples of these, but for
simplicity mmj2 allows only 1.
- Example:
* 1 2 3 4
*234567890123456789012345678901234567890
LogicStmtType,wff
------------------------------------------------------------------
// ----------------------------------------------------------
// RUNPARM Commands for mmj.mmio.Systemizer.java
// ----------------------------------------------------------
LoadFile
: - Optional
- Default: no .mm data loaded.
- Multiple LoadFile commands may be input, however,
if two .mm files are to be processed together then
they should be loaded one after the other without
intervening executable RunParms -- otherwise, the
an "InitializeGrammar" command will be needed, along
with another "Parse,*" command. If two files are
to be processed separately, then use "Clear" and
re-input applicable RunParms for the 2nd file (you
might as well run two separate jobs in this case!)
- NOTE: VERY IMPORTANT...it is possible to load just
part of a .mm file using the "LoadEndpointStmtNbr"
and "LoadEndpointStmtNbr" commands, which can shorten
elapsed startup time and memory utilization by a lot.
If multiple .mm files are loaded then note that the
LoadEndpointStmtNbr are not cumulative. The count
starts over for each file. Also, you can code
"LoadEndpoint..." commands *between* "LoadFile"
commands.
- Value1 = filename, absolute or relative path name.
- Examples:
* 1 2 3 4
*234567890123456789012345678901234567890
LoadEndpointStmtNbr,100
LoadEndpointStmtLabel,mt2i
LoadFile,c:\metamath\set.mm
LoadEndpointStmtNbr,999
LoadFile,c:\metamath\myset.mm
LoadEndpointStmtNbr
: - Optional
- Default = No Limit.
- Value1 = Positive integer. Stop loading when given
statement sequence number is reached (exclusive
endpoint -- "101" means load 100 statements!)
- NOTE: VERY IMPORTANT...it is possible to load just
part of a .mm file using the "LoadEndpointStmtNbr"
and "LoadEndpointStmtNbr" commands, which can shorten
elapsed startup time and memory utilization by a lot.
- If multiple .mm files are loaded then note that the
LoadEndpointStmtNbr are NOT cumulative. The count
starts over for each file. Also, you can code
"LoadEndpointStmtNbr" commands *between* "LoadFile"
commands.
- A statement number endpoint can be input along with
"LoadInputStmtLabel". Whichever is satisfied first
terminates the load process.
- Example:
* 1 2 3 4
*234567890123456789012345678901234567890
LoadEndpointStmtNbr,100
LoadEndpointStmtLabel
: - Optional
- Default = No Limit.
- Value1 = Non-blank, non-null label string that need
no exist in the input file. Means stop loading input
the input .mm file(s) when the given statement label
is read (exclusive endpoint).
- NOTE: VERY IMPORTANT...it is possible to load just
part of a .mm file using the "LoadEndpointStmtNbr"
and "LoadEndpointStmtNbr" commands, which can shorten
elapsed startup time and memory utilization by a lot.
- A statement number endpoint can be input along with
"LoadInputStmtLabel". Whichever is satisfied first
terminates the load process.
- Example:
* 1 2 3 4
*234567890123456789012345678901234567890
LoadEndpointStmtLabel,mt2i
LoadComments
: - Optional
- Default = Load Comments!
- Value1 = "yes" (default) or "no". "yes" means load
Metamath comments into LogicalSystem as Descriptions
for the Math Objects ("MObj"s). The comment immediately
preceding the $p or $a statement is treated as the
description (must be the statement immediately prior to
the $p statement.)
- Only Axiom and Theorem descriptions are loaded now -- which
is for Proof Assistant and Theorem Loader -- but in
principle, the rest could be loaded in this manner,
except for $c and $v statements which often have the
description after the declaration.
- Example:
* 1 2 3 4
*234567890123456789012345678901234567890
LoadComments,yes
LoadProofs
: - Optional
- Default = Yes
- Value1 = "yes" (default) or "no". "yes" means load
Metamath proofs from the input .mm file into the
LogicalSystem as input. Otherwise empty proofs
are stored (single "?" step).
- Use "no" to reduce memory utilization and to
increase startup speed. If set to "no" then RunParm