On Saturday, December 28, 2019 at 1:47:43 AM UTC+1, Norman Megill wrote: > > On Friday, December 27, 2019 at 5:23:37 PM UTC-5, Benoit wrote: >> >> Hi all, >> >> I found it convenient to label most of the theorems in my mathbox as >> bj-xxx (my initials). This allows me to do things like "MM> verify proof >> bj-*" and other things like bulk minimizations and potentially more >> things. I find it convenient to have a "namespace" to do these kinds of >> things. I can also notice more easily when one of these theorems is used >> in a proof. Obviously, when/if they go to the main part, the prefix should >> be removed. Actually, if other mathboxes had this convention, it would be >> easier for us to spot when we're using a theorem from another mathbox and >> then to move it to the main part, or at least to duplicate it. >> > >> David recently remarked ( >> https://groups.google.com/d/msg/metamath/OyBTnESDvnM/rFCBvqJcCwAJ) that >> this convention may make it harder to move theorems to the main part: one >> would need to relabel them, maybe with some complications coming from label >> clashes. I do not think this outweighs the above benefits, but I may be >> missing some other implications. What do you think ? >> > > I agree with you, I don't think the prefix bj- is a problem. While I > don't think we should enforce the use of such a prefix, if a mathbox > contributor wants to use it, that's fine with me. It immediately > identifies the contributor and the fact it's in a mathbox. When moving > theorems into the main set.mm, their labels should be vetted anyway. > Many mathbox labels don't conform to our conventions, especially with > theorems by new users, and a significant percentage will typically need to > be changed anyway. Renaming to remove the bj- will force at least a > cursory inspection of the label. > > We already require a list of theorems and any renames at the top of set.mm > to document the moves to the main set.mm, and that same list can be > easily reformatted to be the input for a global renaming script. > > I agrgee with Norm: the labels for theorems in mathboxes can be prefixed (or marked in another way), maybe this approach can even be recommended according to the advantages mentioned by Benoît, but it should not be mandatory.
An exception is when a theorem has a permanent external reference such as > in the mm100 list, which prompted this discussion, and in that case it is > better to use a more permanent name even before the theorem is moved out of > its mathbox. But that is relatively rare. > A long time ago I suggested to move all theorems of the mm100 list which are still in mathboxes to the main part, David posted a corresponding suggestion recently. Therefore, this should be only a temporary problem > > >> >> Also, I would like to find a way to foster collaborations between >> mathboxes. For the moment, MM does not look at other mathboxes when doing >> MM> IMPROVE, MINIMIZE, or similar things (although there is an option >> /include mathboxes). I do not know about mmj2, but it uses at most >> mathboxes which are before ours. Could there be a method, a script or >> anything that, when a contributor starts proving stuff, it automatically >> positions his mathbox last, and signals when theorems from other mathboxes >> are used (and at the end of the session, restores the original order of the >> mathboxes) ? This might be doable with the /SPLIT option introduced >> recently by Norm. >> > > I don't agree that 'minimize' should scan other mathboxes by default. It > used to be the default, but other mathboxes were causing a problem, such as > accidentally matching a weird variant of a standard theorem that might save > 1 step but would never be used otherwise and would never be imported. I > got tired of manually removing such matches, so I turned them off by > default for routine use. I provided /include_mathboxes so other mathboxes > could be scanned in exceptional cases. But its use should be intentional, > with the results carefully scrutinized. > > Mathboxes are specifically for experimental and rough work that should not > be used by default. If a theorem is useful then it can be imported, but > blindly using whatever matches in other mathboxes isn't a good idea IMO. > On the one hand, I agree with Norm in principle. On the other hand, however, I share Benoît's concern that many useful theorems are burried in mathboxes and are difficult to find. In a former post (unfortunately, I cannot find it anymore...), I proposed to provide a "third stage" between the main part and the mathboxes where "release candidates" (theorems which are ready/worth to be moved to the main part from the contributor's point of view) are collected. These can be included in minimizations (I think no program changes are required for this, because these theorems won't be in mathboxes). The mathboxes can be continued to be used for first steps/experiments, as mention by Norm. > > If a theorem merits a move to the main set.mm, it will be used for > minimization anyway at some point in the future after it is moved. There > is certainly no urgency to use it while it is sitting unvetted inside of a > mathbox. It can wait. Most people don't even seem to care much about > minimizing their mathboxes but wait a year or two for our occasional global > minimize runs. > > 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/e25ef75f-fb9b-49db-a3cb-817175a10e0f%40googlegroups.com.
