Custom attributes and initialize

Stream: lean4

[Mario Carneiro]

What's the status on defining new user attributes like @[to_additive] and @[ext]? A fair number of tactics are blocked on this or some other way of tagging lemmas.

Related: what does initialize do, and how should it be used? When is "initialization"? My impression is that you can use this to store arbitrary data in the environment, which is way better than the lean 3 approach of serializing everything into exprs and sticking them in attributes.

[Mac]

Mario Carneiro said:

A fair number of tactics are blocked on this or some other way of tagging lemmas.

Is it possible you could use type classes as an alternative? That is, have the relevant lemmas be instances of a given type class and use have that type class serve as the tag.

[Jannis Limperg]

Piggybacking on this topic: is there currently any way, regardless how hacky, to get a custom attribute and custom trace option in (short of forking Lean)? #eval registerTraceClass seems to work, but I guess the server expects it to be pure (and it scares me). I also have a tactic prototype that would really benefit from this.

[Mac]

Apparently, according to the devs, @Mario Carneiro is right -- custom user-space attributes are currently not supported. It is in the plans but will not be added right now.

[Jannis Limperg]

Yeah, I had heard the same thing. Just hoping there's a difference between "not supported" and "can't be done".

[Mac]

Well when I asked how to add them in a similar discussion the response was it may be time to implement non built-in attributes which got shot done as a complex thing to do later. This implied to me that there is no way to add non built-in attributes at this time.

[Mac]

The one hacky, non-fork way I could think of doing it is by building a shared library defining the new custom builtin attributes and passing that library to lean --plugin. That may work.

[Mario Carneiro]

Do you (or the devs) know what the specific technical challenges are? That might help suss out where the line between "not supported" and "can't be done" is

[Mac]

To quote @Sebastian Ullrich : "The core limitation that would have to be lifted is the one on registering environment extensions: https://github.com/leanprover/lean4/blob/master/src/Lean/Environment.lean#L227-L230"

[Mac]

Also, see this issue, which goes into more detail: https://github.com/leanprover/lean4/issues/513

[Gabriel Ebner]

Jannis Limperg said:

Piggybacking on this topic: is there currently any way, regardless how hacky, to get a custom attribute and custom trace option in (short of forking Lean)? #eval registerTraceClass seems to work, but I guess the server expects it to be pure (and it scares me). I also have a tactic prototype that would really benefit from this.

I don't think there's a requirement to register the trace class (in fact there's quite a few trace messages in core for unregistered trace classes). The only downside of not registering is that you can't use set_option to enable it. You need to use sudo set_option instead:

import Mathlib.Tactic.SudoSetOption
open Lean

sudo set_option trace.jannis true in
#eval show MetaM Unit from trace[jannis] "Erfolg!"

[Jannis Limperg]

Very nice, thanks! That's more than good enough for prototyping.