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 <[email protected]> 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3ONE57KGXFOW3.33VH46N97A16O%40wilsonb.com.
