Attribute casing convention

Stream: lean4

[Mario Carneiro]

The discussion at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/tactic.20naming.20convention ended with a decision to use snake case for tactics, along with commands (which were already snake case). The suggested heuristic is that anything that acts like a keyword should be camel cased.

But what about attributes? The keyword litmus test is inconclusive, because attributes can either use the catchall parser

@[builtinAttrParser] def simple := leading_parser ident >> optional (priorityParser <|> ident)

which will parse arbitrary identifiers (not keywords), or they can be provided as keywords by adding productions to the attr grammar:

syntax (name := mkIff) "mk_iff" (ppSpace ident)? : attr

This latter method is required for any attribute that takes arguments. I don't like the idea of having different casing conventions for these two, because the user ideally should not have to care about the implementation detail of whether @[foo] is parsed using Attr.simple or Attr.foo.

Currently, attributes in lean 4 core are camel cased (like builtinInit, macroInline, implementedBy), while the attributes in Mathport.Syntax were switched to use snake case along with tactics following mathlib4#141. I have no strong feelings about which way to go here, but it would be good to have a decision about this on record.

@Gabriel Ebner @Sebastian Ullrich @Leonardo de Moura @Mac

[Mario Carneiro]

Another observation that might be relevant: Attribute names are in a flat namespace, in the sense that the name you pass to registerBuiltinAttribute has to be atomic, and it is derived from the last name component of the corresponding syntax. So for example the syntax for mk_iff above is registered under the name "mkIff" even though the user writes @[mk_iff] (even if that syntax declaration is in a namespace, in this case Lean.Parser.Attr.mkIff), and it would clash with any simple attribute like @[mkIff]. If you try to add @[mk_iff] to a declaration without a registered handler, you get the somewhat surprising error that there is no attribute declared for [mkIff], while if you do the same for an undeclared identifier @[foo_bar] the error says there is no attribute declared for [foo_bar].

This suggests that we should try to keep the initial token the same as the name of the syntax, rather than using different naming conventions as in the example.

[Mac]

@Mario Carneiro one other thing to note is that if you use the same casing style for attribute names as for keywords, you can end up with a lot of naming clashes for attributes using the attr.simple parser (i.e., an ident name). For example, if the mk_iff attribute is a simple attribute and has a helper mk_iff syntax to define it then the attribute will now need french quotes when used manually (this is a problem I already experience in Lake with the package and script attributes and syntaxes).

[Mac]

One way to get around this would be if attr.simple used some kind of rawIdent parser (that capture any ident, regardless of keyword status) and the attr category used a leading behavior of symbol (or mixed). I believe that would prevent such clashes from occurring and would not creating parsing ambiguities.

[Mario Carneiro]

If feel like attributes should not keywordify their first token, similar to tactics. They are context-sensitive keywords so this shouldn't cause any problems

[Mac]

@Mario Carneiro The problem is the other way around. The command / term level syntax keywordifies the token which then prevents it from being used as an identifier for attr.simple (without french quotes).

[Mario Carneiro]

I see. Why not use a keyword attr parser in that case?

[Gabriel Ebner]

Because the term keyword might have been declared afterwards or somewhere else.

[Mario Carneiro]

keywordification is a global thing, so you should try to avoid "after the fact" stuff. This is why the precedence command exists in lean 3, to make sure that things don't become keywords post hoc causing order dependent import and other messy things

[Gabriel Ebner]

As far as I'm concerned, we could remove the simple parser and always require syntax definition + elaborator attribute registration, like we do with everything else. But I feel like we're straying off-topic.

[Sebastian Ullrich]

IIRC the simple parser was mostly for bootstrapping

[Sebastian Ullrich]

If we agree that at least morally each attribute comes with its own syntax, then I agree that they should follow the same casing convention as tactics