It looks like my proposal wouldn't be welcomed, so I will abandon it. As for keeping a list of minimized theorems, I'm not really in favor of that either; it would be one more thing to maintain that people will forget or neglect.
As for mathboxes, we've never had a rule about people minimizing proofs in other people's mathboxes, or even finding shorter proofs manually, adding credit and creating a *OLD for the original (and still keeping everything in the mathbox). In the past we've done this often, and I always welcomed it. Indeed, there are well over 100 "(Proof shortened by [someone else]...)" tags currently in mathboxes. And if we add, say, a new variation of syl* in main that shortens 50 proofs, we typically apply it to all of them including ones in mathboxes, without consulting the mathbox owners. What would be the reason someone would not want a proof in their mathbox minimized? I could see a few cases where the proof is still being worked on and minimization would create a merge conflict, but I think that is rare. Most people, once they have a proof (a minimum requirement for the PR checks to pass), go on to the next and only occasionally go back and revise the proof. If a mathbox user doesn't want a proof to be touched because it is still being modified, the tag "(Proof modification is discouraged.)" can be added temporarily until it is finished. In any case, I strongly encourage people to minimize all proofs they submit, whether in their mathbox or not. An informal rule to minimize proofs when importing to main is nice, but it can't be enforced and I doubt it will always be followed. On Saturday, December 12, 2020 at 3:42:36 AM UTC-5 Alexander van der Vekens wrote: > I am currently workin within my Mathbox, and I found a minimization of one > of my poofs (using minimize_with) using a theorem of Benoît's Mathbox > (@Benoît: it's bj-eleq2w - can I move it (together with bj-eleq1w?) to main > set.mm? Where is the right place for them?). > This shouldn't have happened. 'minimize_with' does not consider other mathboxes unless '/include_mathboxes' is specified. Is that what you used, or is this a bug I should investigate? As for moving theorems out of mathboxes, we have often done that when a theorem is needed for another mathbox. Typically we simply move the theorem to main at an appropriate place (I use 'show trace_back' to help identify where it should best go) and add an entry to the list at the top of set.mm, but we don't necessarily notify the mathbox owner. Sometimes a name change is needed e.g. the "bj-" prefix would be removed or a new name is chosen that better conforms to our informal conventions; this is also documented in the same list entry at the top of set.mm. BTW that fact that someone else's mathbox theorem shortens a proof isn't necessarily a good reason to move it to main. E.g. there are many trivial variants of existing propositional calculus theorems in some mathboxes that may, by coincidence, slightly shorten a proof elsewhere in set.mm, but that doesn't necessarily mean we should move it out of the mathbox if it doesn't "pay for itself" in terms of shortening many proofs. > This example shows that there is a flaw in the approaches we discussed so > far: what about minimization if a new theorem is added to main set.mm > which would allow for a minimization of following theorems which were > minimized before? The global run of "minimize_with" on the entire set.mm > would detect and process such cases, but neither the marking proposed by > Norm nor the list proposed by @savask nor my proposal would handle such > cases. > I don't think this happens enough to be concerned with much. The global minimization will handle it, and in individual cases it can be dealt with manually. When proposing moving a new basic logic theorem to set.mm, most people will determine what proofs can be minimized with it as justification, and then will perform those minimizations. Maybe the program/script of my proposal could be extended to check for > proofs which could be minimized by the new/modified theorems (and gives a > hint to the contributor which proofs to minimize before the pull request > can be accepted)? > This isn't practical because for a very large proof, 'minimize_with' may take days to run. Norm > > On Saturday, December 12, 2020 at 7:51:24 AM UTC+1 Alexander van der > Vekens wrote: > >> 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/de0e99fc-aff6-4037-97d3-18390d4d6408n%40googlegroups.com.
