Documentation on attributes

[CohenCyril]

Description of the problem

In https://coq.github.io/doc/master/refman/language/gallina-specification-language.html#attributes I cannot make sense of the English informal syntax description... could someone knowledgeable write a grammar and few more examples?

From the little I understood, it seems that arguments of attributes are also called attributes, am I right? If this is the case, can we find another name for that?

[gares]

Given that for once we did not reinvent the wheel we could just point to https://doc.rust-lang.org/reference/attributes.html in the reference manual

[CohenCyril]

Given that for once we did not reinvent the wheel we could just point to https://doc.rust-lang.org/reference/attributes.html in the reference manual

well, it is certainly greatly inspired, but I believe it is not strictly the same syntax (I did not see ! in the syntax of Coq attributes, while it is present in Rust) ... so a pointer and a grammar are both welcome.

[Zimmi48]

Indeed, the shame is... we didn't actually reuse the same syntax. Anyway, @jfehrle is currently making progress on documenting accurate grammars in the refman, so this should be solved (for 8.12).

[ppedrot]

@CohenCyril we don't have inner attributes in Coq, which is the purpose of the ! annotation.

[jfehrle]

Take a look at the fullGrammar file (may be a little out of date with respect to master):

decorated_vernac: [
| LIST0 quoted_attributes vernac
]

quoted_attributes: [
| "#[" attribute_list "]"
]

attribute_list: [
| LIST0 attribute SEP ","
]

attribute: [
| ident attribute_value
]

attribute_value: [
| "=" string
| "(" attribute_list ")"
|
]