>
>
>
> 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/9c507624-f059-4eba-91ec-7b87e877707e%40googlegroups.com.

Reply via email to