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.