On Monday, December 23, 2019 at 3:58:12 AM UTC-5, Alexander van der Vekens wrote: > > On Sunday, December 22, 2019 at 4:34:17 PM UTC+1, Mario Carneiro wrote: >> >> ... set.mm would have been an optimal starting point, except it's HUGE, >> which makes introductory stuff harder. Even worse, it starts with a comment >> that is tens of thousands of lines long, which makes it very difficult to >> see how "baby's first propositional logic" is supposed to go. >> >
> > Maybe a first step to purify set.mm could be to extract the "history" in > section "1. Recent label changes" at the beginning of set.mm into a > separate file - this would save (currently) about 10.000 lines ... > Possibly, although that might be a good way to ensure it rarely gets updated. :) We've had a pretty good record of keeping it maintained, and I think that's partly because it's at the top where everyone sees it. The label change list already is a separate file called set-header.mm if you use 'write source set.mm /split'. Currently predicate calculus is broken out into a stand-alone mm file called set-pred.mm, but we could further split that into set-prop.mm and set-pred.mm, or however we want. Maybe we could add a comment on the 2nd line of set.mm, "To break this file into smaller modules, in the metamath program type 'read set.mm' followed by 'write source set.mm /split'.", which newcomers would see when first opening set.mm. While we could release set.mm in the form of multiple modules (currently 38) created by /split, that would mean extra work to keep David's autotools updated and possibly cause other confusion as people add, delete, rename, or merge modules in their mathboxes etc. I would prefer not to do that since it doesn't really buy us anything. Another alternative would be to keep only the past year or so and discard older history. Or we could abandon it completely and rely on git, although it might be hard to infer label change history because things are often simultaneously moved and renamed. Historically, I added the label change list around the time other people started to make significant set.mm contributions. People would sometimes work on their part for months then send me their update or mathbox. I used the list to make a script to update the labels in their work so it could be integrated into the current set.mm. Together with the top date to identify what set.mm version they modified, the label change list made it much easier to get their work updated. Now almost everyone (but not all) uses GitHub to submit their work. A couple of months ago, when I located some old material that allowed me to fill in missing dates before 5-Aug-1993, the list enabled me to track the history of many label changes. Of course that was a one-off change that will likely not be repeated. Norm -- 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/114b8174-2bd8-48dd-8056-608cb1b6eaff%40googlegroups.com.
