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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/E1j20DJ-0005li-6I%40rmmprod07.runbox.
