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. On October 2, 2019 10:06:17 AM PDT, "David A. Wheeler" <[email protected]> wrote: >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. -- 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/436C2780-A366-4217-9A83-AA7135AB4B93%40panix.com.
