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. 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. > > 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. 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/d4bd14f3-d54d-462b-b89b-62805554abbd%40googlegroups.com.
