I'm not hitting memory limits so far, I expect this to be CPU limited not memory limited.
I may create a new version of this script using GNU make. GNU make has built-in mechanisms to maximally run as many jobs as reasonable, and starts next jobs as each one completes. If you're only running as many jobs as there are CPUs that won't matter, but if you plan to process more jobs than that, that approach might improve the throughput of the jobs. --- David A.Wheeler -- 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 https://groups.google.com/d/msgid/metamath/AB5C3E22-4A69-454C-BB3F-A92383CEF72F%40dwheeler.com.