Hi Jon On Wednesday, March 4, 2020 at 11:46:58 AM UTC+1, Jon P wrote: > > Thanks both for the help, that is very kind. > > One problem I came across while tracking down which theorems used the ones > in 18.1.7 is I came across several in mathboxes. For example ghomf1o > <http://us.metamath.org/mpeuni/ghomf1o.html> relies on ghomid which is in > 18.1.7. > Yes, I observed this already and asked how to handle these cases in a Github issue on 24-Jan-2020: https://github.com/metamath/set.mm/issues/1432#issuecomment-578288636
> My general question is how should theorems in mathboxes be handled if we > are discussing removing 18.1.7? Do we need to replicate all theorems using > the extensible structures in including all the ones in math boxes? > No, nobody else should spent a lot of work for theorems in others' mathboxes (to shorten proofs or to replace names are exceptions, of course). > What if they are odd theorems that other people aren't so interested in? > Only the mathbox owner can/should judge if one of his/her theorems is odd. Can we contact people and ask them to transfer them themselves? > Usually Norm does this, at least if no contact data is available. Is it ok to delete things from mathboxes without replacing them (I imagine > this might be a problem for some people)? I feel this is a bit above my > paygrade. > Deletions should be done by the owner or by Norm (or on Norm's behalf). > I think I might narrow my efforts down a bit just to doing theorem pairing > (finding the new theorem which is the equivalent to the old). This is a > task that needs to be done for all of parts 18, 19 and 20 and is > non-controversial. I noticed some theorems, for example smgrpismgmOLD > <http://www.google.com/url?q=http%3A%2F%2Fus.metamath.org%2Fmpeuni%2Fghomf1o.html&sa=D&sntz=1&usg=AFQjCNEraRkWXdBMqu9TuY2ucRhYJvnMkA>, > > have in their description a link to their new theorem. Is it ok if I start > submitting pull requests which add links to theorems for which I have found > pairs? Is it ok to add OLD to the name, presumably that is not allowed if > there are any theorems that depend on it as it would break verification? > Yes, this is a good idea, and I practiced it already (smgrpismgmOLD <http://www.google.com/url?q=http%3A%2F%2Fus.metamath.org%2Fmpeuni%2Fghomf1o.html&sa=D&sntz=1&usg=AFQjCNEraRkWXdBMqu9TuY2ucRhYJvnMkA> ). By this, the theorems are clearly marked as not to be used anymore, neither in new proofs nor in existing ones (i.e. have to be replaced sometime). By providing a date ("Obsolete version of ~ sgrpmgm as of 3-Feb-2020") everybody has enough time (usually about one year) to clean up his/her mathboxes until the lifetime of the OLD theorem expires and the OLD theorem (together with all theorems using it) is deleted. > > In that vein could I ask for some help with the following pairs? I think I > have found the right thing but I am not sure. > > Is ghsubablo > <http://www.google.com/url?q=http%3A%2F%2Fus.metamath.org%2Fmpeuni%2Fghsubablo.html&sa=D&sntz=1&usg=AFQjCNF3htYnkhPU6j1sM2q0yjrZDgPOIA> > covered > by ghmabl <http://us.metamath.org/mpeuni/ghmabl.html> or is it to general? > I think it is covered and can be deleted resp. tagged with OLD. Is ghsubgo <http://us.metamath.org/mpeuni/ghsubgo.html> covered by ghmima > <http://us.metamath.org/mpeuni/ghmima.html>? > The same, it is covered and can be deleted resp. tagged with OLD. Is elghom > <http://www.google.com/url?q=http%3A%2F%2Fus.metamath.org%2Fmpeuni%2Felghom.html&sa=D&sntz=1&usg=AFQjCNGf8mcV2DtOBaufhovtbGgCgjC6CA>paired > > with isghm <http://us.metamath.org/mpeuni/isghm.html>? They use quite > different symbols. > The same, it is covered and can be deleted resp. tagged with OLD. The symbols may be different, but the contents are qualitatively identical. By the way, the corresponding lemmata (elghomlem1 etc.) should also be suffixed by OLD and marked as "obsolete". > > For the rest > <https://docs.google.com/spreadsheets/d/19Msa6Qib2oe1zA2QIDWKRjPQvq-08DlbuWVUADV4d04/edit?usp=sharing> > > I think I have all the pairs correct. > > > -- 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/a31cecf9-e929-44c3-8142-0b44481fa7e2%40googlegroups.com.
