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/d05bff4f-e204-45bd-be95-b323f19a90ce%40googlegroups.com.
