Given about 8 hours a run for me, I'll take two batches of 8; 103-111 and 135 to 143.
On Wed, Feb 12, 2020, 6:42 PM Norman Megill <[email protected]> wrote: > On Wednesday, February 12, 2020 at 9:14:32 PM UTC-5, David A. Wheeler > wrote: >> >> Note that I don't use the metamath "log" capability, and use the >> Linux/Unix >> built-in redirection mechanisms instead. If that's a problem of some >> kind, >> let me know...! >> > > The beginning and end will be a little different. An advantage of the log > is that it shows the start and end times. My scripts to build the final > minimize run have been tested on the log format, although I don't expect > any problems. Is there a reason not to use the log, though, in order to > keep things consistent? People running on Windows will be using the log > format. > > In the line commented "Download jobs if not already downloaded", note that > min2020-jobs.zip was updated with the same name, so make sure that the old > one is deleted. > > Norm > > >> >> --- David A. Wheeler >> >> >> ===== scripts/jobs ================ >> #!/bin/sh >> >> # Run set of Metamath minimization jobs from $1 (start) through $2 (end). >> # The number of jobs is the environment variable NPROC if set, else # >> CPUs >> >> # Recommended setup: >> # git clone https://github.com/metamath/set.mm.git >> # cd set.mm >> # scripts/download-metamath >> # scripts/build-metamath >> # # check out the version we want to analyze >> # git checkout 87bc05d4155014c9bc7b8f4f05435347b628b7f0 # or whatever >> # git checkout -b jobs >> >> set -e -u >> die () { >> printf '%s\n' "$1" >&2 >> exit 1 >> } >> >> command -v metamath > /dev/null || 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 >> >> master_log='metamathjobs/master.log' >> >> echo >> echo 'Starting jobs. View job NUM with: tail -c +0 -f >> metamathjobs/jobNUM.log' >> echo "View overall state with: tail -c +0 ${master_log}" >> echo >> >> # We use "nproc" to find the number of CPUs if NPROC is not set. >> >> nohup make --jobs "${NPROC:-$(nproc)}" -r -f scripts/jobs.makefile \ >> first="$first" last="$last" > "$master_log" 2>&1 & >> >> echo >> echo 'Run "killall make metamath" to kill all processes.' >> echo >> >> >> >> ===== scripts/jobs.makefile ============= >> # Makefile to minimize Metamath proofs. Requires GNU make. >> >> all: alljobs >> echo 'DONE.' >> >> LOG_LIST := \ >> $(foreach num, $(shell seq $(first) $(last)), >> metamathjobs/job$(num).log) >> >> $(info LOG_LIST is $(LOG_LIST)) >> >> metamathjobs/job%.log: metamathjobs/job%.cmd >> echo "Running job $*" >> metamath 'read set.mm' "submit 'metamathjobs/job$(*).cmd'" quit >> \ >> > "metamathjobs/job$(*).log" 2>&1 >> >> alljobs: $(LOG_LIST) >> >> # Delete what's generated if a program returns a nonzero (error) result. >> # This can be annoying for debugging, but it means that we can simply >> re-run >> # make if a process is stopped. >> ifndef KEEP_ON_ERROR >> .DELETE_ON_ERROR: >> endif >> > -- > 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/06ad104d-1d7d-4d6e-9dac-706f5a4f4cc2%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/06ad104d-1d7d-4d6e-9dac-706f5a4f4cc2%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAMZ%3Dzj4eHJfWP3a%2B3vzBkT%2BuXO2P0Sva%2Bvaz1TrpM19vqHFjCg%40mail.gmail.com.
