All my jobs but 103 completed overnight. On Wed, Feb 12, 2020, 9:52 AM Norman Megill <[email protected]> wrote:
> This bug first appeared in version 0.179. I am still working on it; all I > know so far is that somewhere it is incorrectly marking ax-dc as already > used by the acdc proof. > > Anyway, we will have to discard the jobs already started. If any of them > finished, it would still be useful to post how long they ran, to give us an > idea of the run times we can expect for the others. Alexander told me > job101 took about 20 hr. BTW the first theorem in each job file always > ~3atlem4, which I will use to calibrate run times for CPU differences; in > his case 3atlem4 took 31 sec. > > I apologize for the work wasted and am very grateful to David Starner for > finding this before we got too deep into the job runs. > > Norm > > On Wednesday, February 12, 2020 at 8:18:44 AM UTC-5, Norman Megill wrote: >> >> On Wednesday, February 12, 2020 at 5:53:59 AM UTC-5, Alexander van der >> Vekens wrote: >>> >>> On Wednesday, February 12, 2020 at 10:00:42 AM UTC+1, David Starner >>> wrote: >>>> >>>> There might be an error in the minimize command; it found that axdc >>>> has a much shorter proof using ax-dc, which is obviously true yet >>>> defeats the purpose of the axdc theorem ( >>>> http://us.metamath.org/mpegif/axdc.html ) and uses new axioms for that >>>> theorem. >>>> >>>> I think ~axdc must be tagged with "(Proof modification is >>> discouraged.)", so that minimize will not touch its proof. This is not an >>> error of the minimize command. >>> >> >> David is right, there is something very wrong here. While ~axdc should >> be tagged with "(Proof modification is discouraged.)" but isn't, in any >> case 'minimize' should not be bringing in the new axiom ~ax-dc. >> >> We should hold off on any more runs until I determine what is happening >> and fix the program. Based on what I find, the jobs may have to be >> restarted. >> >> Thanks, David, this was a good observation. >> >> 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/0b405e55-4212-4d6c-b0ec-ba7ea1ffd5b6%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/0b405e55-4212-4d6c-b0ec-ba7ea1ffd5b6%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAMZ%3Dzj7O1h%3DkYFivs92S%3D_ATj_sgpByTEaY7h3Kn4A12CbNX1A%40mail.gmail.com.
