I use the (spare) time while the minimization is running to relax or to write/improve the comments for the theorem I just have proven...
On Tuesday, December 17, 2019 at 7:02:30 PM UTC+1, fl wrote: > > >> >> Can metamath automatically use all the CPUs available when doing a >> minimize run? >> > > You simply launch several jobs. Each of them covers a different range of > set.mm. One job per CPU. > All the processors are at work this way.But it's getting hot. > > > > >> So you should not be afraid to run a minimization. >> >> > It might be better to ask people to minimize the proofs they made before > they send them. It is called parallel computing after all. > But I used to do that and it is boring. Minimizing one proof can take a > long time and you need to sit down > in front of your computer until it stops. A shell to manage a batch job > might help I think. > > -- > FL > -- 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/f1311e0a-16f4-4ffe-8e28-46d22c8c07a8%40googlegroups.com.
