There might be an error in the minimize command; it found that axdc has a much shorter proof using ax-dc, which is obviously true yet defeats the purpose of the axdc theorem ( http://us.metamath.org/mpegif/axdc.html ) and uses new axioms for that theorem.
On Wed, Feb 12, 2020 at 12:05 AM David Starner <[email protected]> wrote: > > 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 > <[email protected]> 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 <[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. > > > > -- > Kie ekzistas vivo, ekzistas espero. -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAMZ%3Dzj68pwtXKgJnVvu36gYqULARBza%2B%2BGe0pLZQxRSVP4Tv%3DA%40mail.gmail.com.
