Labels in mathboxes and fostering collaborations

[Benoit]

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 ?

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.

Benoît

[ookami]

My earliest additions to my mathbox date back to 09-2013. If I remember right, I was the first using a personal prefix in his mathbox.  The motivation then was to avoid name clashes. This turned out later to be quite useful, if not necessary, because I keep duplicates like wl-imim2 based on a different set of axioms than the main part.

In the past 6 years nobody objected to this practice, and when occasionally theorems found their way to the main part, removing the prefix was never an issue.

I don't see why people should not have the freedom to use their own naming scheme for whatever reason in their mathbox. This provides even a chance to suggest an improvement over the main part.

So unless a general renaming to something convincing is in progress, I am not inclined to 'fix' my personal mathbox.

Wolf

[Norman Megill]

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

[Alexander van der Vekens]

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 agree 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.