All my jobs but 103 completed overnight.

On Wed, Feb 12, 2020, 9:52 AM Norman Megill <n...@alum.mit.edu> 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 metamath+unsubscr...@googlegroups.com.
> 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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/CAMZ%3Dzj7O1h%3DkYFivs92S%3D_ATj_sgpByTEaY7h3Kn4A12CbNX1A%40mail.gmail.com.

Reply via email to