On Friday, February 14, 2020 at 4:15:56 PM UTC-5, David A. Wheeler wrote: > > On Thu, 13 Feb 2020 06:25:42 -0800 (PST), Benoit wrote: > > Actually, most *OLD and *ALT should probably have both discouragement > tags > > as well, it seems ? > > I looked at the .log files I have so far. Once I "cd" into metamathjobs/ > ... > > I have no proposed minimizations involving "OLD": > grep 'decreased' *.log | grep OLD > > But I do have some proposed minimizations involving "ALT": > grep 'decreased' *.log | grep ALT | uniq > > The list: > job129.log:Proof of "dral1ALT" decreased from 81 to 16 bytes using > "dral1". > job129.log:Proof of "dveeq2ALT" decreased from 41 to 15 bytes using > "dveeq2". > job132.log:Proof of "ax16nfALT" decreased from 45 to 16 bytes using > "ax16nf". > > I don't think we want to apply these minimizations :-). > > As a first cut, we might just skip anything involving ALT or OLD, then > look more carefully. > > At the least, we shouldn't use THEOREMT to prove THEOREMTALT. >
A simple way to fix this is to add "(Proof modification is discouraged.)" to dral1ALT, etc. as they should have anyway. Then the final 'minimize' run will skip them. There are also a number of "suspicious" minimizations on non-ALT/OLD theorems as can be seen with "grep 'to [12]. bytes' job*.log" e.g.: job102.log:Proof of "bj-abf" decreased from 45 to 12 bytes using "abf". job103.log:Proof of "hashssle" decreased from 370 to 19 bytes using "hashss". When everything is done, we will need to analyze these and decide what to do. We have a more serious problem though. ~dral1ALT is not in job129.cmd, it is in job124.cmd. When I checked, ~dral1ALT was in the old job129.cmd before the bug fix. In my post https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/odjUQM6nBAAJ I wrote that the min2020-jobs.zip file was updated, but it looks like your script kept the old version: # Download jobs if not already downloaded test -f min2020-jobs.zip || \ wget http://us2.metamath.org/downloads/min2020-jobs.zip Unfortunately these jobs will have to be rerun. The theorems in job133.cmd through job160.cmd were not changed so those runs shou OK. Norm -- 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/10e2d85d-8aca-4412-b260-0a8c16600fda%40googlegroups.com.
