forked from metamath/metamath-exe
-
Notifications
You must be signed in to change notification settings - Fork 0
/
metamath.c
7922 lines (7209 loc) · 323 KB
/
metamath.c
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
/*****************************************************************************/
/* Program name: metamath */
/* Copyright (C) 2020 NORMAN MEGILL nm at alum.mit.edu http://metamath.org */
/* License terms: GNU General Public License Version 2 or any later version */
/*****************************************************************************/
/*34567890123456 (79-character line to adjust editor window) 2345678901234567*/
/* Contributors: In the future, the license may be changed to the MIT license
or public domain. Therefore I request that any patches that are contributed
be free of copyright restrictions (i.e. public domain) in order to provide
this flexibility. Thank you. - NM */
/* Compilation instructions (gcc on Unix/Linus/Cygwin, lcc on Windows):
1. Make sure each .c file above is present in the compilation directory and
that each .c file (except metamath.c) has its corresponding .h file
present.
2. In the directory where these files are present, type:
gcc m*.c -o metamath
3. For full error checking, use:
gcc m*.c -o metamath -O2 -Wall -Wextra -Wmissing-prototypes \
-Wmissing-declarations -Wshadow -Wpointer-arith -Wcast-align \
-Wredundant-decls -Wnested-externs -Winline -Wno-long-long \
-Wconversion -Wstrict-prototypes -ansi -pedantic -Wunused-result
4. For faster runtime, use these gcc options:
gcc m*.c -o metamath -O3 -funroll-loops -finline-functions \
-fomit-frame-pointer -Wall -ansi -pedantic -fno-strict-overflow
5. The Windows version in the download was compiled with LCC-Win32:
lc -O m*.c -o metamath.exe
*/
#define MVERSION "0.181 12-Feb-2020"
/* 0.181 12-Feb-2020 nm (reported by David Starner) metamath.c - fix bug causing
new axioms to be used by MINIMIZE_WITH */
/* 0.180 10-Dec-2019 nm (bj 13-Sep-2019) mmpars.c - fix "line 0" in error msg
when label clashes with math symbol
8-Dec-2019 nm (bj 13-Oct-2019) mmhlpa.c - improve TOOLS> HELP INSERT, DELETE
8-Dec-2019 nm (bj 19-Sep-2019) mminou.c - change bug 1511 to error message
30-Nov-2019 nm (bj 12-Oct-2019) mmwtex.c - trigger Most Recent link on
mmtheorems.html when there is a mathbox statement (currently set.mm and
iset.mm).
30-Nov-2019 nm (bj 13-Sep-2019) mmhlpa.c - improve help for TOOLS> DELETE and
SUBSTITUTE.
30-Nov-2019 nm (bj 13-Sep-2019) mmwtex.c - change "htmlHome" in warnings to
"htmlhome". */
/* 0.179 29-Nov-2019 nm (bj 22-Sep-2019) metamath.c - MINIMIZE_WITH axiom trace
now starts from current NEW_PROOF instead of SAVEd proof.
23-Nov-2019 nm (bj 4-Oct-2019) metamath.c - make sure traceback flags are
cleared after MINIMIZE_WITH
20-Nov-2019 nm mmhlpa.c - add url pointer to HELP WRITE SOURCE /SPLIT
18-Nov-2019 nm mmhlpa.c - clarify HELP WRITE SOURCE /REWRAP
15-Oct-2019 nm mmdata.c - add bug check info for user
14-Oct-2019 nm mmcmds.c - use '|->' (not 'e.') as syntax hint for maps-to
14-Oct-2019 nm mmwtex.c - remove extraneous </TD> */
/* 0.178 10-Aug-2019 nm mminou.c - eliminate redundant fopen in fSafeOpen
6-Aug-2019 nm mmwtex.c,h, mmcmds.c - Add error check for >1 line
section name or missing closing decoration line in getSectionHeadings()
4-Aug-2019 nm mmhlpb.c, mmcmdl.c, metamath.c - Add /ALLOW_NEW_AXIOMS,
renamed /ALLOW_GROWTH to /MAY_GROW
17-Jul-2019 nm mmcmdl.c, mmhlpa.c, metamath.c - Add /NO_VERSIONING to
WRITE THEOREM_LIST
17-Jul-2019 nm metamath.c - Change line of dashes between SHOW STATEMENT
output from hardcoded 79 to current screenWidth */
/* 0.177 27-Apr-2019 nm mmcmds.c -"set" -> "setvar" in htmlAllowedSubst.
mmhlpb.c - fix typos in HELP IMPROVE. */
/* 0.176 25-Mar-2019 nm metamath.c mmcmds.h mmcmds.c mmcmdl.c mmhlpb.c -
add /TOP_DATE_SKIP to VERIFY MARKUP */
/* 0.175 8-Mar-2019 nm mmvstr.c - eliminate warning in gcc 8.3 (patch
provided by David Starner) */
/* 0.174 22-Feb-2019 nm mmwtex.c - fix erroneous warning when using "[["
bracket escape in comment */
/* 0.173 3-Feb-2019 nm mmwtex.c - fix infinite loop when "[" was the first
character in a comment */
/* 0.172 25-Jan-2019 nm mmwtex.c - comment out bug 2343 trap (not a bug) */
/* 0.171 13-Dec-2018 nm metamath.c, mmcmdl.c, mmhlpa.c, mmcmds.c,h, mmwtex.c,h
- add fine-grained qualfiers to MARKUP command */
/* 0.170 12-Dec-2018 nm mmwtex.c - restore line accidentally deleted in 0.169 */
/* 0.169 10-Dec-2018 nm metamath.c, mmcmds.c,h, mmcmdl.c, mmpars.c, mmhlpa.c,
mmwtex.c - Add MARKUP command.
9-Dec-2018 nm mmwtex.c - escape literal "[" with "[[" in comments. */
/* 0.168 8-Dec-2018 nm metamath.c - validate that /NO_REPEATED_STEPS is used
only with /LEMMON.
8-Dec-2018 nm mmcmds.c - fix bug #256 reported by Jim Kingdon
(https://github.com/metamath/set.mm/issues/497). */
/* 0.167 13-Nov-2018 nm mmcmds.c - SHOW TRACE_BACK .../COUNT now uses proof
the way it's stored (previously, it always uncompressed the proof). The
new step count (for compressed proofs) corresponds to the step count the
user would see on the web pages.
12-Nov-2018 nm mmcmds.c - added unlimited precision arithmetic
for SHOW TRACE_BACK .../COUNT/ESSENTIAL */
/* 0.166 31-Oct-2018 nm mmwtex.c - workaround Chrome anchor bug
30-Oct-2018 nm mmcmds.c - put "This theorem is referenced by" after
axioms and definitions used in HTML; use "(None)" instead of suppressing
line if nothing is referenced */
/* 0.165 20-Oct-2018 nm mmwtex.c - added ~ mmtheorems#abc type anchor
in TOC details. mmwtex.c - fix bug (reported by Benoit Jubin) that
changes "_" in labels to subscript. mmcmdl.c - remove unused COMPLETE
qualifier from SHOW PROOF. mmwtex.c - enhance special cases of web page
spacing identified by Benoit Jubin */
/* 0.164 5-Sep-2018 nm mmwtex.c, mmhlpb.c - added NOTE to bib keywords
14-Aug-2018 nm metamath.c - added defaultScrollMode to prevent
SET SCROLL CONTINUOUS from reverting to PROMPTED after a SUBMIT command */
/* 0.163 4-Aug-2018 nm mmwtex.c - removed 2nd "sandbox:bighdr" anchor
in mmtheorems.html; removed Firefox and IE references; changed breadcrumb
font to be consistent with other pages; put asterisk next to TOC entries
that have associated comments */
/* FOR FUTURE REFERENCE: search for "Thierry" in mmwtex.c to modify the link
to tirix.org structured proof site */
/* 0.162-thierry 3-Jun-2018 nm mmwtex.c - add link to tirix.org structured
proofs */
/* 0.162 3-Jun-2018 nm mmpars.c - re-enabled error check for $c not in
outermost scope. mmhlpa.c mmhlpb.c- improve some help messages.
mmwtex.c - added "Observation", "Proof", and "Statement" keywords for
WRITE BIBLIOGRAPHY */
/* 0.161 2-Feb-2018 nm mmpars.c,h mmcmds.c mmwtex.c - fix wrong file name
and line number in error messages */
/* 0.160 24-Jan-2018 nm mmpars.c - fix bug introduced in version 0.158 */
/* 0.159 23-Jan-2018 nm mmpars.c - fix crash due to missing include file */
/* 0.158 22-Jan-2018 nm mminou.c - strip CRs from Windows SUBMIT files
run on Linux */
/* 0.157 15-Jan-2018 nm Major rewrite of READ-related functions.
Added HELP MARKUP.
9-Jan-2018 nm Track line numbers for error messages in included files
1-Jan-2018 nm Changed HOME_DIRECTORY to ROOT_DIRECTORY
31-Dec-2017 nm metamath.c mmcmdl.c,h mmpars.c,h mmcmds.c,h mminou.c,h
mmwtex.c mmhlpb.c mmdata.h - add virtual includes "$( Begin $[...$] $)",
$( End $[...$] $)", "$( Skip $[...$] $)" */
/* 0.156 8-Dec-2017 nm mmwtex.c - fix bug that incorrectly gave "verify markup"
errors when there was a mathbox statement without an "extended" section */
/* 0.155 8-Oct-2017 nm mmcmdl.c - restore accidentally removed HELP HTML;
mmhlpb.c mmwtex.c mmwtex.h,c mmcmds.c metamath.c - improve HELP and make
other cosmetic changes per Benoit Jubin's suggestions */
/* 0.154 2-Oct-2017 nm mmunif.h,c mmcmds.c - add 2 more variables to ERASE;
metamath.c mmcmdl.c - remove obsolete OPEN/CLOSE HTML; mmhlpa.c mmhlpb.c -
fix typos reported by Benoit Jubin */
/* 0.153 1-Oct-2017 nm mmunif.c,h mmcmds.c - Re-initialize internal nmbrStrings
in unify() after 'erase' command reported by Benoit Jubin */
/* 0.152 26-Sep-2017 nm mmcmds.c - change default links from mpegif to mpeuni;
metamath.c - enforce minimum screen width = 3 to prevent crash reported
by Benoit Jubin */
/* 0.151 20-Sep-2017 nm mmwtex.c - better matching to insert space between
A and y in "E. x e. ran A y R x" to prevent spurious spaces in thms rncoeq,
dfiun3g as reported by Benoit Jubin */
/* 0.150 26-Aug-2017 nm mmcmds.c,mmwtex.h - fix hyperlink for Distinct variable
etc. lists so that it will point to mmset.html on other Explorers like NF.
Move the "Dummy variables..." to print after the "Proof of Theorem..."
line. */
/* 0.149 21-Aug-2017 nm mmwtex.c,h mmcmds.c mmhlpb.c - add a subsubsection
"tiny" header with separator "-.-." to table of contents and theorem list;
see HELP WRITE THEOREM_LIST
21-Aug-2017 nm mmcmds.c - remove bug check 255
19-Aug-2017 nm mmcmds.c - change mmset.html links to
../mpeuni/mmset.html so they will work in NF Explorer etc. */
/* 0.148 14-Aug-2017 nm mmcmds.c - hyperlink "Dummy variable(s)" */
/* 0.147 13-Aug-2017 nm mmcmds.c,h - add "Dummy variable x is distinct from all
other variables." to proof web page */
/* 0.146 26-Jun-2017 nm mmwtex.c - fix handling of local labels in
'show proof.../tex' (bug 2341 reported by Eric Parfitt) */
/* 0.145 16-Jun-2017 nm metamath.c mmpars.c - fix bug 1741 during
MINIMIZE_WITH; mmpfas.c - make duplicate bug numbers unique; mmhlpa.c
mmhlpb.c - adjust to prevent lcc compiler "Function too big for the
optimizer"
29-May-2017 nm mmwtex.c mmhlpa.c - take out extraneous <HTML>...</HTML>
markup tags in HTML output so w3c validator will pass */
/* 0.144 15-May-2017 nm metamath.c mmcmds.c - add "(Revised by..." tag for
conversion of legacy .mm's if there is a 2nd date under the proof */
/* 0.143 14-May-2017 nm metamath.c mmdata.c,h mmcmdl.c mmcmds.c mmhlpb.c -
added SET CONTRIBUTOR; for missing "(Contributed by..." use date
below proof if it exists, otherwise use today's date, in order to update
old .mm files.
14-May-2017 Ari Ferrera - mmcmds.c - fix memory leaks in ERASE */
/* 0.142 12-May-2017 nm metamath.c mmdata.c,h mmcmds.c - added
"#define DATE_BELOW_PROOF" in mmdata.h that if uncommented, will enable
use of the (soon-to-be obsolete) date below the proof
4-May-2017 Ari Ferrera - mmcmds.c metamath.c mmdata.c mmcmdl.c
mminou.c mminou.h mmcmdl.h mmdata.h - fixed memory leaks and warnings
found by valgrind.
3-May-2017 nm - metamath.c mmdata.c,h mmcmds.c,h mmpars.c,h mmhlpb.c
mmcmdl.c mmwtex.c - added xxChanged flags to statement structure so
that any part of the source can be changed; removed /CLEAN qualifier
of WRITE SOURCE; automatically put "(Contributed by ?who?..." during
SAVE NEW_PROOF or SAVE PROOF when it is missing; more VERIFY MARKUP
checking. */
/* 0.141 2-May-2017 nm mmdata.c, metamath.c, mmcmds.c, mmhlpb.c - use
getContrib() date for WRITE RECENT instead of date below proof. This lets
us list recent $a's as well as $p's. Also, add caching to getContrib() for
speedup. */
/* 0.140 1-May-2017 nm mmwtex.c, mmcmds.c, metamath.c - fix some LaTeX issues
reported by Ari Ferrera */
/* 0.139 2-Jan-2017 nm metamath.c - print only one line for
'save proof * /compressed/fast' */
/* 0.138 26-Dec-2016 nm mmwtex.c - remove extraneous </TD> causing w3c
validation failure; put space after 1st x in "F/ x x = x";
mmcmds.c - added checking for lines > 79 chars in VERIFY MARKUP;
mmcmds.c, mmcmdl.c, metamath.c, mmhlpb.c, mmcmds.h - added /VERBOSE to
VERIFY MARKUP */
/* 0.137 20-Dec-2016 nm mmcmds.c - check ax-XXX $a vs axXXX $p label convention
in 'verify markup'
18-Dec-2016 nm mmwtex.c, mmpars.c, mmdata.h - use true "header area"
between successive $a/$p for getSectionHeadings() mmcmds.c - add
header comment checking
13-Dec-2016 nm mmdata.c,h - enhanced compareDates() to treat empty string as
older date.
13-Dec-2016 nm metamath.c, mmcmds.c - moved mm* and Microsoft illegal file
name label check to verifyMarkup() (the VERIFY MARKUP command) instead of
checking on READ; added check of set.mm Version date to verifyMarkup().
13-Dec-2016 nm mmwtex.c,h - don't treat bracketed description text with
space as a bib label; add labelMatch parameter to writeBibliography() */
/* 0.136 10-Oct-2016 mminou.c - fix resource leak bug reported by David
Binderman */
/* 0.135 11-Sep-2016, 14-Sep-2016 metamath.c, mmpfas.c,h, mmdata.c,h,
mmpars.c,h mmcmds.c, mmcmdl.c, mmhlpb.c - added EXPAND command */
/* 0.134 16-Aug-2016 mmwtex.c - added breadcrumbs to theorem pages;
metamath.c, mmcmdl.c, mmhlpb.c, mminou.c,.h - added /TIME to SAVE PROOF,
SHOW STATEMENT.../[ALT}HTML, MINIMIZE_WITH */
/* 0.133 13-Aug-2016 mmwtex.c - improve mobile display with <head> tag
mmpars.c - use updated Macintosh information */
/* 0.132 10-Jul-2016 metamath.c, mmcmdl.c, mmcmds.c,.h, mmdata.c,.h, mmhlpb.c,
mmpfas.c - change "restricted" to "discouraged" to match set.mm markup
tags; add SET DISCOURAGEMENT OFF|ON (default ON) to turn off blocking for
convenience of advanced users
6-Jul-2016 metamath.c - add "(void)" in front of "system(...)" to
suppress -Wunused-result warning */
/* 0.131 10-Jun-2016 mminou.c - reverted change of 22-May-2016 because
'minimize_with' depends on error message in string to prevent DV violations.
Todo: write a DV-checking routine for 'minimize_with', then revert
the 22-May-2016 fix for bug 126 (which only occurs when writing web
pages for .mm file with errors).
9-Jun-2016 mmcmdl.c, metamath.c - added _EXIT_PA for use with
scripts that will give an error message outside of MM-PA> rather
than exiting metamath */
/* 0.130 25-May-2016 mmpars.c - workaround clang warning about j = j;
mmvstr.c - workaround gcc -Wstrict-overflow warning */
/* 0.129 24-May-2016 mmdata.c - fix bug 1393 */
/* 0.128 22-May-2016 mminou.c - fixed error message going to html page
instead of to screen, triggering bug 126. */
/* 0.127 10-May-2016 metamath.c, mmcmdl.c, mmhlpb.c - added /OVERRIDE to
PROVE */
/* 0.126 3-May-2016 metamath.c, mmdata.h, mmdata.c, mmcmds.h, mmcmds.c,
mmcmdl.c, mmhlpb.c, mmpars.c - added getMarkupFlag() in mmdata.c;
Added /OVERRIDE added to ASSIGN, REPLACE, IMPROVE, MINIMIZE_WITH,
SAVE NEW_PROOF; PROVE gives warning about SAVE NEW_PROOF for locked
proof. Added SHOW RESTRICTED command.
3-May-2016 m*.c - fix numerous conversion warnings provided by gcc 5.3.0 */
/* 0.125 10-Mar-2016 mmpars.c - fixed bug parsing /EXPLICIT/PACKED format
8-Mar-2016 nm mmdata.c - added "#nnn" to SHOW STATEMENT etc. to reference
statement number e.g. SHOW STATEMENT #58 shows a1i in set.mm.
7-Mar-2016 nm mmwtex.c - added space between } and { in HTML output
6-Mar-2016 nm mmpars.c - disabled wrapping of formula lines in
WRITE SOURCE.../REWRAP
2-Mar-2016 nm metamat.c, mmcmdl.c, mmhlpb.c - added /FAST to
SAVE PROOF, SHOW PROOF */
/* 0.123 25-Jan-2016 nm mmpars.c, mmdata.h, mmdata.c, mmpfas.c, mmcmds.,
metamath.c, mmcmdl.c, mmwtex.c - unlocked SHOW PROOF.../PACKED,
added SHOW PROOF.../EXPLICIT */
/* 0.122 14-Jan-2016 nm metamath.c, mmcmds.c, mmwtex.c, mmwtex.h - surrounded
math HTML output with "<SPAN [htmlFont]>...</SPAN>; added htmlcss and
htmlfont $t commands
10-Jan-2016 nm mmwtex.c - delete duplicate -4px style; metamath.c -
add after char on mmascii.html
3-Jan-2016 nm mmwtex.c - fix bug when doing SHOW STATEMENT * /ALT_HTML after
VERIFY MARKUP */
/* 0.121 17-Nov-2015 nm metamath.c, mmcmdl.h, mmcmdl.c, mmcmds.h, mmcmds.c,
mmwtex.h, mmwtex.c, mmdata.h, mmdata.c -
1. Moved WRITE BIBLIOGRAPHY code from metamath.c to its own function in
mmwtex.c; moved qsortStringCmp() from metamath.c to mmdata.c
2. Added $t, comment markup, and bibliography checking to VERIFY MARKUP
3. Added options to bug() bug-check interception to select aborting,
stepping to next bug, or ignoring subsequent bugs
4. SHOW STATEMENT can now use both /HTML and /ALT_HTML in same session
5. Added /HTML, /ALT_HTML to WRITE THEOREM_LIST and
WRITE RECENT_ADDITIONS */
/* 0.120 7-Nov-2015 nm metamath.c, mmcmdl.c, mmpars.c - add VERIFY MARKUP
4-Nov-2015 nm metamath.c, mmcmds.c/h, mmdata.c/h - move getDescription,
getSourceIndentation from mmcmds.c to mmdata.c.
metamath.c, mmdata.c - add and call parseDate() instead of in-line
code; add getContrib(), getProofDate(), buildDate(), compareDates(). */
/* 0.119 18-Oct-2015 nm mmwtex.c - add summary TOC to Theorem List; improve
math symbol GIF image alignment
2-Oct-2015 nm metamath.c, mmpfas.c, mmwtex.c - fix miscellaneous small
bugs or quirks */
/* 0.118 18-Jul-2015 nm metamath.c, mmcmds.h, mmcmds.c, mmcmdl.c, mmhlpb.h,
mmhlpb.c - added /TO qualifier to SHOW TRACE_BACK. See
HELP SHOW TRACE_BACK. */
/* 0.117 30-May-2015
1. nm mmwtex.c - move <A NAME... tag to math symbol cell in proof pages so
hyperlink will jump to top of cell (reported by Alan Sare)
2. daw mmpfas.c - add INLINE speedup if compiler permits
3. nm metamath.c, mminou.c, mmwtex.c, mmpfas.c - fix clang -Wall warnings
(reported by David A. Wheeler) */
/* 0.116 9-May-2015 nm mmwtex.c - adjust paragraph break in 'write th';
Statement List renamed Theorem List; prevent space in after paragraph
in Theorem List; remove stray "("; put header and header comment
in same table cell; fix <TITLE> of Theorem List pages */
/* 0.115 8-May-2015 nm mmwtex.c - added section header comments to
WRITE THEOREM_LIST and broke out Table of Contents page
24-Apr-2015 nm metamath.c - add # bytes to end of "---Clip out the proof";
reverted to no blank lines there (see 0.113 item 3) */
/* 0.114 22-Apr-2015 nm mmcmds.c - put [-1], [-2],... offsets on 'show
new_proof/unknown' */
/* 0.113 19-Apr-2015 so, nm metamath.c, mmdata.c
1. SHOW LABEL % will show statements with changed proofs
2. SHOW LABEL = will show the statement being proved in MM-PA
3. Added blank lines before, after "---------Clip out the proof" proof
4. Generate date only if the proof is complete */
/* 0.112 15-Apr-2015 nm metamath.c - fix bug 1121 (reported by S. O'Rear);
mwtex.c - add "img { margin-bottom: -4px }" to CSS to align symbol GIFs;
mwtex.c - remove some hard coding for set.mm, for use with new nf.mm;
metamath.c - fix comment parsing in WRITE BIBLIOGRAPHY to ignore
math symbols */
/* 0.111 22-Nov-2014 nm metamath.c, mmcmds.c, mmcmdl.c, mmhlpb.c - added
/NO_NEW_AXIOMS_FROM qualifier to MINIMIZE_WITH; see HELP MINIMIZE_WITH.
21-Nov-2014 Stepan O'Rear mmdata.c, mmhlpb.c - added ~ label range specifier
to wildcards; see HELP SEARCH */
/* 0.110 2-Nov-2014 nm mmcmds.c - fixed bug 1114 (reported by Stefan O'Rear);
metamath.c, mmhlpb.c - added "SHOW STATEMENT =" to show the statement
being proved in MM-PA */
/* 0.109 20-Aug-2014 nm mmwtex.c - fix corrupted HTML caused by misinterpreting
math symbols as comment markup (math symbols with _ [ ] or ~). Also,
allow https:// as well as http:// in ~ label markup.
11-Jul-2014 wl mmdata.c - fix obscure crash in debugging mode db9 */
/* 0.108 25-Jun-2014 nm
(1) metamath.c, mmcmdl.c, mmhlpb.c - MINIMIZE_WITH now checks the size
of the compressed proof, prevents $d violations, and tries forward and
reverse statment scanning order; /NO_DISTINCT, /BRIEF, /REVERSE
qualifiers were removed.
(2) mminou.c - prevent hard breaks (in the middle of a word) in too-long
lines (e.g. long URLs) in WRITE SOURCE .../REWRAP; just overflow the
screen width instead.
(3) mmpfas.c - fixed memory leak in replaceStatement()
(4) mmpfas.c - suppress inf. growth with MINIMIZE_WITH idi/ALLOW_GROWTH */
/* 0.107 21-Jun-2014 nm metamath.c, mmcmdl.c, mmhlpb.c - added /SIZE qualifier
to SHOW PROOF; added SHOW ELAPSED_TIME; mmwtex.c - reformatted WRITE
THEOREM_LIST output; now "$(", newline, "######" starts a "part" */
/* 0.106 30-Mar-2014 nm mmwtex.c - fix bug introduced by 0.105 that disabled
hyperlinks on literature refs in HTML comment. metamath.c - improve
messages */
/* 0.105 15-Feb-2014 nm mmwtex.c - prevented illegal LaTeX output for certain
special characters in comments. */
/* 0.104 14-Feb-2014 nm mmwtex.c - fixed bug 2312, mmcmds.c - enhanced ASSIGN
error message. */
/* 0.103 4-Jan-2014 nm mmcmds.c,h - added "Allowed substitution hints" below
the "Distinct variable groups" list on generated web pages
mmwtex.c - added "*" to indicate DV's occur in Statement List entries. */
/* 0.102 2-Jan-2014 nm mminou.c - made compressed proof line wrapping more
uniform at start of compressed part of proof */
/* 0.101 27-Dec-2013 nm mmdata.h,c, mminou.c, mmcmdl.c, mmhlpb.c, mmvstr.c -
Improved storage efficiency of /COMPRESSED proofs (but with 20% slower run
time); added /OLD_COMPRESSION to specify old algorithm; removed end-of-line
space after label list in old algorithm; fixed linput() bug */
/* 0.100 30-Nov-2013 nm mmpfas.c - reversed statement scan order in
proveFloating(), to speed up SHOW STATEMENT df-* /HTML; metamath.c - remove
the unknown date place holder in SAVE NEW_PROOF; Wolf Lammen mmvstr.c -
some cleanup */
/* 0.07.99 1-Nov-2013 nm metamath.c, mmpfas.h,c, mmcmdl.h,c, mmhlpa.c,
mmhlpb.c - added UNDO, REDO, SET UNDO commands (see HELP UNDO) */
/* 0.07.98 30-Oct-2013 Wolf Lammen mmvstr.c,h, mmiou.c, mmpars.c,
mmdata.c - improve code style and program structure */
/* 0.07.97 20-Oct-2013 Wolf Lammen mmvstr.c,h, metamath.c - improved linput();
nm mmcmds.c, mmdata.c - tolerate bad proofs in SHOW TRACE_BACK etc. */
/* 0.07.96 20-Sep-2013 Wolf Lammen mmvstr.c - revised cat();
nm mmwtex.c, mminou.c - change a print2 to printLongLine to fix bug 1150 */
/* 0.07.95 18-Sep-2013 Wolf Lammen mmvstr.c - optimized cat();
nm metamath.c, mmcmds.c, mmdata.c, mmpars.c, mmpfas.c, mmvstr.c,
mmwtex.c - suppress some clang warnings */
/* 0.07.94 28-Aug-2013 Alexey Merkulov mmcmds.c, mmpars.c - fixed several
memory leaks found by valgrind --leak-check=full --show-possibly-lost=no */
/* 0.07.93 8-Jul-2013 Wolf Lammen mmvstr.c - simplified let() function;
also many minor changes in m*.c and m*.h to assist future refactoring */
/* 0.07.92 28-Jun-2013 nm metamath.c mmcmds.c,h mmcmdl.c mmhlpb.c- added
/NO_REPEATED_STEPS for /LEMMON mode of SHOW PROOF, SHOW NEW_PROOF.
This reverts the /LEMMON mode default display change of 31-Jan-2010
and invokes it when desired via /NO_REPEATED_STEPS. */
/* 0.07.91 20-May-2013 nm metamath.c mmpfas.c,h mmcmds.c,h mmcmdl.c
mmhlpb.c- added /FORBID qualifier to MINIMIZE_WITH */
/* 0.07.90 19-May-2013 nm metamath.c mmcmds.c mmcmdl.c mmhlpb.c - added /MATCH
qualifier to SHOW TRACE_BACK */
/* 0.07.88 18-Nov-2012 nm mmcmds.c - fixed bug 243 */
/* 0.07.87 17-Nov-2012 nm mmwtex.c - fixed formatting problem when label
markup ends a comment in SHOW PROOF ... /HTML */
/* 0.07.86 27-Oct-2012 nm mmcmds.c, mmwtex.c, mmwtex.h - fixed ERASE bug
caused by imperfect re-initialization; reported by Wolf Lammen */
/* 0.07.85 10-Oct-2012 nm metamath.c, mmcmdl.c, mmwtex.c, mmwtex.h, mmhlpb.c -
added /SHOW_LEMMAS to WRITE THEOREM_LIST to bypass lemma math suppression */
/* 0.07.84 9-Oct-2012 nm mmcmds.c - fixed bug in getStatementNum() */
/* 0.07.83 19-Sep-2012 nm mmwtex.c - fixed bug reported by Wolf Lammen */
/* 0.07.82 16-Sep-2012 nm metamath.c, mmpfas.c - fixed REPLACE infinite loop;
improved REPLACE message for shared dummy variables */
/* 0.07.81 14-Sep-2012 nm metamath.c, mmcmds.c, mmcmds.h, mmcmdl.c, mmhlpb.c
- added FIRST, LAST, +nn, -nn where missing from ASSIGN, REPLACE,
IMPROVE, LET STEP. Wildcards are allowed for PROVE, ASSIGN, REPLACE
labels provided there is a unique match. */
/* 0.07.80 4-Sep-2012 nm metamath.c, mmpfas.c, mmpfas.h, mmcmdl.c, mmhlpb.c
- added / 1, / 2, / 3, / SUBPROOFS to IMPROVE to specify search level */
/* 0.07.79 31-Aug-2012 nm m*.c - clean up some gcc warnings */
/* 0.07.78 28-Aug-2012 nm mmpfas.c - fix bug in 0.07.77. */
/* 0.07.77 25-Aug-2012 nm metamath.c, mmpfas.c - Enhanced IMPROVE algorithm to
allow non-shared dummy variables in unknown steps */
/* 0.07.76 22-Aug-2012 nm metamath.c, mmpfas.c, mmcmdl.c, mmhlpb.c -
Enhanced IMPROVE algorithm to also try REPLACE algorithm */
/* 0.07.75 14-Aug-2012 nm metamath.c - MINIMIZE_WITH now checks current
mathbox (but not other mathboxes) even if /INCLUDE_MATHBOXES is omitted */
/* 0.07.74 18-Mar-2012 nm mmwtex.c, mmcmds.c, metamath.c - improved texToken()
error message */
/* 0.07.73 26-Dec-2011 nm mmwtex.c, mmpars.c - added <HTML>...</HTML> in
comments for passing through raw HTML code into HTML files generated with
SHOw STATEMENT xxx / HTML */
/* 0.07.72 25-Dec-2011 nm (obsolete) */
/* 0.07.71 10-Nov-2011 nm metamath.c, mmcmdl.c - added /REV to MINIMIZE_WITH */
/* 0.07.70 6-Aug-2011 nm mmwtex.c - fix handling of double quotes inside
of htmldef strings to match spec in Metamath book Appendix A p. 156 */
/* 0.07.69 9-Jul-2011 nm mmpars.c, mmvstr.c - Untab file in WRITE SOURCE
... /REWRAP */
/* 0.07.68 3-Jul-2011 nm metamath.c, mminou.h, mminou.c - Nested SUBMIT calls
(SUBMIT calls inside of a SUBMIT command file) are now allowed.
Also, mmdata.c - fix memory leak. */
/* 0.07.67 2-Jul-2011 nm metamath.c, mmcmdl.c, mmhlpa.c - Added TAG command
to TOOLS. See HELP TAG under TOOLS. (The old special-purpose TAG command
was renamed to UPDATE.) */
/* 0.07.66 1-Jul-2011 nm metamath.c, mmcmds.c, mmpars.c, mmpars.h - Added code
to strip spurious "$( [?] $)" in WRITE SOURCE ... /CLEAN output */
/* 0.07.65 30-Jun-2011 nm mmwtex.c - Prevent processing [...] bibliography
brackets inside of `...` math strings in comments. */
/* 0.07.64 28-Jun-2011 nm metamath.c, mmcmdl.c - Added /INCLUDE_MATHBOXES
qualifier to MINIMIZE_WITH; without it, MINIMIZE_WITH * will skip
checking user mathboxes. */
/* 0.07.63 26-Jun-2011 nm mmwtex.c - check that .gifs exist for htmldefs */
/* 0.07.62 18-Jun-2011 nm mmpars.c - fixed bug where redeclaration of active
$v was not detected */
/* 0.07.61 12-Jun-2011 nm mmpfas.c, mmcmds.c, metamath.c, mmhlpb.c - added
/FORMAT and /REWRAP qualifiers to WRITE SOURCE to format according to set.mm
conventions - set HELP WRITE SOURCE */
/* 0.07.60 7-Jun-2011 nm mmpfas.c - fixed bug 1805 which occurred when doing
MINIMIZE_WITH weq/ALLOW_GROWTH after DELETE DELETE FLOATING_HYPOTHESES */
/* 0.07.59 11-Dec-2010 nm mmpfas.c - increased default SET SEARCH_LIMIT from
10000 to 25000 to accomodate df-plig web page in set.mm */
/* 0.07.58 9-Dec-2010 nm mmpars.c - detect if same symbol is used with both
$c and $v, in order to conform with Metamath spec */
/* 0.07.57 19-Oct-2010 nm mmpars.c - fix bug causing incorrect line count
for error messages when non-ASCII character was found; mminou.h -
increase SET WIDTH maximum from 999 to 9999 */
/* 0.07.56 27-Sep-2010 nm mmpars.c, mmpfas.c - check for $a's with
one token e.g. "$a wff $."; if found, turn SET EMPTY_SUBSTITUTION ON
automatically. (Suggested by Mel O'Cat; patent pending.) */
/* 0.07.55 26-Sep-2010 nm mmunif.c, mmcmds.c, mmunif.h - check for mismatched
brackets in all $a's, so that if there are any, the bracket matching
algorithm (for fewer ambiguous unifications) in mmunif.c will be turned
off. */
/* 0.07.54 25-Sep-2010 nm mmpars.c - added $f checking to conform to the
current Metamath spec, so footnote 2 on p. 92 of Metamath book is
no longer applicable. */
/* 0.07.53 24-Sep-2010 nm mmveri.c - fixed bug(2106), reported by Michal
Burger */
/* 0.07.52 14-Sep-2010 nm metamath.c, mmwtex.h, mmwtex.c, mmcmds.c,
mmcmdl.c, mmhlpb.c - rewrote the LaTeX output for easier hand-editing
and embedding in LaTeX documents. The old LaTeX output is still
available with /OLD_TEX on OPEN TEX, SHOW STATEMENT, and SHOW PROOF,
but it is obsolete and will be deleted eventually if no one objects. The
new /TEX output also replaces the old /SIMPLE_TEX, which was removed. */
/* 0.07.51 9-Sep-2010 Stefan Allen mmwtex.c - put hyperlinks on hypothesis
label references in SHOW STATEMENT * /HTML, ALT_HTML output */
/* 0.07.50 21-Feb-2010 nm mminou.c - "./metamath < empty", where "empty" is a
0-byte file, now exits metamath instead of producing an infinite loop.
Also, ^D now exits metamath. Reported by Cai Yufei */
/* 0.07.49 31-Jan-2010 nm mmcmds.c - Lemmon-style proofs (SHOW PROOF xxx
/LEMON/RENUMBER) no longer have steps with dummy labels; instead, steps
are now the same as in HTML page proofs. (There is a line to comment
out if you want to revert to old behavior.) */
/* 0.07.48 11-Sep-2009 nm mmpars.c, mm, mmvstr.c, mmdata.c - Added detection of
non-whitespace around keywords (mmpars.c); small changes to eliminate
warnings in gcc 3.4.4 (mmvstr.c, mmdata.c) */
/* 0.07.47 2-Aug-2009 nm mmwtex.c, mmwtex.h - added user name to mathbox
pages */
/* 0.07.46 24-Jul-2009 nm metamath.c, mmwtex.c - changed name of sandbox
to "mathbox" */
/* 0.07.45 15-Jun-2009 nm metamath.c, mmhlpb.c - put "!" before each line of
SET ECHO ON output to make them easy to identity for creating scripts */
/* 0.07.44 12-May-2009 Stefan Allan, nm metamath.c, mmcmdl.c, mmwtex.c -
added SHOW STATEMENT / MNEMONICS - see HELP SHOW STATEMENT */
/* 0.07.43 29-Aug-2008 nm mmwtex.c - workaround for Unicode huge font bug in
FireFox 3 */
/* 0.07.42 8-Aug-2008 nm metamath.c - added sandbox, Hilbert Space colors to
Definition List */
/* 0.07.41 29-Jul-2008 nm metamath.c, mmwtex.h, mmwtex.c - Added handling of
sandbox section of Metamath Proof Explorer web pages */
/* 0.07.40 6-Jul-2008 nm metamath.c, mmcmdl.c, mmhlpa.c, mmhlpb.c - Added
/ NO_VERSIONING qualifier for SHOW STATEMENT, so website can be regenerated
in place with less temporary space required. Also, the wildcard trigger
for mmdefinitions.html, etc. is more flexible (see HELP HTML). */
/* 0.07.39 21-May-2008 nm metamath.c, mmhlpb.c - Added wildcard handling to
statement label in SHOW TRACE_BACK. All wildcards now allow
comma-separated lists [i.e. matchesList() instead of matches()] */
/* 0.07.38 26-Apr-2008 nm metamath.c, mmdata.h, mmdata.c, mmvstr.c, mmhlpb.c -
Enhanced / EXCEPT qualifier for MINIMIZE_WITH to handle comma-separated
wildcard list. */
/* 0.07.37 14-Apr-2008 nm metamath.c, mmcmdl.c, mmhlpb.c - Added / JOIN
qualifier to SEARCH. */
/* 0.07.36 7-Jan-2008 nm metamath.c, mmcmdl.c, mmhlpb.c - Added wildcard
handling for labels in SHOW USAGE. */
/* 0.07.35 2-Jan-2008 nm mmcmdl.c, metamath.c, mmhlpb.c - Changed keywords
COMPACT to PACKED and COLUMN to START_COLUMN so that SAVE/SHOW proof can use
C to abbreviate COMPRESSED. (PACKED format is supported but "unofficial,"
used mainly for debugging purposes, and is not listed in HELP SAVE
PROOF.) */
/* 0.07.34 19-Nov-2007 nm mmwtex.c, mminou.c - Added tooltips to proof step
hyperlinks in SHOW STATEMENT.../HTML,ALT_HTML output (suggested by Reinder
Verlinde) */
/* 0.07.33 19-Jul-2007 nm mminou.c, mmvstr.c, mmdata.c, mmword.c - added fflush
after each printf() call for proper behavior inside emacs (suggested by
Frederic Line) */
/* 0.07.32 29-Apr-2007 nm mminou.c - fSafeOpen now stops at gap; e.g. if ~2
doesn't exist, ~1 will be renamed to ~2, but any ~3, etc. are not touched */
/* 0.07.31 5-Apr-2007 nm mmwtex.c - Don't make "_" in hyperlink a subscript */
/* 0.07.30 8-Feb-2007 nm mmcmds.c, mmwtex.c Added HTML statement number info to
SHOW STATEMENT.../FULL; friendlier "Contents+1" link in mmtheorems*.html */
/* 0.07.29 6-Feb-2007 Jason Orendorff mmpfas.c - Patch to eliminate the
duplicate "Exceeded trial limit at step n" messages */
/* 0.07.28 22-Dec-2006 nm mmhlpb.c - Added info on quotes to HELP LET */
/* 0.07.27 23-Oct-2006 nm metamath.c, mminou.c, mmhlpa.c, mmhlpb.c - Added
/ SILENT qualifier to SUBMIT command */
/* 0.07.26 12-Oct-2006 nm mminou.c - Fixed bug when SUBMIT file was missing
a new-line at end of file (reported by Marnix Klooster) */
/* 0.07.25 10-Oct-2006 nm metamath.c - Fixed bug invoking TOOLS as a ./metamath
command-line argument */
/* 0.07.24 25-Sep-2006 nm mmcmdl.c Fixed bug in
SHOW NEW_PROOF/START_COLUMN nn/LEM */
/* 0.07.23 31-Aug-2006 nm mmwtex.c - Added Home and Contents links to bottom of
WRITE THEOREM_LIST pages */
/* 0.07.22 26-Aug-2006 nm metamath.c, mmcmdl.c, mmhlpb.c - Changed 'IMPROVE
STEP <step>' to 'IMPROVE <step>' for user convenience and to be consistent
with ASSIGN <step> */
/* 0.07.21 20-Aug-2006 nm mmwtex.c - Revised small colored numbers so that all
colors have the same grayscale brightness.. */
/* 0.07.20 19-Aug-2006 nm mmpars.c - Made the error "Required hypotheses may
not be explicitly declared" in a compressed proof non-severe, so that we
can still SAVE the proof to reformat and recover it. */
/* 0.07.19 11-Aug-06 nm mmcmds.c - "Distinct variable group(s)" is now
"group" or "groups" as appropriate. */
/* 0.07.18 31-Jul-06 nm mmwtex.c - added table to contents to p.1 of output of
WRITE THEOREM_LIST command. */
/* 0.07.17 4-Jun-06 nm mmpars.c - do not allow labels to match math symbols
(new spec proposed by O'Cat). mmwtex.c - made theorem name 1st in title,
for readability in Firefox tabs. */
/* 0.07.16 16-Apr-06 nm metamath.c, mmcmdl.c, mmpfas.c, mmhlpb.c - allow step
to be negative (relative to end of proof) for ASSIGN, UNIFY, and LET STEP
(see their HELPs). Added INITIALIZE USER to delete LET STEP assignments
(see HELP INITIALIZE). Fixed bug in LET STEP (mmpfas.c). */
/* 0.07.15 10-Apr-06 nm metamath.c, mmvstr.c - change dates from 2-digit to
4-digit year; make compatible with older 2-digit year. */
/* 0.07.14 21-Mar-06 nm mmpars.c - fix bug 1722 when compressed proof has
"Z" at beginning of proof instead of after a proof step. */
/* 0.07.13 3-Feb-06 nm mmpfas.c - minor improvement to MINIMIZE_WITH */
/* 0.07.12 30-Jan-06 nm metamath.c, mmcmds.c, mmdata.c, mmdata.h, mmhlpa.c,
mmhlpb.c - added "?" wildcard to match single character. See HELP SEARCH. */
/* 0.07.11 7-Jan-06 nm metamath.c, mmcmdl.c, mmhlpb.c - added EXCEPT qualifier
to MINIMIZE_WITH */
/* 0.07.10 28-Dec-05 nm metamath.c, mmcmds.c - cosmetic tweaks */
/* 0.07.10 11-Dec-05 nm metamath.c, mmcmdl.c, mmhlpb.c - added ASSIGN FIRST
and IMPROVE FIRST commands. Also enhanced READ error message */
/* 0.07.9 1-Dec-05 nm mmvstr.c - added comment on how to make portable */
/* 0.07.9 18-Nov-05 nm metamath.c, mminou.c, mminou.h, mmcmdl.c, mmhlpb.c -
added SET HEIGHT command; changed SET SCREEN_WIDTH to SET WIDTH; changed
SET HENTY_FILTER to SET JEREMY_HENTY_FILTER (to make H for HEIGHT
unambiguous); added HELP for SET JEREMY_HENTY_FILTER */
/* 0.07.8 15-Nov-05 nm mmunif.c - now detects wrong order in bracket matching
heuristic to further reduce ambiguous unifications in Proof Assistant */
/* 0.07.7 12-Nov-05 nm mmunif.c - add "[","]" and "[_","]_" bracket matching
heuristic to reduce ambiguous unifications in Proof Assistant.
mmwtex.c - added heuristic for HTML spacing after "sum_" token. */
/* 0.07.6 15-Oct-05 nm mmcmds.c,mmpars.c - fixed compressed proof algorithm
to match spec in book (with new algorithm due to Marnix Klooster).
Users are warned to convert proofs when the old compression is found. */
/* 0.07.5 6-Oct-05 nm mmpars.c - fixed bug that reset "severe error in
proof" flag when a proof with severe error also had unknown steps */
/* 0.07.4 1-Oct-05 nm mmcmds.c - ignored bug 235, which could happen for
non-standard logics */
/* 0.07.3 17-Sep-05 nm mmpars.c - reinstated duplicate local label checking to
conform to strict spec */
/* 0.07.2 19-Aug-05 nm mmwtex.c - suppressed math content for lemmas in
WRITE THEOREMS output */
/* 0.07.1 28-Jul-05 nm Added SIMPLE_TEX qualifier to SHOW STATEMENT */
/* 0.07: Official 0.07 22-Jun-05 corresponding to Metamath book */
/* 0.07x: Fixed to work with AMD64 with 64-bit longs by
Waldek Hebisch; deleted unused stuff in mmdata.c */
/* 0.07w: .mm date format like "$( [7-Sep-04] $)" is now
generated and permitted (old one is tolerated too for compatibility) */
/* Metamath Proof Verifier - main program */
/* See the book "Metamath" for description of Metamath and run instructions */
/* The overall functionality of the modules is as follows:
metamath.c - Contains main(); executes or calls commands
mmcmdl.c - Command line interpreter
mmcmds.c - Extends metamath.c command() to execute SHOW and other
commands; added after command() became too bloated (still is:)
mmdata.c - Defines global data structures and manipulates arrays
with functions similar to BASIC string functions;
memory management; converts between proof formats
mmhlpa.c - The help file, part 1.
mmhlpb.c - The help file, part 2.
mminou.c - Basic input and output interface
mmmaci.c - THINK C Macintosh interface (obsolete)
mmpars.c - Parses the source file
mmpfas.c - Proof Assistant
mmunif.c - Unification algorithm for Proof Assistant
mmutil.c - Miscellaneous I/O utilities (reserved for future use)
mmveri.c - Proof verifier for source file
mmvstr.c - BASIC-like string functions
mmwtex.c - LaTeX/HTML source generation
mmword.c - File revision utility (for TOOLS> UPDATE) (not generally useful)
*/
/*****************************************************************************/
/*----------------------------------------------------------------------*/
#include <string.h>
#include <stdio.h>
#include <limits.h>
#include <stdlib.h>
#include <ctype.h>
#include <stdarg.h>
/* #include <time.h> */ /* 21-Jun-2014 nm For ELAPSED_TIME */
#ifdef THINK_C
#include <console.h>
#endif
#include "mmutil.h"
#include "mmvstr.h"
#include "mmdata.h"
#include "mmcmdl.h"
#include "mmcmds.h"
#include "mmhlpa.h"
#include "mmhlpb.h"
#include "mminou.h"
#include "mmpars.h"
#include "mmveri.h"
#include "mmpfas.h"
#include "mmunif.h"
#include "mmword.h"
#include "mmwtex.h"
#ifdef THINK_C
#include "mmmaci.h"
#endif
void command(int argc, char *argv[]);
int main(int argc, char *argv[])
{
/* argc is the number of arguments; argv points to an array containing them */
#ifdef THINK_C
/* Set console attributes */
console_options.pause_atexit = 0; /* No pause at exit */
console_options.title = (unsigned char*)"\pMetamath";
#endif
#ifdef THINK_C
/* The standard stream triggers the console package to initialize the
Macintosh Toolbox managers and use the console interface. cshow must
be called before using our own window to prevent crashing (THINK C
Standard Library Reference p. 43). */
cshow(stdout);
/* Initialize MacIntosh interface */
/*ToolBoxInit(); */ /* cshow did this automatically */
/* Display opening window */
/*
WindowInit();
DrawMyPicture();
*/
/* Wait for mouse click or key */
/*while (!Button());*/
#endif
/****** If listMode is set to 1 here, the startup will be Text Tools
utilities, and Metamath will be disabled ***************************/
/* (Historically, this mode was used for the creation of a stand-alone
"TOOLS>" utility for people not interested in Metamath. This utility
was named "LIST.EXE", "tools.exe", and "tools" on VMS, DOS, and Unix
platforms respectively. The UPDATE command of TOOLS (mmword.c) was
custom-written in accordance with the version control requirements of a
company that used it; it documents the differences between two versions
of a program as C-style comments embedded in the newer version.) */
listMode = 0; /* Force Metamath mode as startup */
toolsMode = listMode;
if (!listMode) {
/*print2("Metamath - Version %s\n", MVERSION);*/
print2("Metamath - Version %s%s", MVERSION, space(27 - (long)strlen(MVERSION)));
}
/* if (argc < 2) */ print2("Type HELP for help, EXIT to exit.\n");
/* Allocate big arrays */
initBigArrays();
/* 14-May-2017 nm */
/* Set the default contributor */
let(&contributorName, DEFAULT_CONTRIBUTOR);
/* Process a command line until EXIT */
command(argc, argv);
/* Close logging command file */
if (listMode && listFile_fp != NULL) {
fclose(listFile_fp);
}
return 0;
}
void command(int argc, char *argv[])
{
/* Command line user interface -- this is an infinite loop; it fetches and
processes a command; returns only if the command is 'EXIT' or 'QUIT' and
never returns otherwise. */
long argsProcessed = 0; /* Number of argv initial command-line
arguments processed so far */
long /*c,*/ i, j, k, m, l, n, p, q, r, s /*,tokenNum*/;
long stmt, step;
int subType = 0;
#define SYNTAX 4
vstring str1 = "", str2 = "", str3 = "", str4 = "", str5= "";
nmbrString *nmbrTmpPtr; /* Pointer only; not allocated directly */
nmbrString *nmbrTmp = NULL_NMBRSTRING;
nmbrString *nmbrSaveProof = NULL_NMBRSTRING;
/*pntrString *pntrTmpPtr;*/ /* Pointer only; not allocated directly */
pntrString *pntrTmp = NULL_PNTRSTRING;
pntrString *expandedProof = NULL_PNTRSTRING;
flag tmpFlag;
/* 1-Nov-2013 nm proofSavedFlag tells us there was at least one
SAVE NEW_PROOF during the MM-PA session while the UNDO stack wasn't
empty, meaning that "UNDO stack empty" is no longer a reliable indication
that the proof wasn't changed. It is cleared upon entering MM-PA, and
set by SAVE NEW_PROOF. */
flag proofSavedFlag = 0;
/* Variables for SHOW PROOF */
flag pipFlag; /* Proof-in-progress flag */
long outStatement; /* Statement for SHOW PROOF or SHOW NEW_PROOF */
flag explicitTargets; /* For SAVE PROOF /EXPLICIT */
long startStep; long endStep;
/* long startIndent; */
long endIndent; /* Also for SHOW TRACE_BACK */
flag essentialFlag; /* Also for SHOW TRACE_BACK */
flag renumberFlag; /* Flag to use essential step numbering */
flag unknownFlag;
flag notUnifiedFlag;
flag reverseFlag;
long detailStep;
flag noIndentFlag; /* Flag to use non-indented display */
long splitColumn; /* Column at which formula starts in nonindented display */
flag skipRepeatedSteps; /* NO_REPEATED_STEPS qualifier */ /* 28-Jun-2013 nm */
flag texFlag; /* Flag for TeX */
flag saveFlag; /* Flag to save in source */
flag fastFlag; /* Flag for SAVE PROOF.../FAST */ /* 2-Jan-2017 nm */
long indentation; /* Number of spaces to indent proof */
vstring labelMatch = ""; /* SHOW PROOF <label> argument */
flag axiomFlag; /* For SHOW TRACE_BACK */
flag treeFlag; /* For SHOW TRACE_BACK */ /* 19-May-2013 nm */
flag countStepsFlag; /* For SHOW TRACE_BACK */ /* 19-May-2013 nm */
flag matchFlag; /* For SHOW TRACE_BACK */ /* 19-May-2013 nm */
vstring matchList = ""; /* For SHOW TRACE_BACK */ /* 19-May-2013 nm */
vstring traceToList = ""; /* For SHOW TRACE_BACK */ /* 18-Jul-2015 nm */
flag recursiveFlag; /* For SHOW USAGE */
long fromLine, toLine; /* For TYPE, SEARCH */
flag joinFlag; /* For SEARCH */
long searchWindow; /* For SEARCH */
FILE *type_fp; /* For TYPE, SEARCH */
long maxEssential; /* For MATCH */
nmbrString *essentialFlags = NULL_NMBRSTRING;
/* For ASSIGN/IMPROVE FIRST/LAST */
long improveDepth; /* For IMPROVE */
flag searchAlg; /* For IMPROVE */ /* 22-Aug-2012 nm */
flag searchUnkSubproofs; /* For IMPROVE */ /* 4-Sep-2012 nm */
flag dummyVarIsoFlag; /* For IMPROVE */ /* 25-Aug-2012 nm */
long improveAllIter; /* For IMPROVE ALL */ /* 25-Aug-2012 nm */
flag proofStepUnk; /* For IMPROVE ALL */ /* 25-Aug-2012 nm */
flag texHeaderFlag; /* For OPEN TEX, CLOSE TEX */
flag commentOnlyFlag; /* For SHOW STATEMENT */
flag briefFlag; /* For SHOW STATEMENT */
flag linearFlag; /* For SHOW LABELS */
vstring bgcolor = ""; /* For SHOW STATEMENT definition list */
/* 8-Aug-2008 nm */
flag verboseMode, mayGrowFlag /*, noDistinctFlag*/; /* For MINIMIZE_WITH */
long prntStatus; /* For MINIMIZE_WITH */
flag hasWildCard; /* For MINIMIZE_WITH */
long exceptPos; /* For MINIMIZE_WITH */
flag mathboxFlag; /* For MINIMIZE_WITH */ /* 28-Jun-2011 nm */
long thisMathboxStmt; /* For MINIMIZE_WITH */ /* 14-Aug-2012 nm */
flag forwFlag; /* For MINIMIZE_WITH */ /* 11-Nov-2011 nm */
long forbidMatchPos; /* For MINIMIZE_WITH */ /* 20-May-2013 nm */
vstring forbidMatchList = ""; /* For MINIMIZE_WITH */ /* 20-May-2013 nm */
long noNewAxiomsMatchPos; /* For NO_NEW_AXIOMS_FROM */ /* 22-Nov-2014 nm */
vstring noNewAxiomsMatchList = ""; /* For NO_NEW_AXIOMS_FROM */ /* 22-Nov-2014 */
long allowNewAxiomsMatchPos; /* For NO_NEW_AXIOMS_FROM */ /* 4-Aug-2019 nm */
vstring allowNewAxiomsMatchList = ""; /* For NO_NEW_AXIOMS_FROM */ /* 4-Aug-2019 */
vstring traceProofFlags = ""; /* For NO_NEW_AXIOMS_FROM */ /* 22-Nov-2014 nm */
vstring traceTrialFlags = ""; /* For NO_NEW_AXIOMS_FROM */ /* 22-Nov-2014 nm */
flag overrideFlag; /* For discouraged statement /OVERRIDE */ /* 3-May-2016 nm */
struct pip_struct saveProofForReverting = {
NULL_NMBRSTRING, NULL_PNTRSTRING, NULL_PNTRSTRING, NULL_PNTRSTRING };
/* For MINIMIZE_WITH */ /* 20-May-2013 nm */
long origCompressedLength; /* For MINIMIZE_WITH */ /* 25-Jun-2014 nm */
long oldCompressedLength = 0; /* For MINIMIZE_WITH */ /* 25-Jun-2014 nm */
long newCompressedLength = 0; /* For MINIMIZE_WITH */ /* 25-Jun-2014 nm */
long forwardCompressedLength = 0; /* For MINIMIZE_WITH */ /* 25-Jun-2014 nm */
long forwardLength = 0; /* For MINIMIZE_WITH */ /* 25-Jun-2014 nm */
vstring saveZappedProofSectionPtr; /* Pointer only */ /* For MINIMIZE_WITH */
long saveZappedProofSectionLen; /* For MINIMIZE_WITH */ /* 25-Jun-2014 nm */
flag saveZappedProofSectionChanged; /* For MINIMIZE_WITH */ /* 16-Jun-2017 nm */
struct pip_struct saveOrigProof = {
NULL_NMBRSTRING, NULL_PNTRSTRING, NULL_PNTRSTRING, NULL_PNTRSTRING };
/* For MINIMIZE_WITH */ /* 25-Jun-2014 nm */
struct pip_struct save1stPassProof = {
NULL_NMBRSTRING, NULL_PNTRSTRING, NULL_PNTRSTRING, NULL_PNTRSTRING };
/* For MINIMIZE_WITH */ /* 25-Jun-2014 nm */
long forwRevPass; /* 1 = forward pass */ /* 25-Jun-2014 nm */
long sourceStatement; /* For EXPAND */ /* 11-Sep-2016 nm */
flag showLemmas; /* For WRITE THEOREM_LIST */ /* 10-Oct-2012 nm */
flag noVersioning; /* For WRITE THEOREM_LIST & others */ /* 17-Jul-2019 nm */
long theoremsPerPage; /* For WRITE THEOREM_LIST */ /* 17-Jul-2019 nm */
/* toolsMode-specific variables */
flag commandProcessedFlag = 0; /* Set when the first command line processed;
used to exit shell command line mode */
FILE *list1_fp;
FILE *list2_fp;
FILE *list3_fp;
vstring list2_fname = "", list2_ftmpname = "";
vstring list3_ftmpname = "";
vstring oldstr = "", newstr = "";
long lines, changedLines, oldChangedLines, twoMatches, p1, p2;
long firstChangedLine;
flag cmdMode, changedFlag, outMsgFlag;
double sum;
vstring bufferedLine = "";
vstring tagStartMatch = ""; /* 2-Jul-2011 nm For TAG command */
long tagStartCount = 0; /* 2-Jul-2011 nm For TAG command */
vstring tagEndMatch = ""; /* 2-Jul-2011 nm For TAG command */
long tagEndCount = 0; /* 2-Jul-2011 nm For TAG command */
long tagStartCounter = 0; /* 2-Jul-2011 nm For TAG command */
long tagEndCounter = 0; /* 2-Jul-2011 nm For TAG command */
/* 21-Jun-2014 */
/* 16-Aug-2016 nm Now in getElapasedTime() */
/* clock_t timePrevious = 0; */ /* For SHOW ELAPSED_TIME command */
/* clock_t timeNow = 0; */ /* For SHOW ELAPSED_TIME command */
/* 16-Aug-2016 nm */
double timeTotal = 0;
double timeIncr = 0;
flag printTime; /* Set by "/ TIME" in SAVE PROOF and others */
/* 14-Aug-2018 nm */
flag defaultScrollMode = 1; /* Default to prompted mode */
/* Initialization to avoid compiler warning (should not be theoretically
necessary) */
p = 0;
q = 0;
s = 0;
texHeaderFlag = 0;
firstChangedLine = 0;
tagStartCount = 0; /* 2-Jul-2011 nm For TAG command */
tagEndCount = 0; /* 2-Jul-2011 nm For TAG command */
tagStartCounter = 0; /* 2-Jul-2011 nm For TAG command */
tagEndCounter = 0; /* 2-Jul-2011 nm For TAG command */
while (1) {
if (listMode) {
/* If called from the OS shell with arguments, do one command
then exit program. */
/* (However, let a SUBMIT job complete) */
if (argc > 1 && commandProcessedFlag &&
commandFileNestingLevel == 0) return;
}
errorCount = 0; /* Reset error count before each read or proof parse. */
/* Deallocate stuff that may have been used in previous pass */
let(&str1,"");
let(&str2,"");
let(&str3,"");
let(&str4,"");
let(&str5,"");
nmbrLet(&nmbrTmp, NULL_NMBRSTRING);
pntrLet(&pntrTmp, NULL_PNTRSTRING);
nmbrLet(&nmbrSaveProof, NULL_NMBRSTRING);
nmbrLet(&essentialFlags, NULL_NMBRSTRING);
j = nmbrLen(rawArgNmbr);
if (j != rawArgs) bug(1110);
j = pntrLen(rawArgPntr);
if (j != rawArgs) bug(1111);
rawArgs = 0;
for (i = 0; i < j; i++) let((vstring *)(&rawArgPntr[i]), "");
pntrLet(&rawArgPntr, NULL_PNTRSTRING);
nmbrLet(&rawArgNmbr, NULL_NMBRSTRING);
j = pntrLen(fullArg);
for (i = 0; i < j; i++) let((vstring *)(&fullArg[i]),"");
pntrLet(&fullArg,NULL_PNTRSTRING);
j = pntrLen(expandedProof);
if (j) {
for (i = 0; i < j; i++) {
let((vstring *)(&expandedProof[i]),"");
}
pntrLet(&expandedProof,NULL_PNTRSTRING);
}
let(&list2_fname, "");
let(&list2_ftmpname, "");
let(&list3_ftmpname, "");
let(&oldstr, "");
let(&newstr, "");
let(&labelMatch, "");
/* (End of space deallocation) */
midiFlag = 0; /* 8/28/00 Initialize here in case SHOW PROOF exits early */
if (memoryStatus) {
/*??? Change to user-friendly message */
#ifdef THINK_C
print2("Memory: string %ld xxxString %ld free %ld\n",db,db3,(long)FreeMem());
getPoolStats(&i, &j, &k);
print2("Pool: free alloc %ld used alloc %ld used actual %ld\n",i,j,k);
#else
print2("Memory: string %ld xxxString %ld\n",db,db3);
#endif
getPoolStats(&i, &j, &k);
print2("Pool: free alloc %ld used alloc %ld used actual %ld\n",i,j,k);
}
if (!toolsMode) {
if (PFASmode) {
let(&commandPrompt,"MM-PA> ");
} else {
let(&commandPrompt,"MM> ");
}
} else {
if (listMode) {
let(&commandPrompt,"Tools> ");
} else {
let(&commandPrompt,"TOOLS> ");
}
}
let(&commandLine,""); /* Deallocate previous contents */
if (!commandProcessedFlag && argc > 1 && argsProcessed < argc - 1
&& commandFileNestingLevel == 0) {
/* if (toolsMode) { */ /* 10-Oct-2006 nm Fix bug: changed to listMode */
if (listMode) {
/* If program was compiled in TOOLS mode, the command-line argument
is assumed to be a single TOOLS command; build the equivalent
TOOLS command */
for (i = 1; i < argc; i++) {
argsProcessed++;
/* Put quotes around an argument with spaces or tabs or quotes
or empty string */
if (instr(1, argv[i], " ") || instr(1, argv[i], "\t")
|| instr(1, argv[i], "\"") || instr(1, argv[i], "'")
|| (argv[i])[0] == 0) {
/* If it contains a double quote, use a single quote */
if (instr(1, argv[i], "\"")) {
let(&str1, cat("'", argv[i], "'", NULL));
} else {
/* (??? (TODO)Case of both ' and " is not handled) */
let(&str1, cat("\"", argv[i], "\"", NULL));
}
} else {
let(&str1, argv[i]);
}
let(&commandLine, cat(commandLine, (i == 1) ? "" : " ", str1, NULL));
}
} else {
/* If program was compiled in default (Metamath) mode, each command-line
argument is considered a full Metamath command. User is responsible
for ensuring necessary quotes around arguments are passed in. */
argsProcessed++;
scrollMode = 0; /* Set continuous scrolling until completed */
let(&commandLine, cat(commandLine, argv[argsProcessed], NULL));
if (argc == 2 && instr(1, argv[1], " ") == 0) {
/* Assume the user intended a READ command. This special mode allows
invocation via "metamath xxx.mm". */
if (instr(1, commandLine, "\"") || instr(1, commandLine, "'")) {
/* If it already has quotes don't put quotes */