Norman Megill: >The primary purpose of a label is to identify a theorem uniquely.
>Note that at the top of set.mm I added a link to label conventions. As someone who helped write the section on label conventions, I appreciate that. :-) >For me personally, an important reason to keep labels short is to make them >easier to type. Maybe this isn't everyone's experience, ... > since they are never >going to be spelled out in full English, what abbreviations were chosen. >There seems to be a threshold label length of maybe around 8 to 10 >characters where I start to make mistakes typing it in... >The Wikiproofs site (wikiproofs.org) seems to be down, but looking it >up on >archive.org it uses theorem labels like >"introduceBiconditionalFromImplicationsInConsequent". Personally I >think >that would slow me down and I would dislike it. IIRC Jim Kingdon >contributed to that project, and it would be interesting to hear his >experience with long labels. I would also like to hear their experiences. I suspect full names like that would be suboptimal for set.mm, but I'm willing to be convinced otherwise. One problem with long names like that is that in the two-column format there would be much less room on a phone for the expression. >Another smaller consideration is the set.mm file size. Inside of >proofs in >the current set.mm, there are 1.1 million instances of labels with an >average length of 5.8 bytes. Each extra byte of average label length would >add a megabyte to the file size. >> If we want names to be much easier to read for newcomers, though, I >think >> the obvious way would be to insert separators between the named parts. >> The obvious separator is "_", so we could rename "sqr2irr" into >> "sqrt_2_irr". ... >I don't see the point of "squareroot_2_irrational" - long to type, >annoying >to shift for the _, and not necessarily easy to remember precisely (is >it >"2" or "of_2"? Yes, I think squareroot_2_irrational is probably too long ( though as I noted above, I'd be interested to hear other opinions). But changing our label conventions so that underscores are between the abbreviations might be a good idea. That would produce labels of the form sqr_2_irr. That might make it a lot easier for people. Currently you have to know the entire set of abbreviations to read what the parts are. If you don't recognize the first abbreviation, it's harder to understand the rest. If we added underscore separators, it'd be much easier for newcomers to understand the label convention and be able to understand at least some of the parts. As the database gets bigger, it becomes harder and harder to remember all the abbreviations, so having a separator is starting to become more and more justifiable. We could make a few exceptions if you think that's important, e.g., for 2p2e4. It also wouldn't add that much more space. I'm guessing there is an average of 4 abbreviations in a label, so we'd add an average of 3 underscores to each label. That means the average label would change from 5.8 to 8.8. That is very doable. It is not a killer in disk space, and it is also within your goal length for labels. Even if the average is 6 abbreviations, which I doubt, that would make the average label length 10.8 which isn't really all that bad, especially since the underscores are really just separators and thus easy to remember. One nice side effect of using underscores as separators in labels is that we can instruct css break on underscores, which could improve the formatting in some cases. It'd be a pain to rename everything, but that is something that can be done once and could be almost entirely automated. --- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/5AF5A9F0-FF79-4FBA-8EDF-93C1E20DEDEE%40dwheeler.com.
