I've just posted an updated "jobs" system if you want to do big-scale minimization, especially if you're using a number of cores.
This version supports disjoint sets of jobs, e.g., you can now say: scripts/jobs 112 125-132 144-151 That means the API has changed, but I think it's for the better. Also, the log files it produces should be exactly what Norm expects (if it's not, please let me know so I can fix it). It's merged into the "develop" branch. A minor complication is that Norm wants the actual work to be done on an earlier commit (87bc05d41550). It's not complicated, git makes that easy, but only if you know how :-). Below is an example of how to do that with git. Let me know of any problems. It *seems* to work ;-). --- David A. Wheeler ========================================= # Set up git clone https://github.com/metamath/set.mm.git # if you don't have it cd set.mm git pull # Make sure you have the current version! # Ensure metamath is up-to-date scripts/download-metamath scripts/build-metamath # check out the version we want to analyze git checkout 87bc05d4155014c9bc7b8f4f05435347b628b7f0 # go back in time git checkout -b my_minimization # create a branch name for where you'll work # Extract the *current* version of the jobs scripts from develop branch git checkout develop -- scripts/jobs scripts/jobs.makefile # We're ready! Now plug in your JOB_NUMBERS, e.g.: # scripts/jobs 112 125-132 144-151 scripts/jobs JOB_NUMBERS # Wait a while. You can follow progress by running: tail -c +0 -f metamathjobs/master.log # You can stop tailing at any time with control-C; that won't stop work. # You'll eventually have a bunch of files named metamathjobs/jobNUMBER.log # You send those in. # When you're all done: git checkout develop =========================================== On Thu, 13 Feb 2020 14:28:54 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote: > Here is an update of current commitments as of Feb. 13, 17:30 EST : > > 101 Alexander > 102 heiphohmia > 103-111 David Starner > 112 David A. Wheeler > 113-124 UNASSIGNED > 125-132 David A. Wheeler > 133-134 UNASSIGNED > 135-143 David Starner > 144-151 David A. Wheeler > 152-160 UNASSIGNED > > Thierry has volunteered starting next week. > > David S., you mentioned "batches of 8" but your ranges have 9 each. Do you > want to adjust them or keep them as is? > > Norm > > -- > 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/67a1e124-4dc2-443d-89f2-d71e34793052%40googlegroups.com. -- 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/E1j2NlA-0004FU-GU%40rmmprod07.runbox.
