Verifying nnawordi / omssadd history

[David A. Wheeler]

I'm trying to verify the correct history of nnawordi - formerly known as omssadd.
Can anyone help me?
I especially would like to hear from Scott Fenton, Mario, and/or Norm, but
if anyone knows anything more I'd like to hear it.

Here's the issue. Currently set.mm says:

$d A x y $. $d B x y $. $d C x y $.
$( Adding to both sides of an inequality in ` _om ` (Contributed by Scott
Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 12-May-2012.) $)
nnawordi $p |- ( ( A e. _om /\ B e. _om /\ C e. _om ) ->
( A C_ B -> ( A +o C ) C_ ( B +o C ) ) ) $=

But I think that is mistaken. Based on info I've gathered below,
I suspect that Scott Fenton *also* did the revision of nnawordi
on 12-May-2012 and not Mario. I'm at least fairly confident that Mario didn't do it.

I think what happened is
that Mario made a commit that renamed omssadd into nnawordi ,
and later processing noticed a missing "revision" that was probably supposed to be
Scott Fenton's but since that info was missing the processing assigned credit
to the person who made the commit (Mario).

But I could be mistaken, so details below & suggestions appreciated.

--- David A. Wheeler

============ DETAILS ============================

Here are detailed facts (and how I've collected them)
that lead me to this conclusion. That said, it's not
conclusive, so I'm hoping someone can confirm it more strongly.

If first verified that
Ii commit 964590ec44fbb23b9949aee229246c116ea51282
stable release, archive name set.mm.2013-09-10

There is no nnawordi, but we do have this matching theorem:
$d A x y $. $d B x y $. $d C x y $.
$( Adding to both sides of an inequality in ` om ` $)
omssadd $p |- ( ( A e. om /\ B e. om /\ C e. om ) ->
( A C_ B -> ( A +o C ) C_ ( B +o C ) ) ) $=
...
$( [12-May-2012] $) $( [16-Apr-2012] $)

So clearly something got renamed.
To find where nnawordi was first renamed, I used "git bisect".
I document the process here so it can be reused.
Basically, I pretended that adding "nnawordi" was bad, and then
asked where the bad commit occurred:

# Find where nnawordi was created
cat > omits-nnawordi << END
#!/bin/sh
! grep ' nnawordi .p ' set.mm
END
chmod a+x omits-nnawordi
git bisect start
git bisect bad 1fd41ef22614a998e1f97ea57e29ce9cb9d7502c
git bisect good 964590ec44fbb23b9949aee229246c116ea51282
git bisect run ./omits-nnawordi

This reported:
3de364e88fae63ee75ca638622d3324368c0140f is the first bad commit
commit 3de364e88fae63ee75ca638622d3324368c0140f
Author: Mario Carneiro <di....@gmail.com>
Date: Mon Dec 1 06:23:55 2014 -0500

clean up ax-rep

In this commit nnawordi is credited to *just* Scott Fenton...
even though this is a commit by Mario.

$d A x y $. $d B x y $. $d C x y $.
$( Adding to both sides of an inequality in ` om ` (Contributed by Scott
Fenton, 16-Apr-2012.) $)
nnawordi $p |- ( ( A e. om /\ B e. om /\ C e. om ) ->
( A C_ B -> ( A +o C ) C_ ( B +o C ) ) ) $=
....
$( [12-May-2012] $) $( [16-Apr-2012] $)


The previous commit e2363e04ce6bf979ad984304624e9b77c5f36c85
"stable release, archive name set.mm.2014-11-30-so-substr"
Has this:

$d A x y $. $d B x y $. $d C x y $.
$( Adding to both sides of an inequality in ` om ` (Contributed by Scott
Fenton, 16-Apr-2012.) $)
omssadd $p |- ( ( A e. om /\ B e. om /\ C e. om ) ->
( A C_ B -> ( A +o C ) C_ ( B +o C ) ) ) $=
...
$( [12-May-2012] $) $( [16-Apr-2012] $)

Earlier commit 00e7d63218baae4264b593e60460aa8ed146d0cc
stable release, archive name set.mm.2012-05-21
has *NO* credits to anyone, but does have those same commit dates.
$d A x y $. $d B x y $. $d C x y $.
$( Adding to both sides of an inequality in ` om ` $)
omssadd $p |- ( ( A e. om /\ B e. om /\ C e. om ) ->
( A C_ B -> ( A +o C ) C_ ( B +o C ) ) ) $=
( vx vy com wcel wss coa co wi wa cv c0 csuc wceq opreq2 sseq12d imbi2d
weq con0 oa0 adantr adantl biimprd nnon syl2an word wb nnacl ancoms
adantrr syl eloni adantrl ordsucsssuc syl11anc biimpa nnasuc mpbird ex
imim2d a2d finds com12 3impia ) AFGZBFGZCFGZABHZACIJZBCIJZHZKZVIVGVHLZVNV
... $.
$( [12-May-2012] $) $( [16-Apr-2012] $)

I think what happened is that the item was added with the
date but without credit to Scott Fenton, credit to Scott Fenton
was added for contribution but not the revision, and then
Mario renamed it but there was a missing revision credit,
so that later processing looking to fill in the credit
assigned it to Mario (because it was renamed in that commit
by Mario).

[Jim Kingdon]

You'll presumably want to copy whatever you decide to http://us2.metamath.org/ileuni/nnawordi.html

Most of the attributions in iset.mm focus on changes to the theorem being proved, not to the proof, which is why this attribution is identical to the set.mm one.

[Norman Megill]

I commented on this case at
https://github.com/metamath/set.mm/pull/1141#issuecomment-537664085
Essentially both dates are Scott Fenton's, and the 2nd date should probably be removed for the reasons discussed there.

Also note that in early set.mm's, there were no acknowledgments in mathboxes, since it was assumed to be contributed by the mathbox owner.  When I moved a theorem to the main part of set.mm, I would add the acknowledgment.

Norm