I agree with Alexander's comments, and if you want to create a PR for this
(renaming the to-be-deleted theorems as *OLD) it is fine.
It is preferable for the comment in *OLD to be e.g. "Obsolete version of ~
sgrpmgm as of 3-Mar-2020. " because when I look for expired theorems to
delete, I would search for "Mar-2020. " in April 2021 (or if we wait until
2022, just "2020. ") where a space (or newline) follows the period.
Although the space after the period isn't mandatory nor an official
convention, it can help speed up the cleanup process a little.
BTW a *OLD cleanup is a little overdue, and other people can do this as
well, if anyone wants to volunteer. All that is needed is simply to delete
any *OLD theorem after a year from the "Obsolete..." comment; no entry in
the list at the top of set.mm is needed. But I would prefer that each case
be inspected by hand before deletion to give it a final sanity check; an
automated tool to do these deletions might be dangerous, for example if the
date is suspicious, it might be a typo like typing 2019 instead of 2020.
Of course you should make sure that the *OLD isn't used ('verify proof *
/syntax_only' would catch that instantly). There are some *OLDs without an
"Obsolete..." comment, which will require a judgment call; maybe it would
be best to add an "Obsolete..." comment with today's date and otherwise
leave it alone. If the *OLD is in a mathbox, sometimes a little more care
should be taken, since the mathbox user could just be experimenting with
different versions of a theorem (but if it has an expired "Obsolete..."
comment it should pretty much always be safe to delete).
Norm
On Wednesday, March 4, 2020 at 9:32:55 AM UTC-5, Alexander van der Vekens
wrote:
>
> 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/3115f977-af71-4567-b5ec-c228f307b035%40googlegroups.com.
