How to add user attributes?

Stream: lean4

[François G. Dorais]

I've been enjoying Lean 4 a great deal and I'm really impressed by the powerful macro system which has so far helped me delay learning more about the deeper parts of Lean 4 metaprogramming. However, there are some things that are beyond the macro system. I know the docs aren't ready yet and I'm generally happy to wait... but Lean 4 is so exciting!

Perhaps this is not a wise place to get started learning about using the Lean 4 monads, but I thought I'd ask since I couldn't find any examples in the tests or elsewhere and there's a similar thing I want to do to port some old Lean 3 code. Let's say I want to add a simple tag attribute called tellMeYourName such that

@[tellMeYourName] def blah := 0

prints out "My name is blah" (or some other inconsequential but observable action). How would I go about doing that in Lean 4?

[Leonardo de Moura]

Users will be able to define their own attributes. However, the attribute API is still changing. We will document and add examples as soon as it is stable.

[Mario Carneiro]

Now that env extensions have landed, my understanding is that user attributes are now possible, but I could really use a usage example. This isn't working for me:
Test/A.lean:

import Lean
open Lean

syntax (name := foo) "foo " ident : attr

initialize fooRef : IO.Ref (Array (Name × Name)) ← IO.mkRef #[]

def fooAttr : AttributeImpl where
  name := `foo
  descr := "foo"
  add
  | declName, stx, attrKind => do
    fooRef.modify fun foos => foos.push (declName, stx.isNameLit?.get!)

#eval show CoreM Unit from do
  match registerAttributeOfDecl (← getEnv) (← getOptions) ``fooAttr with
  | Except.ok env => setEnv env
  | Except.error e => throwError e

Test.lean:

import Test.A -- unknown declaration 'fooAttr'
@[foo bar] def baz := 1

[Daniel Selsam]

I haven't double-checked that this works, but FYI @Jannis Limperg implemented this here: https://github.com/JLimperg/aesop/blob/master/Aesop/Config.lean#L370-L396

[Leonardo de Moura]

You have to use the initialize command. We have examples here
https://github.com/leanprover/lean4/tree/master/tests/leanpkg/user_attr
It is part of our test suite, and it is being tested on all platforms by the CI.
Other relevant examples for user extensions
https://github.com/leanprover/lean4/tree/master/tests/leanpkg/user_ext
https://github.com/leanprover/lean4/tree/master/tests/leanpkg/user_opt