Suggestion: Add "Conventions" appendix to mmset.html

[David A. Wheeler]

Perhaps the set.mm index page <http://us.metamath.org/mpegif/mmset.html>
should have a new appendix called "Conventions". I expect it would be especially
useful for new readers.

This should probably include subsets from the embedded
"5. Other notes" section inside set.mm, which is currently completely invisible
to people reading the generated HTML.
In addition, I'd add something like this:

----------------------------
In a number of cases it's useful to consider a statement an axiom
by higher-level statements, even if it can be proven.
In these cases the statement is expressed as an axiom, with the name "ax-...",
after it has been proven using the name "ax...".

If something should only be used in limited ways, it is marked with
"(New usage is discouraged.)". This is used, for example, when something
can be constructed in more than one way, and we do not want later theorems
to depend on a specific construction.

In some cases a proof should not normally be changed, e.g., when it demonstrates
some specific technique. These are marked with "(Proof modification is discouraged.)".
-----------------------------


--- David A. Wheeler

[Norman Megill]

On Saturday, December 17, 2016 at 12:37:05 PM UTC-5, David A. Wheeler wrote:

Perhaps the set.mm index page <http://us.metamath.org/mpegif/mmset.html>
should have a new appendix called "Conventions".  I expect it would be especially
useful for new readers.

This should probably include subsets from the embedded
"5. Other notes" section inside set.mm, which is currently completely invisible
to people reading the generated HTML.

I agree that this should be documented in a way that is easy to find, but mmset.html is getting uncomfortably long.  A supplementary page covering the language and markup conventions may be better, linked to on mmset.html and referenced at relevant points in the mmset body.  While I would eventually provide such a page, it may be some time before I get to it.  If anyone else wants to start such a page I can review it, make corrections, and add missing material.  Another auxiliary page such as Real and Complex Numbers could be used as a starting template for a uniform appearance.

The intended purpose of mmset.html is to assist a newcomer in understanding the axiom and theorem web pages, without getting into the source language underneath.  Understanding the markup conventions is primarily of interest to someone creating new theorems, supplementing an understanding of the language itself.
 

In addition, I'd add something like this:

----------------------------
In a number of cases it's useful to consider a statement an axiom
by higher-level statements, even if it can be proven.
In these cases the statement is expressed as an axiom, with the name "ax-...",
after it has been proven using the name "ax...".

If something should only be used in limited ways, it is marked with
"(New usage is discouraged.)". This is used, for example, when something
can be constructed in more than one way, and we do not want later theorems
to depend on a specific construction.

In some cases a proof should not normally be changed, e.g., when it demonstrates
some specific technique.  These are marked with "(Proof modification is discouraged.)".
-----------------------------

 

This falls in an in-between area of understanding the source database and the web pages, since it does appear as plain text on the web pages (I like that).  I can add the above to mmset as a summary description, with a link to the more detailed description of how it should affect the behavior of a proof assistant on a new language and conventions page.  Or maybe it would be best to keep everything on the new page.

