Any other major Metamath/set.mm events?

[David A. Wheeler]

I intend to eventually re-run Gource to visualize the progress of set.mm.
Many things have happened, and there are a lot of corrections to the
dates of the early theorems (my thanks to Norm for tracking that down!).

Are there any other "major events" in Metamath/set.mm that aren't well-captured?
The current list is here: https://github.com/metamath/set.mm/blob/develop/scripts/gource-captions.txt

For example:
* I think the OpenAI proofs are important - does this text capture things well?:
"OpenAI provides first contribution of a Metamath proof created/minimized via machine learning"
* I don't know what the "right" date is for extensible structures - can anyone suggest something?
df-struct was contributed by Mario Carneiro on 29-Aug-2015, yet the
structure component index extractor df-ndx was contributed earlier by NM on 4-Sep-2011.
Suggestions on a date - and what to say - about adding extensible structures would be welcome.
* What important events are missing, especially when nothing else happens near those times?

Tooting your own horn is fine, just make sure it's a good note :-).

--- David A. Wheeler

[savask]

Maybe the introduction of mmj2 is a good candidate for an important event?

[David A. Wheeler]

On Sun, 12 Apr 2020 08:38:06 -0700 (PDT), savask <sav...@yandex.ru> 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.
~~~~