User attributes

[leodemoura]

We should allow users to declare their own attributes. This feature is supported in Lean 3 and is used in a few mathlib metaprograms.

[Kha]

Just to explain the current state: attributes can be registered only in builtin_initialize, i.e. initializers compiled into native code. However, this is not a good idea to do in plugins (i.e. anywhere outside the stdlib) because environment extensions (what attributes boil down to) are identified by an index assumed to be globally unique. Thus .olean files will not be compatible between packages using different sequences of attribute-declaring plugins, and in particular you will not be able to depend on two independent packages declaring (and using) attributes. If I'm not mistaken.

[tydeu]

Looking through the environment code, I noticed that the globally unique index @Kha mentioned is an incrementing Nat that is simply the extension's index in the array of extensions. Could one way of solving at least the order problem @Kha presented be to use a Name instead to index the extensions? This would at least allow users to safely use plugins to register new attributes (until proper non-builtin attributes arrive).