"David A. Wheeler" <[email protected]> wrote:
> 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
For what it's worth, there's a bit of git-fu that lets you grab a file from a
commit without having to do a checkout:
$ git -C /path/to/metamath/repo show 87bc05d4:set.mm >/where/to/save/set.mm
See git-show(1) for details, but that's the essence. This makes it easy to do
the jobs in a temporary directory, without interfering with repo usage at all,
so you can essentially keep working as normally if need be.
>
> # 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 <[email protected]>
> 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 [email protected].
> > 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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/3LI90R0NVQVNR.3IQS2GKYQOZMG%40wilsonb.com.
