I've got a decent desktop sitting around because it's crashing when
the GUI is running; I'll try 103 through 111 (an 8-core system).

On Tue, Feb 11, 2020 at 3:48 PM heiphohmia via Metamath
<metamath@googlegroups.com> wrote:
>
> I only have a 10 year old laptop, so for now I picked up job102 and will
> contribute more if it seems reasonable.
>
> Happy minimizing!
>
> Norman Megill <n...@alum.mit.edu> wrote:
> > We are ready to do a full 'minimize' run on set.mm.  So you can fire up
> > your high-end gaming rigs for some serious work and help make the world a
> > better place through shorter proofs.  :)
> >
> > With the help of Saveliy's script mentioned at
> > https://groups.google.com/d/msg/metamath/djIdTu2Wq-I/mgs4MD7YDAAJ, I
> > partitioned the minimize run for all of set.mm into 60 scripts called
> > job101.cmd through job160.cmd.  They are contained in the file
> > http://us2.metamath.org/downloads/min2020-jobs.zip
> >
> > If you want to help out, let me know which scripts you want to commit to.
> > Until we have a better way of doing this, maybe it's easiest to handle it
> > informally and respond here with the job(s) you plan to work on so others
> > won't repeat the effort.  (GitHub might not be the best way to track this
> > since not everyone has an account there.)  If you don't want to post here,
> > email me privately and I'll update the public list.
> >
> > The purpose of these runs is to discover what minimizations will happen;
> > you won't be changing set.mm directly.  When finished, you would send me
> > (say by email for now) the job*.log file for each job you ran.  I will use
> > the log files to create the final 'minimize' run and also to collect run
> > time statistics to help improve future estimates.
> >
> >
> > Instructions
> > ------------
> >
> > You should use yesterday's set.mm which is at
> > https://github.com/metamath/set.mm/commit/59bd588e52523db5238db18241e518941112ea34
> > (click "..." in the set.mm row, then select "View file", then select
> > "Download").
> >
> > Assuming the 60 job*.cmd files (from the zip file above), set.mm, and
> > metamath[.exe] are in the same directory, you would type:
> >
> > Unix/Linux/Cygwin terminal 1:
> > ./metamath 'read set.mm' 'open log job101.log' 'submit job101.cmd/silent'
> > exit
> > Unix/Linux/Cygwin terminal 2:
> > ./metamath 'read set.mm' 'open log job102.log' 'submit job102.cmd/silent'
> > exit
> > ...
> > (etc. until for example cores or hyperthreads are filled up.)
> >
> > In a Windows Command Prompt you would type:
> > metamath "read set.mm" "open log job101.log" "submit job101.cmd/silent" exit
> >
> > On Linux, you can use 'tail -f job101.log' on a different terminal to
> > monitor the progress.  In the Windows Command Prompt, you can omit
> > "/silent" to monitor progress on the screen.
> >
> >
> > job101.cmd through job132.cmd
> > -----------------------------
> >
> > job101.cmd through job132.cmd each minimize around 1000 theorems and should
> > each take roughly the same amount of time (maybe around a day).  Within a
> > given .cmd file, the theorems are sorted starting from shortest estimated
> > run times, and the last theorem in each .cmd file is expected to have the
> > longest run time.
> >
> > If a job, say job101.cmd, seems to be taking too long and you run out of
> > patience, you can abort the job and send me the partial job101.log, which I
> > can still use.  I will then create job101b.cmd for the proofs that are
> > left, and someone else can continue with it.
> >
> >
> > job133.cmd through job160.cmd
> > -----------------------------
> >
> > job133.cmd through job160.cmd each minimizes a single big proof. job133.cmd
> > is expected to take roughly the same time as the entire job132.cmd run.  As
> > the job numbers go up, the proofs get larger and larger, and the expected
> > run times will increase, until job160.cmd which might take orders of
> > magnitude longer, who knows.  To help avoid frustration, you should start
> > with the lower job numbers first.
> >
> > The biggest proofs may be infeasible unless we break up the 'minimize' run
> > into small ranges of statements and/or break up the proof into smaller
> > lemmas.  We'll have to see how it goes with experience.
> >
> > 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/3ONE57KGXFOW3.33VH46N97A16O%40wilsonb.com.



-- 
Kie ekzistas vivo, ekzistas espero.

-- 
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/CAMZ%3Dzj6s04D-xbOtukZOcMoR6ndGKiwL6zAYxyr%3DBNAiRwCWvQ%40mail.gmail.com.

Reply via email to