Whether selected parts from the top of set.mm are added to mmset depends on whether they are something that a web page user needs to understand, but a lot of it (such as the idiom ph -> A. x ph) is already on mmset, in Appendix 2 in this case.  (The description of that idiom will have to be revised for Mario's ENF.)

Here are some sources for material for a supplementary Language and Conventions page (or should it be two separate pages?):

- Notes at the top of set.mm, "5. Other notes" section
- Notes scattered throughout this Google Group e.g. https://groups.google.com/d/msg/metamath/QE0lwg9f5Ho/J8ekl_lH1I8J on headers for the Theorem List.  Posts written by me near the end of a thread sometimes have a summary of agreed upon changes that have been implemented in metamath.exe.
- Notes scattered about the randomly maintained http://us.metamath.org/mpegif/mmnotes.txt such as the detailed behavior of the "discouraged" markup currently at the top
- Notes in the older http://us.metamath.org/mpegif/mmnotes2004.txt such as the 13-May-04 entry for informal label conventions (that needs to be updated a little for our current conventions)
- In metamath.exe, 'help language', 'help html', 'help write theorem_list', 'help write bibliography', 'help set discouragement', 'help show discouraged', and the '/override' qualifier in 'help prove, assign, replace, improve, minimize_with, save new_proof'  provide a summary of existing markup conventions and their behavior.  The entire help text content is contained in mmhlpa.c and mmhlpb.c.
- Notes in the old AsteroidMeta pages http://us.metamath.org/other.html#asteroid (directory listing http://us.metamath.org/other/AsteroidMeta/ which needs ".html" appended to the file names and internal links), in particular the "set.mm_discussion_replacement" page

The Language part of the page could have the official Metamath language spec kept up to date.  While these will be updated the Metamath book eventually, I don't change the book very often for several reasons (people use page number references in emails or posts, changing things can lead to bad line and page breaks that have to be repaired, and updating the printed version has run into unexpected problems with changes in the lulu.com software).  A web page is much easier to keep updated.  I think the following provide the current differences between proposed spec changes and the book:

- Proposed language spec changes #1-#7 (on #7, my current thought is that there is no reason to complicate the language by forbidding $e in the outermost scope, even though it is useless in a practical sense) - https://groups.google.com/d/msg/metamath/ZlRle52FVO0/7TqSetEtCQAJ
- Proposed spec change #8 - https://groups.google.com/d/msg/metamath/yQTxS6Y5o0E/S1hzmRFqCAAJ

If anyone has other sources I've overlooked, or other useful Google Group posts, you can add them to this thread.

Norm

[David A. Wheeler]

On Sun, 18 Dec 2016 10:21:09 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> I agree that this should be documented in a way that is easy to find, but

> mmset.html is getting uncomfortably long....

I'm not sure what the length issue is. All browsers handle the current page trivially.

> A supplementary page covering
> the language and markup conventions may be better, linked to on mmset.html
> and referenced at relevant points in the mmset body.

If you'd prefer that, sure, let's do that!

>... If anyone else wants to start such a page I can review it, make corrections,

> and add missing material. Another auxiliary page such as Real and Complex
> Numbers could be used as a starting template for a uniform appearance.

Sure, I'd be happy to start that. No doubt there will *always* be *something* missing -
so let's create something useful, and that can always be improved.

I have to first finish grading my classes (I teach grad classes at GMU), hopefully that will
only be a few more days!!

--- David A. Wheeler

[Norman Megill]

On Sunday, December 18, 2016 at 3:39:32 PM UTC-5, David A. Wheeler wrote:

On Sun, 18 Dec 2016 10:21:09 -0800 (PST), Norman Megill wrote:
> I agree that this should be documented in a way that is easy to find, but
> mmset.html is getting uncomfortably long....

I'm not sure what the length issue is.  All browsers handle the current page trivially.

Nothing to do with browser capability.  It's a matter of whether too much information overwhelms a newcomer.  I would say it's pushing that limit (although no one has actually complained yet).

I dislike sites that have zillions of tiny pages for no apparent reason (except maybe to serve up more ads) - hard to search, hard to skim, and continually locating and clicking the Next link at the bottom wastes time and tires the finger.  Sometimes the documentation on a site gives a choice of reading the manual all at once or section by section linked from a table of contents.  I always choose "all at once."  So I made the MPE Home Page into what I thought I would like to see, with everything relevant in one place.  But good things can be taken too far.

Also, a separate Language and Conventions page is something I would happily encourage active editing of, perhaps on Github, and it can have a primary author byline like the Metamath 100 page has.  OTOH the MPE Home Page, while not perfect, presents the material the way I want.  While I welcome suggestions (most recently, the Theory of Classes section was suggested by Gérard Lang), I prefer to have control of it and not have to disappoint people by rejecting well-intentioned but misguided edits.
 

> A supplementary page covering
> the language and markup conventions may be better, linked to on mmset.html
> and referenced at relevant points in the mmset body.

If you'd prefer that, sure, let's do that!

>...  If anyone else wants to start such a page I can review it, make corrections,
> and add missing material.  Another auxiliary page such as Real and Complex
> Numbers could be used as a starting template for a uniform appearance.

Sure, I'd be happy to start that.  No doubt there will *always* be *something* missing -
so let's create something useful, and that can always be improved.

I have to first finish grading my classes (I teach grad classes at GMU), hopefully that will
only be a few more days!!

No hurry of course; whenever you are ready.  As you've probably figured, it's going to take some time to study, organize, and vet the various sources I mentioned as well as finding others I missed.  I don't think we have to go overboard with source hyperlinks or have any at all, and anything I wrote can be copy/pasted without acknowledgment.  But it may be occasionally useful to have the source URL embedded as an HTML comment in case we want to double check something.  Sometimes it may be useful to link to say the relevant Google Group discussion to provide context for something that seems unclear, unresolved, or uncertain.

Norm

[David A. Wheeler]

On Sun, 18 Dec 2016 14:56:39 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> Also, a separate Language and Conventions page is something I would happily

> encourage active editing of...

I've started looking at gathering the language and conventions information for MPE,
and I'm immediately struck by an obvious problem: it has to refer
to a lot of mathematical symbols. I could do this directly in HTML as an appendix, but:
* it's a pain to do this directly in HTML
* it won't generate GIF vs. Unicode easily
* it's all too easy over time to generate symbols that will look *different* than the
actual generated HTML pages, especially when an htmldef changes, and
* there's no easy way to tell metamath to apply `...` to standalone pages.
As a separate page it'll be more likely for it to go out-of-sync, too.

Instead of a true stand-alone page, how about creating a new "theorem" called
"conventions", where the comment documents conventions.
This is just like "mathbox" - and I expect I'd again prove |- x = x .
It could be anywhere in the document, e.g., near the beginning to explain things,
or just before "mathbox" - we could even move it later.
Then *clearly* it will match the generated symbols - and if an htmldef changes,
it will change to match.

If that's okay, I'll create an early draft of "conventions" so we can see what it looks like.

--- David A. Wheeler

[David A. Wheeler]

(Replying to myself)

I've now created a git branch "conventions" of set.mm that creates a new
"conventions" theorem, whose real purpose is to document the conventions
in way easily read by people who just look at the generated HTML.

Early draft here:
https://github.com/metamath/set.mm/tree/conventions

Comments welcome. It currently generates a lot of these warnings:
?Warning: No page number after [<author>] bib ref in "conventions".
and I haven't figured out how to turn them off (?).

--- David A. Wheeler

[Norman Megill]

This is always required for bib refs in a statement description, which are normally used to locate a definition or theorem in a book or article.  There is no way to turn this off, and I don't think we want to otherwise people would just reference a 500-page book without bothering to look up the page number - a pet peeve of mine when authors do this in the literature.  Once I wasted a couple of hours going through every page of a book for a proof said to be there, not knowing if it was expressed with different terminology or notation, and in the end not finding it.  But the real reason is that otherwise there would be no page number for the mmbiblio.html page.

A workaround is the put the comment under a section header, where the page number is not required, since those aren't included on the mmbiblio.html page.

As to whether the conventions should permanently be in set.mm, it's fine for right now and we can decide what to do later once it stabilizes.  More than once I've used 'show statement ... /html' to generate text to copy/paste onto a web page like MPE home.  I understand the advantage of labels etc. being automatically updated if it's in set.mm.  OTOH a web page provides more flexibility in layout, figures, etc.

Norm

[David A. Wheeler]

> On Tuesday, December 27, 2016 at 4:57:33 PM UTC-5, David A. Wheeler wrote:
> > It currently generates a lot of these warnings:
> > ?Warning: No page number after [<author>] bib ref in "conventions".

On Tue, 27 Dec 2016 14:50:11 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> This is always required for bib refs in a statement description, which are

> normally used to locate a definition or theorem in a book or article...

> A workaround is the put the comment under a section header, where the page

> number is not required...

Okay, I did that. There were a few specific references, so I looked up the theorem & page numbers
and added them.

> As to whether the conventions should permanently be in set.mm, it's fine
> for right now and we can decide what to do later once it stabilizes.

Okay, I've done it as a pull request, so that someone else can look before
pulling the trigger:

https://github.com/metamath/set.mm/pull/90

> I understand the advantage of
> labels etc. being automatically updated if it's in set.mm. OTOH a web page
> provides more flexibility in layout, figures, etc.

The <HTML>...</HTML> workaround seems more than adequate. The only
thing I needed (that comments don't currently provide) is a mechanism for making a list.
At this point I think the "conventions" theorem should just stay in set.mm indefinitely.
It's much easier to update and keep consistent that way.

---- David A. Wheeler

[Norman Megill]

The us2 site has been updated with David's "conventions":
http://us2.metamath.org:88/mpeuni/conventions.html
Comments are welcome.

Norm