On Sat, 15 Jun 2019 07:05:43 -0400, Mario Carneiro <[email protected]> wrote: > I would like to get away from label conventions in favor of something > machine readable and not hardcoded.
I'm fine with adding additional mechanisms. However, I'd like to keep using & enforcing the label conventions. I find they're very helpful for the humans who are trying to read this stuff :-). And once the humans start depending on the conventions, it's wise to enforce the conventions so the fragile humans aren't misled. Label conventions are also "machine readable". You can make them not hardcoded by adding a mechanism to declare the label convention. > The mechanism I propose is: > > If an $a statement is given for a syntax typecode (i.e. not |-), then it > is a definition iff the immediately following statement is a definitional > axiom $a |- foo = ... which satisfies the usual rules. Otherwise, it is > treated as an axiom, and a warning is issued if the label convention > implies that the axiom would like to be treated as a definition and there > is no warning-suppressing pragma attached to the axiom. That's extremely strict. Even though we don't use it in set.mm today, I worry about being unable to escape it later. I'd prefer that to be the *normal* case, but with a special statement (say a $j) that means "it's a definition even though it's down here" statement. > We can add $j commands to define the df-* convention for issuing warnings, > and suppressing warnings on the definitions that aren't actually > definitions but are called df-* anyway. I would call the df-* definitions definitions, but otherwise sounds good. > Some label changes I see (skimming through mmdefinitions.html) are: > > wb --> wbi (and similarly for wo wa, w3o, w3a, wxo), even though df-bi > > is a special case > > df-v --> df-vv (to match cvv and avoid collision with cv) > > > > The general rule has been to make constant names as short as possible while > still disambiguated, because they are not visible to the user. (I'm > starting to regret this choice in the recently completed lean translation > because these names are literally all that I see.) In particular, making > wceq and wcel longer will have a significant effect on total size of set.mm > because they are by far the most common theorems applied. (Maybe we should > use a Huffman encoding to choose label lengths?) I think conventions are good, even if it would increase the size of set.mm. So I would support switching to "wDFNAME" everywhere. We've already been moving to increasingly keep our label names consistent with the "df-NAME" definitions. And while the constant names aren't usually visible to the user, in your lean translation they *ARE* directly visible, and they're also visible in the HTML showing definitions. Also - the larger size only applies to the *expanded* size. When stored/transmitted using git or .tar.gz or .zip, I believe these will be trivially compressed to essentially the same size. This kind of sequence repetition is exactly what compression algorithms are good at handling. --- 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/E1hc9sr-0005Pa-Q1%40rmmprod07.runbox.
