Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Manpage #98

Merged
merged 7 commits into from
Sep 19, 2022
Merged

Manpage #98

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
b30c096
manpage: consistent spelling 'database'; consistent double space afte…
benjub Sep 7, 2022
93f4ffb
README.TXT: consistent spelling 'database'
benjub Sep 7, 2022
8ce9dba
add bib words criterion/criteria
benjub Sep 7, 2022
ba94c56
fix typo mmhlpb.c-->mmhlpa.c
benjub Sep 12, 2022
e97c24d
sort list of keywords alphabetically
benjub Sep 12, 2022
e1083de
reorder list of keywords
benjub Sep 12, 2022
a64621b
comment indentation
benjub Sep 16, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion README.TXT
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
32 changes: 16 additions & 16 deletions src/mmwtex.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5271,52 +5271,52 @@ 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 */
|| !strcmp(mid(str2, k, (long)strlen("THEOREM")), "THEOREM")
Copy link
Contributor

@wlammen wlammen Sep 12, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This list is searched sequentially. Matching an item at the beginning is obviously way more efficient (1 comparison) than one at the end (40 comparisons). So if you know, the keyword in str2 is 'theorem' 70% of the time, it makes some sense, to have it at the beginning. This is the gist of the deleted comment here. I think, the first 5 elements of the old list were deliberately put in the early position for speed up. The tail starting with 'AXIOM' are matched fairly seldom, so their exact position does not really matter, and we can keep an alphabetic order there, without compromising speed to a noticeable degree.

What do I personally think of it? Well, if search time really matters, than there are better strategies around, like binary search, for example. This is a poor man's optimization. It may have an improving effect, though, depending on how often a search is called. Without knowing details, I would keep the first five elements, but order the tail.

The 0 in the beginning of the list is likely optimized out and just there to keep all items, including the first, in the same textual format.

Copy link
Contributor

@wlammen wlammen Sep 12, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

From a technical point of view, I do not object to this PR any more, unless you see a slow down due to the impoverished search.
Maybe one should add a
// ---- end of optimized search -----
in between head and tail of the list, for better understanding.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I do not know C well enough, so I rely on you here. What order do you prefer ? Is the following ok (including comments) ?

           /* **IMPORTANT** Make sure to update mmhlpa.c HELP WRITE BIBLIOGRAPHY
              if new items are added to this list. */
           if (0
              /* 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 -----
              ... [alphabetical]

?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is fine

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks. That's the content of my latest commit. So I guess you can approve. (On this repository, I have no right to approve or merge --- and am not asking for one.)

|| !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")
|| !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("DEFINITION")), "DEFINITION")
|| !strcmp(mid(str2, k, (long)strlen("EQUATION")), "EQUATION")
|| !strcmp(mid(str2, k, (long)strlen("EXAMPLE")), "EXAMPLE")
|| !strcmp(mid(str2, k, (long)strlen("EXERCISE")), "EXERCISE")
|| !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("LEMMA")), "LEMMA")
|| !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")
|| !strcmp(mid(str2, k, (long)strlen("THEOREM")), "THEOREM")
) {
m = k;
break;
Expand Down