(Switching to the mininmize thread) On Tuesday, December 17, 2019 at 12:46:30 PM UTC-5, David A. Wheeler wrote: > > > >The last one I did myself was around 3 years ago, using a laptop with a > >powerful i7 processor maxed out with 8 threads. > > Can metamath automatically use all the CPUs available when doing a > minimize run?
metamath.exe can only use one core, and as FL said you have to run separate processes, doing it in pieces. (I'm not sure how that would be done in the program, but I would guess it would involve system-specific calls, making it non-ANSI.) > > > The CPU ran quite hot > >(Speccy reported around 90-95C even with a new fan), and it died near > >the end. > > All systems have temperature measures that should prevent any permanent > damage and automatically slow down as necessary. Also, some modern > computers are designed to run absurdly hot. Yes, some systems have defects > in their temperature measurement systems, but those should be relatively > rare. So you should not be afraid to run a minimization. The laptop was an HP 8570p. IIRC the CPU was spec'ed to run up to 100C, so it probably was throttling. However, keeping that high continuously for weeks may have shortened its life. I think I've seen a recommendation to keep CPUs under 80C for long life. I just checked out the us2 server, and maxing the CPU (4 processes) raised the temperature to 83C (in a cool room at 18C), which seems high and makes me uncomfortable. It may have a bad fan, but I would have to shut down us2 to find out and fix. When I ran one process (such as the site build), the temperature increased to only 50C, so I can postpone looking into this until there's a slow period for contributions. > > I might be able to run minimization on a useful beefy system, but I'll > have to check first. > I'll update the script I gave to Dylan Houlihan and post it somewhere, and people can do whatever parts they want, with some informal coordination with me. 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. After I collect all the results, I will create a one-off script to do the actual proof updating. The actual updating is fast because 'minimize' is run against single theorems, and it will be a one-time change to set.mm. There's no rush for doing this. Even if set.mm changes in the interim, worst case it just means some minimizations may not happen, but they will catch up in the next year's round. I'll wait until the proposed moves of mm100 theorems etc. to the main set.mm are completed so it can be as accurate as possible. 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/0553e848-2d46-4473-85ad-15c9b320b6b3%40googlegroups.com.
