On Wednesday, February 12, 2020 at 5:10:34 PM UTC-5, David A. Wheeler wrote:
> While we're waiting for the tweaks to metamath.exe to fix the 
> minimize bug, below is a quick shell script I wrote to do this for 
> Linux/Unix. 
> If you store this as file "jobs" and make it executable ("chmod a+x 
> jobs"), 
> you can run in parallel jobs 120 through 128 by running: 
> jobs 120 128 

I'm not sure how often it will happen, but I anticipate that the jobs may 
not always be in order.  In particular, jobs 133-160 are almost certainly 
going to take very large and unpredictable amounts of time, and with some 
users giving up on some of them, there are bound to be gaps.  Even 101-132 
might run into unexpectedly long runtimes where a user gives up in the 
middle, and someone else will need to run say job130b.cmd to finish the 
rest of it.

Aside from that, thanks for putting this together!


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 

Reply via email to