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.
