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.