The set.mm section "Recent label changes" has a list of such label and related changes, beginning line 97 and ending line 12445 (as of 2021-12-02). I think it is huge and grew much faster in recent years, because its purpose changed. It is now considered a "history" of set.mm, whereas, if I understood correctly, it was originally made to record only the changes that would break proofs building on theorems in Main.
Typically, if a statement in Main is relabeled or if a token is changed, it should be mentioned, but if a new statement or syntax is added, or moved from a mathbox, it need not appear since it would not break proofs building on theorems in Main. Additionally, there is now a reliable history tracking with git, so I think there is no need to clutter set.mm beyond what is strictly necessary to update proofs. So I think the purpose of that "Recent label changes" section should be made more precise. As for me, I think the second option is preferable, but I'll go with any decision. Benoît -- 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/cf9c6097-7f50-4344-86f3-318176be7ea6n%40googlegroups.com.
