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.
