On Thursday, February 13, 2020 at 9:25:42 AM UTC-5, Benoit wrote: > > David: yes, ~bisymOLD and ~bi3antOLD should have both discouragement > tags. I'm away from my main computer... can you add them ? > > Actually, most *OLD and *ALT should probably have both discouragement tags > as well, it seems ? >
I think so. This can be checked by making sure all *OLD and *ALT labels have both discouragements in the 'discouraged' file. There might be rare exceptions for *ALT although I can't remember - e.g. we don't necessarily want to prevent a shorter proof for a *ALT that occurs before the non-ALT. I should look at each *ALT case with a missing discouragement. I don't think it's worth restarting the jobs at this point, nor use an updated set.mm for new jobs, because I'd prefer everything be based on a stable set.mm. There shouldn't be many cases, and I can address them individually for the final minimize run. In the meantime, we can update set.mm independently - that will automatically "fix" some of them for the final run, since 'prove' will not allow discouraged theorems by default, and my final script will tolerate that rejection. The ones that have to be addressed manually are those where a *OLD/ALT was used to minimize a proof. 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/a6c9cbf0-ebb0-4971-b2d2-543b64f1e36e%40googlegroups.com.
