I fully agree with Norm's demand that all theorems in set.mm (at least in the main body of set.mm!) should be minimized, but I am of the same opinion as @savask that tagging minimized/not minimized theorems as proposed by Norm is not practicable and would make set.mm more clumsy.
At least I would not be happy if I have to care for these tags in my Mathbox (or allowing others to perform minimizations in my Mathbox, although I always would welcome hints that there is a way to minimize a proof in my Mathbox). I think we should restrict our attention/efforts to main set.mm. For my part, I always minimize new/modified theorems (unless I do not forget it unintentionally!) before I push them to the Git repository. Hints as suggested by @savask would be a (small) step to achieve more quality (with respect to minimization) and should be provided if this is possible with little effort. Regarding a list to be maintained I am a little bit sceptical if this was practical. What about checking for not minimized proofs while checking a Pull Request? Of course a program/script has to be written for it. Such a programm/script could look for all new/modified theorems (in main set.mm, not being tagged with "(Proof modification is discouraged.)") and run "minimize_with" for them. If the result is always "No shorter proof was found", then the check is passed, otherwise the pull request should be rejected. By this, each contributor is responsible for providing minimized proofs only. Alexander On Saturday, December 12, 2020 at 7:04:09 AM UTC+1 savask wrote: > I agree that minimization markers "add no value", so in my opinion they > should be kept out of set.mm altogether. Maybe we can create a file > "minimized_theorems" (something like "discouraged") which will be a list > of, well, minimized theorems :-) Contributors won't have to set any tags or > modify that file, but if someone decides to minimize a theorem, they will > check that file and in case if the theorem wasn't processed earlier they > will minimize it and add the name to the file. That way we will avoid > additional bureaucratic burden of contributing to set.mm. > > The "minimize" command of metamath.exe can be made to skip minimization of > theorems mentioned in the "minimized_theorems" file, so minimization > volunteers will be able to minimize whole ranges of theorems in bulk, > without doing double work. > > And speaking of making users minimize their theorems, I think most people > need only a small reminder. Right now, after you complete a proof in > metamath.exe, the program will remind you to do "SAVE NEW_PROOF" and > "VERIFY PROOF". Perhaps a suggestion to minimize the proof can be added > there as well? Same goes for mmj2, after a proof is finished and mmj2 > compiles it to the compressed proof format, one can add an automatic > comment suggesting the user to run "minimize" in metamath.exe. > -- 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/b3bf5060-e1f3-422c-b625-bae2c636d8e2n%40googlegroups.com.
