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 <[email protected]>
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).
--
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/E1iFi4v-0006A8-NQ%40rmmprod07.runbox.
