On Sun, 12 Apr 2020 08:38:06 -0700 (PDT), savask <[email protected]> wrote: > Maybe the introduction of mmj2 is a good candidate for an important event?
Good idea. I'm struggling to find the exact date of its introduction. Below is my effort to find that date; if someone has better information, please let me know! While I can't find the literal first date, it looks like an announcement of mmj2 on the metamath news, which was also the date of a revision of mmj2, was posted on Aug-30-2005. So I propose this: Aug-30-2005: mmj2 tool formally announced as Metamath news If someone has better information, please let me know! --- David A. Wheeler ==================================== A lot of the early stuff was posted on PlanetMath which is long-gone, making dating more difficult. First, looking at the current mmj2 (maintained by Mario), the mmj2 download file CHGLOG.TXT's earliest date is Aug-30-2005, but it's clearly documenting changes from an earlier version. The copyright statements generally say "2005-", so the first version was sometime earlier in 2005 or maybe a little earlier. On http://us.metamath.org/other/AsteroidMeta/metamath There's a posting by ocat on 17-Dec-2005 saying: "First, I would like to thank Planet Math and Asteroid Meta for hosting mmj2 and the Metamath+Friends discussion area. The kindness is appreciated greatly. And I would like to thank Norm Megill for inventing Metamath, thereby providing a source of endless amusement and educational benefits for people all over the world!" Again, that's evidence that it was 2005 or earlier. There's a mirror of lots of mmj2 info here, but I didn't find a lot of hints: http://us.metamath.org/other/AsteroidMeta/mmj2 I went back & got the currently-available file from Mel O'Cat: http://us2.metamath.org:88/downloads/mmj2-orig.zip Ignoring the .gif files that are clearly from an external site, the earliest dates I found were: -rw-r--r-- 1 dwheeler None 5606 May 13 2005 doc/GrammarRuleTreeNotes.html -rw-r--r-- 1 dwheeler None 40183 Oct 19 2004 doc/mmjProofVerification.html Of course, the software might not have been *released* on those dates. I looked over the Internet Archive, and in particular found this: https://web.archive.org/web/20060212080840/http://planetx.cc.vt.edu/AsteroidMeta/mmj2 ~~~~ Official mmj2 announcement at Metamath: http://us2.metamath.org:8888/mpegif/mmrecent.html#new "(30-Aug-05) Mel O'Cat has written a new proof verifier for the Metamath language, called mmj2. Written in Java, mmj2 meticulously enforces the strict Metamath spec and should provide a "gold standard" for ensuring the absolute correctness of the syntax and proofs in a Metamath database. (As noted in the footnote on p. 92 of the Metamath book, the current Metamath program implements an older, slightly looser syntax.) Together with Raph Levien's mmverify.py, there are now 3 independently-written proof verifiers." FYI, mmj2.html was updated today, Aug-30-2005 to absolutely state that Sun's JDK1.5 is required (until GNU Java has PriorityQueues?, Chained Exceptions, etc.) And mmj2.zip was updated with a few minor things like a CHGLOG.TXT. No biggie. ~~~~ -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jNfJ2-0003uT-K0%40rmmprod07.runbox.
