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.

Reply via email to