(Branch of thread "George Hotz, a 5+ hours video complaining about Metamath, with 14000+ views and 163 thumb up", see post https://groups.google.com/d/msg/metamath/XPYuatviNV0/3LtVDyu-DQAJ):
David A. Wheeler: >> 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". ... Norman Megill: >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"? David A. Wheeler: 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. Related posts afterwards Mario Carneiro/David A. Wheeler(https://groups.google.com/d/msg/metamath/XPYuatviNV0/zI-ImZDEDQAJ): On January 4, 2020 10:17:44 AM EST, Mario Carneiro <[email protected]> wrote: >On Sat, Jan 4, 2020 at 10:08 AM David A. Wheeler ><[email protected]> >wrote: > >> But changing our label conventions so that underscores are between >the >> abbreviations might be a good idea. >> >> It'd be a pain to rename everything, but that is something that can >be >> done once and could be almost entirely automated. >> > >I doubt this. Determining where the breaks are would be a highly >nontrivial >task that I would not trust to a computer without oversight, and it will >hit almost all theorems, so this is not an easy task at all. Oh, oversight would be absolutely necessary. I think a first cut could be partly automated by noticing which symbols exist, finding their df-NAME, and splitting by NAME in that label. But it would clearly take some time. -- 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/ff049cf6-15b5-4a0f-a948-c7e3b8b1f3d1%40googlegroups.com.
