The bug is fixed, and I updated the metamath program to version 0.181. It has been updated on us2 http://us2.metamath.org/index.html#mmprog and github. I will post about restarting the job runs in a separate post. We might as well start from the most recent set.mm, and I will re-create the job files for it (after I have some dinner).
Per request of Giovanni (see https://groups.google.com/d/msg/metamath/uSa8Q0fWKeM/9dDcUM-DCwAJ ) I also did the following. I assume this is still desired? git commit -m'Release version 0.181.' git tag v0.181 git push git push --tags Here is a description of the bug and its impact. In November (version 0.179 29-Nov-2019) I changed 'minimize' to use the MM-PA proof in progress instead of the saved proof. This was done to avoid the need to 'save new_proof' before running 'minimize'. To speed up 'minimize', the (relatively slow) trace_back algorithm is called only when it is needed to test whether a proposed minimization match uses a new axiom. The results of this trace_back call are saved so that it will be done at most once during a 'minimize' run. As a result of the November mod, when the trace_back algorithm is called, it is now handed the proof in progress instead of the saved proof. The mistake was that I overlooked that the proof in progress was modified by the proposed minimization at that point, and instead I should have handed trace_back an earlier saved version of the proof in progress. Therefore, any 'minimize' runs done between 29-Nov-2019 and now are suspect. For most proofs it shouldn't matter, but for ones such as axdc that study axiomatizations, it was a serious bug. If you ran 'minimize' on one of these, you probably want to check that the axioms being used are the ones you wanted. Note the following: When the bug was present, a theorem using a new axiom would be brought into the proof if and only if it was the *first* statement matched by 'minimize'. The second and later matches, if any, would not bring in new axioms. So if, for example, 'minimize' on axdc first matched syl5eq, it would then later correctly reject ax-dc. In other words, sometimes a new axiom would be accepted and other times it wouldn't, depending on the order in which the match occurred. Norm On Wednesday, February 12, 2020 at 12:52:38 PM UTC-5, Norman Megill 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 > > -- 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/60d3afc2-17c2-4d48-8734-cccb46229e2a%40googlegroups.com.
