Yes, I forgot to include /time, which was also used in the runs 2 years ago. I had in mind finding a function that correlated proof size and set.mm position to run time (at least roughly) to help plan jobs with more predictable run times, but I never got around to it. I still have the data, though.
No, /verbose is primarily for me to help with debugging. I think it might confuse the current script that assembles all the log files into the final minimize run. Norm On Tuesday, December 17, 2019 at 4:46:55 PM UTC-5, Benoit wrote: > > The basic idea is to run 'minimize */a */n ax-*' on each proof and send >> the results (in a log file) to me, without saving the proof. >> > > Maybe add the options /VERBOSE /TIME to have all the information possible. > > Benoît > > -- 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/2e07812f-9ffb-4b71-82ac-31ccdd9c0501%40googlegroups.com.
