The set.mm section "Recent label changes"

[Benoit]

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

[Norman Megill]

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

[David A. Wheeler]

> On Dec 5, 2021, at 5:48 PM, Norman Megill <n...@alum.mit.edu> wrote:
>
> 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?

I would prefer simply moving this history into its own file & keep it in the repo.
Having a canonical source of info can be useful, but we don't need to re-read it in every verification run,
and it creates a HUGE number of lines that are useless for many.

--- David A. Wheeler

[Mario Carneiro]

I'm not sure the list pulls its weight. If we had a tool that could read it (and check it for machine readability errors) then I might feel differently, but as it is now it's just a huge maintenance overhead for very little gain.

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/B212880D-D3E4-4515-AD28-1BED26048B27%40dwheeler.com.

[Alexander van der Vekens]

On Mon, Dec 6, 2021 at 3:00 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:

I would prefer simply moving this history into its own file & keep it in the repo.
Having a canonical source of info can be useful, but we don't need to re-read it in every verification run,
and it creates a HUGE number of lines that are useless for many.

I made this proposal already in 2019, see https://groups.google.com/g/metamath/c/XPYuatviNV0/m/brh1f_76CQAJ, and Norm argued against it in https://groups.google.com/g/metamath/c/XPYuatviNV0/m/1Terj6AYCgAJ.

[Alexander van der Vekens]

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.

[David A. Wheeler]

> On Dec 6, 2021, at 4:44 PM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> 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

[Norman Megill]

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: