On Saturday, May 23, 2020 at 11:52:50 PM UTC+2, Norman Megill wrote: > > ... > As was already mentioned, there is no section called "Commons". There is a > section called "(Future - to be reviewed and classified)" that possibly > could be renamed as discussed here: > https://groups.google.com/d/msg/metamath/UwTUuNPgaB0/NdWefzG4AgAJ > The purpose of this section is to provide a place for theorems needed by 2 > or more mathboxes that otherwise don't currently have a place elsewhere in > set.mm. While I'm not rejecting your proposal out of hand, your work > would not immediately be needed by 2 mathboxes, and to me it doesn't really > fit in with the purpose of this section. I would prefer that you use a > mathbox like everyone else. >
I was not aware of section "(Future - to be reviewed and classified)" until now (sorry, Norm, that I did not noticed it in your post on April 25, 2020). In this post, it is written: 3. Note that we already have a section called "(Future - to be reviewed and > classified)" http://us.metamath.org/mpeuni/mmtheorems.html#dtl:17.3 that > was added primarily for the purpose of the "Commons" you mention. If people > think that renaming it to "Commons" would be more intuitive, that's fine > with me. Maybe "(Commons - to be reviewed and classified eventually)". > I would propose to move this section into part *PART 21 SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)* <http://us2.metamath.org/mpeuni/mmtheorems275.html#mm27487h>, maybe as section "21.2 Mathbox for Commons". In the section header, it could be described in more detail what this section contains and how it should be used: definitions/theorems to be reviewed and classified eventually, not yet mature enough to be contained in the main body of set.mm, processed by more than one person, used in a personal mathbox, etc. - and which rules should be obeyed (additional content should be available in a personal mathbox for some time before, review during a PR recommended, contents should not be deleted or significantly modified without asking the contributor, etc.). The main reason to treat this section as mathbox is that the definitions/theorems of this section should be treated as if they were contained in a mathbox (e.g. should not be used by minimize by default). According to the existing rule, the definitions/theorems of this section should be moved to the main body if they are used in at least 2 personal mathboxes. As I have written already before, the definitions/theorems of this section could be regarded as "release candidates" for the main body of set.mm. > > Nonetheless, if we are to place your work directly in the main part of > set.mm, it needs to be of high quality and vetted. It would be good if > you post here the new definitions you propose and provide a description or > outline of what theorems you intend to prove. Could you do that? Thanks. > I agree with Norm that the general rule should still be to provide new proposals in a (personal) mathbox first (to demonstrate a certain amount of maturity). Exceptions could be granted if such a demonstration is provided on another way, e.g. by a post in the Google group as Norm proposed, or as "issue" in GitHub. Alexander -- 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/3504c5fa-9081-4c32-9552-da8d79b0905d%40googlegroups.com.
