Thank you, Alexander and Glauco. I'd like to hear from Benoit and Wolf who have a number of theorems in these lists. After than I'll organize it into the final list of actions we'll take. (I will probably do the necessary editing of set.mm myself to prevent confusion or conflict.)
Here are some more ALT cases (with duplicates removed): $ grep 'using ".*ALT"' j*g job116.log:Proof of "climf" decreased from 873 to 872 bytes using "rexbidvALT". <- use rexbidv instead job147.log:Proof of "fourierdlem65" decreased from 9585 to 9567 bytes using "rexbidvALT". <- use rexbidv instead $ grep 'Proof of "ALT" decr' j*g job119.log:Proof of "ismgmALT" decreased from 199 to 151 bytes using "elab2g". <- Alexander: I assume this is ok to do? Norm On Thursday, February 20, 2020 at 10:28:24 PM UTC-5, Norman Megill wrote: > > All jobs from 101 to 158 have completed. Many thanks to all who > contributed CPU time! Jobs 159 and 160 are still running, but we will > handle those manually later. Therefore we are ready to start the final > analysis. > > I put all of the logs except 159 and 160 here: > http://us2.metamath.org/downloads/min2020-logs.zip > > Other links for reference: > 'minimize' scripts: http://us2.metamath.org/downloads/min2020-jobs.zip > Job status: > https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/odjUQM6nBAAJ > Estimates vs. actual run times: > https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/WmovUJiKBAAJ > 2018 'minimize' scripts: > http://us2.metamath.org/downloads/min2018-jobs.zip > 2018 logs: http://us2.metamath.org/downloads/min2018-logs.zip > <http://us2.metamath.org/downloads/min2018-jobs.zip> > Before performing the final minimize run, we need to make sure it will do > what we expect. Below are some greps I used to flag some unusually large > size reductions that we probably want to look at. (The 'uniq' is to get > rid of identical lines from the forward and backward 'minimize' scans. I > also edited out some duplicates where the 'from' number was different for > the two scans, as well as a couple that I will take care of myself.) If > anyone identifies other suspicious minimizations (with better grep ranges, > manual inspection of the logs, etc.), please post here. > > Many of the suspect cases are in various mathboxes, and it would be best > if mathbox users review the minimizations done on their mathboxes. > > We should edit set.mm to prevent unwanted minimizations rather than > editing the final minimize job, so that we don't have to do this same > analysis for next year's run. For example, ~ eqeq1dALT should have "(Proof > modification is discouraged.)" in its description to prevent overwriting > its proof with ~ eqeq1d. > > I'm not sure what the best way to maintain the results of the analysis. > Google Documents is a possibility, but I've never used it; someone else > would have to volunteer to set it up and post instructions for people like > me. Alternately, I could maintain a fixed post that I edit as people > respond to this post, like I did for the job status - maybe I'll start off > doing that. > > In the end I'd like to have each minimization accompanied by a > recommendation e.g. > > job128.log:Proof of "fprodshft" decreased from 1054 to 209 bytes using > "mptfzshft". > Resolution: ok (NM) > > job101.log:Proof of "eqeq1dALT" decreased from 144 to 17 bytes using > "eqeq1d". > Resolution: discourage proof modification of eqeq1dALT (WL) > > The initials would indicate who analyzed the case and, if not ok, who will > make the modification to set.mm. > > Norm > > > > $ grep '[0-9]... to [1-3].. bytes' job*.log | uniq > job128.log:Proof of "fprodshft" decreased from 1054 to 209 bytes using > "mptfzshft". > > $ grep '[2-9].. to [4-9]. bytes' job*.log | uniq > job102.log:Proof of "ncolne2" decreased from 304 to 53 bytes using > "ncolcom". > job104.log:Proof of "gsumsn2" decreased from 351 to 45 bytes using > "gsumsnd". > job109.log:Proof of "fz0hash" decreased from 207 to 98 bytes using > "hashfz0". > job115.log:Proof of "signswbase" decreased from 257 to 86 bytes using > "grpbase". > job132.log:Proof of "euhash1" decreased from 514 to 93 bytes using > "hashen1". > job154.log:Proof of "fourierdlem45" decreased from 5709 to 53 bytes using > "ioodvbdlimc1lem > > $ grep 'to [1-3]. bytes' job*.log | uniq > job101.log:Proof of "bj-bi3ant" decreased from 84 to 21 bytes using > "bi3antOLD". > job101.log:Proof of "eqeq1dALT" decreased from 144 to 17 bytes using > "eqeq1d". > job102.log:Proof of "bj-abf" decreased from 45 to 12 bytes using "abf". > job102.log:Proof of "frege53aid" decreased from 58 to 33 bytes using > "com12". > job102.log:Proof of "ifeq123d" decreased from 174 to 25 bytes using > "ifbieq12d". > job102.log:Proof of "mplrcl" decreased from 170 to 38 bytes using > "strov2rcl". > job103.log:Proof of "frege24" decreased from 55 to 19 bytes using > "rp-frege24". > job103.log:Proof of "hashssle" decreased from 447 to 19 bytes using > "hashss". > job103.log:Proof of "tsor2" decreased from 55 to 39 bytes using "imori". > job104.log:Proof of "aevALT" decreased from 90 to 14 bytes using "aev". > job104.log:Proof of "frege25" decreased from 55 to 20 bytes using > "rp-frege25". > job104.log:Proof of "tsor3" decreased from 59 to 39 bytes using "imori". > job106.log:Proof of "gsumsndf" decreased from 351 to 29 bytes using > "gsumsnfd". > job107.log:Proof of "perpdrag" decreased from 420 to 36 bytes using > "perpdragALT". > job108.log:Proof of "leimnltd" decreased from 50 to 19 bytes using > "lensymd". > job108.log:Proof of "orcomdd" decreased from 60 to 31 bytes using "syl6". > job109.log:Proof of "bj-bisym" decreased from 39 to 18 bytes using > "bisymOLD". > job109.log:Proof of "fseq0hash" decreased from 88 to 16 bytes using > "ffzohash". > job109.log:Proof of "symgfixfvh" decreased from 116 to 32 bytes using > "fvtresfn". > job110.log:Proof of "bj-hbsb3" decreased from 50 to 15 bytes using "hbsb3". > job110.log:Proof of "bj-nfs1" decreased from 42 to 14 bytes using "nfs1". > job110.log:Proof of "frege55aid" decreased from 30 to 14 bytes using > "bicom1". > job110.log:Proof of "sbequ8ALT" decreased from 72 to 15 bytes using > "sbequ8". > job111.log:Proof of "frege55b" decreased from 138 to 15 bytes using > "equcomi". > job112.log:Proof of "equsb3ALT" decreased from 96 to 15 bytes using > "equsb3". > job112.log:Proof of "rp-simp2" decreased from 33 to 14 bytes using "simp2". > job113.log:Proof of "rp-simp2-frege" decreased from 39 to 34 bytes using > "rp-a1i". > job114.log:Proof of "cleqf" decreased from 59 to 35 bytes using "nfcrii". > job114.log:Proof of "vdgfrgra0" decreased from 495 to 17 bytes using > "vdfrgra0". > job115.log:Proof of "AnelBC" decreased from 61 to 32 bytes using "nelir". > job115.log:Proof of "nfnfcALT" decreased from 89 to 15 bytes using "nfnfc". > job116.log:Proof of "rexbidvaALT" decreased from 26 to 20 bytes using > "rexbidva". > job116.log:Proof of "sbceq1ddi2" decreased from 105 to 38 bytes using > "sbceq1ddi". > job116.log:Proof of "wl-equsal" decreased from 86 to 18 bytes using > "equsal". > job117.log:Proof of "adant423" decreased from 56 to 39 bytes using > "sylancom". > job117.log:Proof of "frege39" decreased from 56 to 34 bytes using > "rp-frege2i". > job117.log:Proof of "rexbidvALT" decreased from 25 to 19 bytes using > "rexbidv". > job118.log:Proof of "pirp2" decreased from 72 to 30 bytes using "elrpii". > job119.log:Proof of "rp-frege2ii" decreased from 47 to 37 bytes using > "rp-frege2i". > job120.log:Proof of "eleq2dALT" decreased from 165 to 17 bytes using > "eleq2d". > job120.log:Proof of "frege57aid" decreased from 58 to 11 bytes using "bi2". > job120.log:Proof of "impel" decreased from 61 to 35 bytes using "syl2anr". > job120.log:Proof of "rp-frege2iii" decreased from 51 to 32 bytes using > "rp-frege2ii". > job122.log:Proof of "cbvald" decreased from 41 to 34 bytes using "nfvd". > job123.log:Proof of "ex3" decreased from 53 to 35 bytes using "3impa". > job124.log:Proof of "3expc" decreased from 26 to 16 bytes using "exp31". > job124.log:Proof of "dral1ALT" decreased from 81 to 16 bytes using "dral1". > job124.log:Proof of "frege58bcor" decreased from 64 to 16 bytes using > "spsbim". > job125.log:Proof of "dveeq2ALT" decreased from 41 to 15 bytes using > "dveeq2". > job125.log:Proof of "tgiooss" decreased from 218 to 17 bytes using > "rerest". > job125.log:Proof of "wl-sb6nae" decreased from 63 to 13 bytes using "sb4b". > job126.log:Proof of "adantlllr" decreased from 47 to 21 bytes using > "adantl3r". > job126.log:Proof of "ax12a2" decreased from 55 to 26 bytes using "ax12v". > job127.log:Proof of "absnpncand" decreased from 148 to 21 bytes using > "abs3difd". > job127.log:Proof of "ad5ant1345" decreased from 54 to 21 bytes using > "adantl3r". > job127.log:Proof of "ax16nfALT" decreased from 45 to 16 bytes using > "ax16nf". > job130.log:Proof of "bf-frege55a" decreased from 73 to 23 bytes using > "bj-frege55lem2a". > job130.log:Proof of "bj-csbprc" decreased from 157 to 15 bytes using > "csbprc". > job130.log:Proof of "nn0ge2m1nnALT" decreased from 172 to 17 bytes using > "nn0ge2m1nn". > job131.log:Proof of "bf-frege55cor1a" decreased from 74 to 14 bytes using > "bicom1". > job131.log:Proof of "ccat2s1fvwALT" decreased from 477 to 21 bytes using > "ccat2s1fvw". > job131.log:Proof of "wl-sbal1" decreased from 97 to 15 bytes using "sbal1". > job132.log:Proof of "4an31" decreased from 67 to 37 bytes using "sylanb". > job132.log:Proof of "frege52b" decreased from 42 to 16 bytes using > "sbequi". > job132.log:Proof of "wl-sbal2" decreased from 97 to 15 bytes using "sbal2". > > -- 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/46faae28-79e9-45f6-901e-767b4f8fbdc8%40googlegroups.com.
