I agree that we don't need to keep a complete history of all theorems moved from mathboxes. Sometimes I have found it useful to know the recent ones to be aware of changes made to the main part. Perhaps we could have a policy of deleting the ones over say 1 year old like we do for *OLD theorems?
Norm On Sunday, December 5, 2021 at 6:37:44 AM UTC-5 Benoit wrote: > 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/92ed7ee7-6603-44e8-b5e0-645d5af4b6d3n%40googlegroups.com.
