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!
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/3935cd4b-7af5-4002-9761-0feb1ccfd1eb%40googlegroups.com.
