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.
On Monday, December 6, 2021 at 10:34:49 PM UTC+1 Alexander van der Vekens wrote: > On Mon, Dec 6, 2021 at 3:00 PM David A. Wheeler <[email protected]> >> 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. > -- 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/00c0c68c-a903-4933-ad8e-d30503352338n%40googlegroups.com.
