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 My suggested setup is slightly different, see the comments below. I share this in the hopes it'll be useful. I have access to an 8 CPU 128GB machine that should help in this little quest. I'll probably eventually propose a variant like this for the "scripts/" directory. If people have comments, let me know. --- David A. Wheeler ============== File "jobs" ======================== #!/bin/sh # Run set of Metamath minimization jobs from $1 (start) through $2 (end). # Recommended setup: # git clone https://github.com/metamath/set.mm.git # cd set.mm # scripts/download-metamath # scripts/build-metamath # git checkout 59bd588e52523db5238db18241e518941112ea34 # git checkout -b jobs set -e -u die () { printf '%s\n' >&2 exit 1 } command -v metamath || die 'Metamath program not on path' [ "$#" = 2 ] || die 'Requires exactly 2 parameters, the start and end job #s' first="$1" last="$2" # Download jobs if not already downloaded test -f min2020-jobs.zip || \ wget http://us2.metamath.org/downloads/min2020-jobs.zip # unzip if not already unzipped test -d metamathjobs || unzip min2020-jobs.zip for num in `seq $first $last`; do logfile="metamathjobs/job${num}.log" echo "Starting job $num. View with: tail -c +0 -f ${logfile}" # Instead of using Metamath 'open log', use redirection to capture everything nohup time metamath 'read set.mm' "submit 'metamathjobs/job${num}.cmd'" \ quit > "$logfile" 2>&1 & done echo echo 'Run "killall metamath" to kill all processes.' echo -- 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/E1j20DJ-0005li-6I%40rmmprod07.runbox.