If someone wants to maintain this, that's fine with me, although adding another file to remember to update doesn't seem ideal.
Another possibility that doesn't require a separate file is to state at the end of a truncated list something like "Older entries can be found in set.mm version of <date>, <GitHub download URL>". You can build the full list by following the links until there is no "Older entries..." line. (The date provides a backup in case the GitHub link stops working. If there is concern about availability of very old versions, the full list could be refreshed every now and then in a special commit.) Off and on in the past, I've thought about truncating the label change list since we can always go back to historical versions. One reason I didn't do it was that the list represented a relatively small part of set.mm and it didn't seem like an urgent matter. The current stats are: Size of label change list: 598kB, or 1.4% of set.mm size Lines in label change list: 12350, or 1.7% of set.mm line count Number of lines with "moved": 3459, or 28% of label change list lines Still, I agree some kind of truncation would be less clutter in the set.mm header section. Norm On Monday, December 6, 2021 at 5:58:01 PM UTC-5 David A. Wheeler wrote: > > > > On Dec 6, 2021, at 4:44 PM, 'Alexander van der Vekens' via Metamath > wrote: > > > > Maybe we can find a compromise between David's (and my) proposal to have > a separate file and Norm's proposal to keep only the recent changes in set. > mm: Every time (year) the old entries are removed from set.mm, these > entries are added to the history file. By this, we avoid (regularily) > maintaining a separate file, which seems to be impractical, keep set.mm > short and retain the whole history. > > I'd be delighted to see that. Maybe call it "older_changes" or something > like that. > > --- David A. Wheeler > > -- 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/1a5064a9-3264-42c7-bd1b-f90dc0e86725n%40googlegroups.com.