Dates in set.mm

[Norman Megill]

To improve attributions and history in the set.mm database, we will start requiring a "(Contributed by...)" comment tag in every $p and in those $a's that have a turnstile "|-" i.e. ax-* and df-*.  "(Revised by...)" and "(Proof shortened by...)", which are now the only other kinds of tags, are optional.

Below each proof are one or two dates.  If there are two, the first should be the most recent.  The oldest date must match the "(Contributed by...)" date and if there are two, the newest date must match the most recent "(Revised by...)" or "(Proof shortened by...)".  Conversely, if there are one or more "(Revised by...)" and "(Proof shortened by...)" tags then there should be a second date below the proof.

The date(s) below the proof may eventually become obsolete since they are redundant.  But for now we can at least ensure that they are consistent.  Currently, the newest date below the proof determines the order of what appears on the Most Recent Proofs page.

The current metamath program (0.120, http://us2.metamath.org:88/index.html#mmprog) adds a new command, "verify markup *".  This will verify the above rules, and if you run it prior to a submission, it will save me time fixing the dates.  (Right now that is all this command does.  Someday I hope to add markup checking for ~ label, ` math string `, [bibref], and htmldefs.).

Only the set.mm database needs to conform to these rules.  They are recommended but optional in the other databases.

Norm

[David A. Wheeler]

If you're fiddling with dates anyway, may I suggest a switch from the current format (e.g., "18-Nov-05") to ISO date format (e.g., "2005-11-18")?

ISO date format (generally "YYYY-MM-DD") is language-independent, sorts nicely, and gracefully handles the future (in 2107 it won't be obvious when "05" is). More details about ISO 8601 are here, though you really don't need them: https://en.wikipedia.org/wiki/ISO_8601

Yes, that changes a lot of lines, but it's trivial to do automatically in the set.mm file.

--- David A. Wheeler

[Norman Megill]

Well, there are many opinions on this issue so it could become an interesting discussion.  :)

The ISO-8601 date format is very useful when ease of sorting is needed.  For example, I often append it to the file name to indicate an older version.

The problem with any all-numeric date format is potential day-month ambiguity.  Even ISO can be read wrong by non-computer people.  My parents, for example, would likely guess it wrong since they are used to mm/dd/yy from U.S. friends and dd-mm-yy (with dashes or periods) from overseas friends.

I don't know the origin of the format [d]d-Mmm-yyyy, but it was the date standard for DEC's VMS in the 1990s.  Because I started Metamath development on this system, I chose that format for set.mm and the date functions in the metamath program.

A 3-letter month abbreviation does have the disadvantage of being specific to the English language.  However, the abbreviation is nearly identical in most Romance and Germanic languages, as well as Esperanto, so it should be recognizable to almost anyone with minimal exposure to one of those languages.

From my personal perspective, even though the ISO format is completely unambiguous and I know what it means, there there still is that ever-so-slight moment of distraction to register that 2000-01-02 is January and not February.  Basically I see ISO as computer friendly and an alphabetic month as human friendly.

The dates in almost all legal documents have the month spelled out to eliminate potential ambiguity.  Strunk and White's Elements of Style says, "6 April 1958...is an excellent way to write a date; the figures are separated by a word and are, for that reason, quickly grasped."

As for 2-digit years, the only place they occur in set.mm is in the "Recent label changes" list, in order to provide two extra columns on the line.  As its name suggests, it is primarily intended to identify "recent" changes to help people update their local work.  In 100 years, ambiguity can be resolved by looking at the date tag in a referenced theorem.

Norm

[Norman Megill]

On Saturday, November 14, 2015 at 10:09:27 AM UTC-5, Norman Megill wrote:

The current metamath program (0.120, http://us2.metamath.org:88/index.html#mmprog) adds a new command, "verify markup *".  This will verify the above rules, and if you run it prior to a submission, it will save me time fixing the dates.  (Right now that is all this command does.  Someday I hope to add markup checking for ~ label, ` math string `, [bibref], and htmldefs.).

Version 0.121 now adds all these checks to 'verify markup'.  The qualifier /date_skip can be used with non-set.mm databases not requiring date consistency, and /file_skip checks all it can without requiring the presence of external files (GIFs, mmset.html, mmbiblio.html).

Norm