On Wed, 12 Feb 2020 17:57:39 -0800 (PST), Norman Megill <[email protected]> wrote: > The job files have been updated for today's set.mm. The new job files are > available at http://us2.metamath.org/downloads/min2020-jobs.zip
Thanks! I've quickly cobbled together an updated script & corresponding makefile (scripts/jobs and scripts/jobs.makefile) for Linux/Unix below. You can stick them in their respective places and run "chmod a+x scripts/jobs". Then if you want to process jobs 120 through 130 (inclusive), run: scripts/jobs 120 130 It'll run simultaneous processes (by default the number of CPU processors, set the environment variable NPROC if you want something different). Once a task is done, it'll run the next one, until all is done. You can run a single job easily enough: scripts/jobs 120 120 This is fresh out of my fingers, and not well tested yet. Feedback welcome. My plan is to eventually put this in the shared scripts directory so it'll be easier to do next time. 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...! --- 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/E1j241P-0003SB-5P%40rmmprod07.runbox.
