Skip to content

Commit

Permalink
Merge pull request #98 from benjub/manpage
Browse files Browse the repository at this point in the history 
Manpage
  • Loading branch information
@david-a-wheeler
david-a-wheeler authored Sep 19, 2022
2 parents adb9bec + a64621b commit 134468f
Show file tree
Hide file tree
Showing 5 changed files with 37 additions and 32 deletions.
2 changes: 1 addition & 1 deletion README.TXT
View file
Original file line number Diff line number Diff line change
Expand Up @@ -127,7 +127,7 @@ you can use "make uninstall" to remove it.
List of databases
-----------------

The data base files included are:
The database files included are:

set.mm - logic and set theory database (see Ch. 3 of the Metamath book).
The Metamath Proof Explorer pages were generated from this database.
Expand Down
28 changes: 14 additions & 14 deletions src/metamath.1
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ metamath \- Formal proof verifier and proof assistant
is a formal proof verifier and proof assistant for the Metamath language.
It can be initialized via a series of
.I commands
or with a data base
or with a database
.IR file ,
which can then be explored interactively.
.PP
Expand All @@ -38,10 +38,10 @@ installed along with the package.
.SH LANGUAGE
A Metamath database consists of a sequence of three kinds of tokens
separated by white space (which is any sequence of one or more white
space characters). The set of keyword tokens is
space characters). The set of keyword tokens is
.BR ${ ", " $} ", " $c ", " $v ", " $f ", " $e ", " $d ", " $a ", " $p ", "
.BR $. ", " $= ", " $( ", " $) ", " $[ ", and " $] .
The latter four are called auxiliary or preprocessing keywords. A
The latter four are called auxiliary or preprocessing keywords. A
.I label
token consists of any combination of letters, digits, and the characters hyphen,
underscore, and period.
Expand All @@ -62,29 +62,29 @@ Include the contents of a
.IR file .
.TP
.BI ${ " statements " $}
Scoped block of statements. A math symbol becomes active when declared and
Scoped block of statements. A math symbol becomes active when declared and
stays active until the end of the block in which it is declared.
.TP
.BI $v " symbols " $.
Declare
.I symbols
as variables. A variable may not be declared a second time while it is active,
as variables. A variable may not be declared a second time while it is active,
but it may be declared again (as a variable, but not as a constant) after it
becomes inactive.
.TP
.BI $c " symbols " $.
Declare
.I symbols
as constants. A constant must be declared in the outermost block and may not be
declared a second time.
as constants. A constant must be declared in the outermost block and may not
be declared a second time.
.TP
.IB "label " $f " constant variable " $.
Variable-type hypothesis to specify the nature or type of a variable (such as
`let x be an integer.'). A variable must have its type specified in a
`let x be an integer.'). A variable must have its type specified in a
.B $f
statement before it may be used in a
.BR $e ", " $a ", or " $p
statement. There may not be two active
statement. There may not be two active
.B $f
statements containing the same variable.
.TP
Expand All @@ -93,31 +93,31 @@ Logical hypothesis, expressing a logical truth (such as `assume x is prime')
that must be established in order for an assertion requiring it to also be true.
.TP
.BI $d " variables " $.
Disjoint variable restriction. For distinct active
Disjoint variable restriction. For distinct active
.IR variables ,
it forbids the substitution of one variable with another.
.TP
.IB "label " $a " constant symbols " $.
Axiomatic assertion.
.TP
.IB "label " $p " constant symbols " $= " proof " $.
Provable assertion. The
Provable assertion. The
.I proof
is a sequence of statement
.IR label s.
This label sequence serves as a set of instructions that the Metamath program
uses to construct a series of math symbol sequences. The construction must
uses to construct a series of math symbol sequences. The construction must
ultimately result in the math symbol sequence contained between the
.BR $p " and " $=
keywords of the
.B $p
statement. For details, see section 4.3 in [1].
statement. For details, see section 4.3 in [1].
Proofs are most easily written using the interactive prompt in
.BR metamath .
.SH FILES
.I /usr/share/metamath
.RS
Data base files for several formal theories.
Database files for several formal theories.
.SH SEE ALSO
.B "[1]"
Norman Megill:
Expand Down
4 changes: 3 additions & 1 deletion src/metamath.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,9 @@
Remove mmmaci and everything related to THINK_C compiler
4-Jan-2022 mc - change VERIFY MARKUP /TOP_DATE_SKIP and /FILE_SKIP to
/TOP_DATE_CHECK and /FILE_CHECK (with opposite meaning), and make the
skip behavior the default. */
skip behavior the default.
7-Sep-2022 bj mmwtex.c, mmhlpa.c Added CRITERIA CRITERION to [bib]
keywords */
/* 0.198 nm 7-Aug-2021 mmpars.c - Fix cosmetic bug in WRITE SOURCE ... /REWRAP
that prevented end of sentence (e.g. period) from appearing in column 79,
thus causing some lines to be shorter than necessary. */
Expand Down
10 changes: 5 additions & 5 deletions src/mmhlpa.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1130,11 +1130,11 @@ H("");
H("The <keyword>, which is not case-sensitive, must be one of the following:");
H("");
H(" Axiom, Chapter, Claim, Compare, Conclusion, Condition, Conjecture,");
H(" Corollary, Definition, Equation, Example, Exercise, Fact, Figure,");
H(" Introduction, Item, Lemma, Lemmas, Line, Lines, Notation, Note,");
H(" Observation, Paragraph, Part, Postulate, Problem, Proof, Property,");
H(" Proposition, Remark, Result, Rule, Scheme, Scolia, Scolion, Section,");
H(" Statement, Subsection, Table, Theorem");
H(" Corollary, Criteria, Criterion, Definition, Equation, Example,");
H(" Exercise, Fact, Figure, Introduction, Item, Lemma, Lemmas, Line,");
H(" Lines, Notation, Note, Observation, Paragraph, Part, Postulate,");
H(" Problem, Proof, Property, Proposition, Remark, Result, Rule, Scheme,");
H(" Scolia, Scolion, Section, Statement, Subsection, Table, Theorem");
H("");
H("The <identifier> is optional, as in for example \"Remark in [Monk] p. 22\".");
H("");
Expand Down
25 changes: 14 additions & 11 deletions src/mmwtex.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5271,50 +5271,53 @@ flag writeBibliography(vstring bibFile,
/* (The string search below is rather inefficient; maybe improve
the algorithm if speed becomes a problem.) */
for (k = j - 1; k >= 1; k--) {
/* **IMPORTANT** Make sure to update mmhlpb.c HELP WRITE BIBLIOGRAPHY
/* **IMPORTANT** Make sure to update mmhlpa.c HELP WRITE BIBLIOGRAPHY
if new items are added to this list. */
if (0
/* Put the most frequent ones first to speed up search;
TODO: count occurrences in mmbiblio.html to find optimal order */
/* The first five keywords are more frequent so are put first for
efficiency; the rest is in alphabetical order. */
|| !strcmp(mid(str2, k, (long)strlen("THEOREM")), "THEOREM")
|| !strcmp(mid(str2, k, (long)strlen("EQUATION")), "EQUATION")
|| !strcmp(mid(str2, k, (long)strlen("DEFINITION")), "DEFINITION")
|| !strcmp(mid(str2, k, (long)strlen("LEMMA")), "LEMMA")
|| !strcmp(mid(str2, k, (long)strlen("EXERCISE")), "EXERCISE")
// ---- end of optimized search -----
|| !strcmp(mid(str2, k, (long)strlen("AXIOM")), "AXIOM")
|| !strcmp(mid(str2, k, (long)strlen("CLAIM")), "CLAIM")
|| !strcmp(mid(str2, k, (long)strlen("CHAPTER")), "CHAPTER")
|| !strcmp(mid(str2, k, (long)strlen("CLAIM")), "CLAIM")
|| !strcmp(mid(str2, k, (long)strlen("COMPARE")), "COMPARE")
|| !strcmp(mid(str2, k, (long)strlen("CONCLUSION")), "CONCLUSION")
|| !strcmp(mid(str2, k, (long)strlen("CONDITION")), "CONDITION")
|| !strcmp(mid(str2, k, (long)strlen("CONJECTURE")), "CONJECTURE")
|| !strcmp(mid(str2, k, (long)strlen("COROLLARY")), "COROLLARY")
|| !strcmp(mid(str2, k, (long)strlen("CRITERIA")), "CRITERIA")
|| !strcmp(mid(str2, k, (long)strlen("CRITERION")), "CRITERION")
|| !strcmp(mid(str2, k, (long)strlen("EXAMPLE")), "EXAMPLE")
|| !strcmp(mid(str2, k, (long)strlen("FACT")), "FACT")
|| !strcmp(mid(str2, k, (long)strlen("FIGURE")), "FIGURE")
|| !strcmp(mid(str2, k, (long)strlen("INTRODUCTION")), "INTRODUCTION")
|| !strcmp(mid(str2, k, (long)strlen("ITEM")), "ITEM")
|| !strcmp(mid(str2, k, (long)strlen("LEMMAS")), "LEMMAS")
|| !strcmp(mid(str2, k, (long)strlen("LINE")), "LINE")
|| !strcmp(mid(str2, k, (long)strlen("LINES")), "LINES")
|| !strcmp(mid(str2, k, (long)strlen("NOTATION")), "NOTATION")
|| !strcmp(mid(str2, k, (long)strlen("NOTE")), "NOTE")
|| !strcmp(mid(str2, k, (long)strlen("OBSERVATION")), "OBSERVATION")
|| !strcmp(mid(str2, k, (long)strlen("PARAGRAPH")), "PARAGRAPH")
|| !strcmp(mid(str2, k, (long)strlen("PART")), "PART")
|| !strcmp(mid(str2, k, (long)strlen("POSTULATE")), "POSTULATE")
|| !strcmp(mid(str2, k, (long)strlen("PROBLEM")), "PROBLEM")
|| !strcmp(mid(str2, k, (long)strlen("PROOF")), "PROOF")
|| !strcmp(mid(str2, k, (long)strlen("PROPERTY")), "PROPERTY")
|| !strcmp(mid(str2, k, (long)strlen("PROPOSITION")), "PROPOSITION")
|| !strcmp(mid(str2, k, (long)strlen("REMARK")), "REMARK")
|| !strcmp(mid(str2, k, (long)strlen("RESULT")), "RESULT")
|| !strcmp(mid(str2, k, (long)strlen("RULE")), "RULE")
|| !strcmp(mid(str2, k, (long)strlen("SCHEME")), "SCHEME")
|| !strcmp(mid(str2, k, (long)strlen("SECTION")), "SECTION")
|| !strcmp(mid(str2, k, (long)strlen("PROOF")), "PROOF")
|| !strcmp(mid(str2, k, (long)strlen("STATEMENT")), "STATEMENT")
|| !strcmp(mid(str2, k, (long)strlen("CONCLUSION")), "CONCLUSION")
|| !strcmp(mid(str2, k, (long)strlen("FACT")), "FACT")
|| !strcmp(mid(str2, k, (long)strlen("INTRODUCTION")), "INTRODUCTION")
|| !strcmp(mid(str2, k, (long)strlen("PARAGRAPH")), "PARAGRAPH")
|| !strcmp(mid(str2, k, (long)strlen("SCOLIA")), "SCOLIA")
|| !strcmp(mid(str2, k, (long)strlen("SCOLION")), "SCOLION")
|| !strcmp(mid(str2, k, (long)strlen("SECTION")), "SECTION")
|| !strcmp(mid(str2, k, (long)strlen("STATEMENT")), "STATEMENT")
|| !strcmp(mid(str2, k, (long)strlen("SUBSECTION")), "SUBSECTION")
|| !strcmp(mid(str2, k, (long)strlen("TABLE")), "TABLE")
) {
Expand Down

0 comments on commit 134468f

Please sign in to comment.