attributes attached to a declaration

Stream: lean4

[Kevin Buzzard]

How can I see the attributes attached to a declaration? In Lean 3 I could see them with #print.

[Kevin Buzzard]

I hadn't realised that this would be so complicated. What's happening in practice is that I'm trying to understand the behaviour of to_additive and tags, and the only tags I'm interested in inspecting on a declaration are simp, norm_cast and coe. I'm having to construct examples to check whether tags are there because I can't just look to see what's going on.

[Tomas Skrivan]

I know how to go the other way around in a particular case.

Here is a command checking if an instance declaration is marked as default_instance

import Lean
import Lean.Meta

open Lean Elab Command Term Meta

syntax (name := mycommand1) "#is_default_instance" ident : command

@[command_elab mycommand1]
def isDefaultInstanceCommand : CommandElab
| `(#is_default_instance $declId:ident) => do
  let env ← getEnv
  let decl := declId.getId

  -- We can get list of all default instances with:
  let di := (defaultInstanceExtension.getState env).defaultInstances

  -- to check if `decl` is a default instance we simply do:
  let is_default_instance := di.any λ className listOfInstancesAndPrio =>
    listOfInstancesAndPrio.any λ (instName, prio) => instName = decl

  IO.println s!"Declaration {decl} is default instance: {is_default_instance}"

| _ => throwUnsupportedSyntax

#is_default_instance instHAdd  -- true
#is_default_instance HAdd      -- false
#is_default_instance instAddFloat -- false

However the approach is quite specialized for default_instance attribute, for another attribute it would look a bit different. It is not even clear that the corresponding PersistentEnvExtension has to hold the necessary information.

The chapter on attributes in the meta programming book seems to be empty :( It would be great to have an explanation of TagAttribute, ParametricAttribute, EnumAttributes and what are environment extensions and how are attributes connected.

[Jannis Limperg]

I think this functionality (list all attributes for a given constant) is still missing. In Lean 3, the attribute architecture makes this easy to do; in Lean 4, it needs specific support which has not been written yet.

If you're interested in a closed collection of attributes, you can write, for each of them, a function which checks whether the attribute was applied to the constant. The details vary depending on how the attribute stores its data, but it'll be broadly similar to Tomas' example. I would expect such functions to already exist for certain attributes.

[Jannis Limperg]

Tomas Skrivan said:

The chapter on attributes in the meta programming book seems to be empty :( It would be great to have an explanation of TagAttribute, ParametricAttribute, EnumAttributes and what are environment extensions and how are attributes connected.

I'll put this on the todo list, but I'm quite busy right now. Maybe over Christmas.

[Jannis Limperg]

Oh, I see there was already a long discussion about this in #mathlib4 > to_additive and coe

[Floris van Doorn]

I believe that even if you have a specific attribute, it is hard to check whether it is attached to a declaration. Some attributes don't record to which declarations they are attached. For example, this information is hard to get for @[ext], unless you want to navigate the whole DiscTree.

[Jannis Limperg]

I have a std4 PR for folding DiscrTrees but yeah, O(n) membership query is not great. SimpTheorems uses a DiscrTree plus one or two HashMaps to support erasing and efficient membership queries and I use the same approach for Aesop. Maybe it would be worth packaging this up into a data structure.

[Mario Carneiro]

I think a better approach for membership queries is to use the tag attribute's data structure, since that adds no startup cost

[Jannis Limperg]

Oh interesting, I didn't know about this optimisation.

[Tudor achim]

Consider the following parametric attribute definition (adapted from https://github.com/leanprover/lean4/blob/master/tests/pkg/user_attr/UserAttr/BlaAttr.lean).

Is there any way to get the fully qualified module name from the declName variable in the second to last line? Right now it prints only the name of the entity that has been tagged.

syntax (name := tag) "tag" str : attr

initialize tagAttr : ParametricAttribute String ←
  registerParametricAttribute {
    name := `tag
    descr := "parametric attribute containing the tag"
    getParam := fun _ stx =>
      match stx with
      | `(attr| tag $tag:str) =>
        return (tag.getString)
      | _  => throwError "unexpected tag attribute"
    afterSet := fun declName tag => do
      IO.println s!"<<ATTR>> {declName}:tag:{tag}"
  }

[Tudor achim]

In fact, I'm having great difficulty registering an attribute that accepts a (String \cross String) parameter; when I try to initialize the corresponding Attr it says it's not found. Specifically this kind of code:

syntax (name := kvtag) "kvtag" str str : attr

initialize kvtagAttr : ParametricAttribute (String ⨯ String) ←
  registerParametricAttribute {
    name := `kvtag
    descr := "kvtag"
    getParam := fun _ stx =>
      match stx with
      | `(attr| tag $tag:str $val:str) =>
        return (tag.getString, val.getString)
      | _  => throwError "unexpected tag attribute"
    afterSet := fun declName tag val => do
      IO.println s!"<<ATTR>> {declName}:{tag}:{val}"
  }

[Mac Malone]

Tudor achim said:

  | `(attr| tag $tag:str $val:str) =>

This line should be using kvtag, not tag.

[Tudor achim]

Thanks. That was a small typo, but fixing it led to the main error I've been seeing:

syntax (name := kvtag) "kvtag" str str : attr

initialize kvtagAttr : ParametricAttribute (String ⨯ String) ←
  registerParametricAttribute {
    name := `kvtag
    descr := "kvtag"
    getParam := fun _ stx =>
      match stx with
      | `(attr| kvtag $tag:str $val:str) =>
        return (tag.getString, val.getString)
      | _  => throwError "unexpected tag attribute"
    afterSet := fun declName tag val => do
      IO.println s!"<<ATTR>> {declName}:{tag}:{val}"
  }

image.png

Seems quite strange. If I change it to be a ParametricAttribute that just takes one parameter then it starts to work again.

[Mac Malone]

@Tudor achim The problem is that you are using the wrong cross character for (String x String) (you are using ⨯(\X) instead of the correct × (\x) character). This causes the parse of the initialize command to fail which then produces strange errors.

[Tudor achim]

@Mac Malone : that solved it. I'm confident I wouldn't have gotten it without that feedback :joy:

[Tudor achim]

Very interesting -- I think I was actually using \times not \X because I'm so used to latex

[Tudor achim]

Also wondering if you have thoughts on the original question:

Is there any way to get the fully qualified module name from the declName variable in the second to last line? Right now it prints only the name of the entity that has been tagged.

The idea is to pull the module name, sort of how you can pull that in python with the inspect module in the context of a decorator.

Looking at https://github.com/leanprover/lean4/blob/3aa1cfcceabf7d091a3b2e5d4330df76767336ac/src/Init/Prelude.lean#L3406 it's not clear you can do this the way I have things set up

[Patrick Massot]

Tudor achim said:

Very interesting -- I think I was actually using \times not \X because I'm so used to latex

\timeswill give you the same thing as \x. The different one is \X which is used for cross-products.

[Kyle Miller]

You can get the namespace for the declName using declName.getPrefix -- or do you mean the module, like the file the declaration is defined in?

[Tudor achim]

Patrick Massot said:

Tudor achim said:

Very interesting -- I think I was actually using \times not \X because I'm so used to latex

\timeswill give you the same thing as \x. The different one is \X which is used for cross-products.

Hmm I just tested that and confirmed you're right. No idea how the \X came in the picture, then, since I never used that in Latex.

Kyle Miller said:

You can get the namespace for the declName using declName.getPrefix -- or do you mean the module, like the file the declaration is defined in?

That's correct, I mean the module, similar to what python's inspect module lets you do from within the decorator function definition.

[Kyle Miller]

Comparing with python is a bit confusing, because python fuses the notions of a module and a namespace, but it's definitely possible to get the module for a declaration in Lean.

[Tudor achim]

Kyle Miller said:

Comparing with python is a bit confusing, because python fuses the notions of a module and a namespace, but it's definitely possible to get the module for a declaration in Lean.

Thanks! I didn't understand this distinction. I think what I actually wanted was to use namespaces, which I've just switched to, and confirm they have the behavior I was looking for (w.r.t. attributes and the Name lookup).

[Patrick Massot]

A useful trick to get even more help is to post #mwe (that's a link). Currently I cannot copy your code into a fresh Lean file and experience the problem you are facing.

[Kyle Miller]

For what it's worth, you can get the filename of the declaration in afterSet from the third argument (that you called val) as val.fileName.

[Tudor achim]

For sure, I thought I was doing that but I see I didn't include the headers. In this case it just uses core Lean

import Lean
open Lean

Either way, you've all been super helpful and my issues are resolved. Thanks!

[Patrick Massot]

The import and open are indeed very important for this.

[Tudor achim]

I can't tell if I'm running into arcane Lean issues or just missing something simple. When I write the following code:

import Lean
open Lean

syntax (name := kvtag) "kvtag" str str : attr

initialize kvtagAttr : ParametricAttribute (String × String) ←
  registerParametricAttribute {
    name := `kvtag
    descr := "kvtag"
    getParam := fun _ stx =>
      match stx with
      | `(attr| kvtag $tag:str $val:str) =>
        return (tag.getString, val.getString)
      | _  => throwError "unexpected tag attribute"
    afterSet := fun declName val ctx => do
      IO.println s!"<<ATTR>> {declName}:{val} {ctx.fileName}"
  }

I get this error:
image.png

From what I can tell, the third argument is a Core.Context as @Kyle Miller suggested:

image.png

Looking at the code for Core.Context, it seems like fileName is indeed a String:
image.png

So I'm really unsure about why the compiler is not accepting this.

[Kyle Miller]

It's something to do with IO.println being incompatible with whatever monad we're in -- when I was testing I switched that to dbg_trace

[Kyle Miller]

    afterSet := fun declName tag val => do
      dbg_trace s!"<<ATTR>> {declName.getPrefix}:{tag}:{val.fileName}"

[Tudor achim]

Great, that also worked for me. It's unclear to me why adding another String triggers an issue with println, though

[Kyle Miller]

I never got IO.println to work at all myself, no matter what string I gave it

[Kyle Miller]

Does IO.println "" work for you?

[Tudor achim]

I think something gets screwed when we add the third argument, it seems to change the expected type.

This works:

open Lean

syntax (name := kvtag) "kvtag" str str : attr

initialize kvtagAttr : ParametricAttribute (String × String) ←
  registerParametricAttribute {
    name := `kvtag
    descr := "kvtag"
    getParam := fun _ stx =>
      match stx with
      | `(attr| kvtag $tag:str $val:str) =>
        return (tag.getString, val.getString)
      | _  => throwError "unexpected tag attribute"
    afterSet := fun declName val => do
      IO.println s!"<<ATTR>> {declName}:{val}"
      -- dbg_trace s!"<<ATTR>> [{ctx.fileName}] {declName}:{val}"
  }

This does NOT:

initialize kvtagAttr : ParametricAttribute (String × String) ←
  registerParametricAttribute {
    name := `kvtag
    descr := "kvtag"
    getParam := fun _ stx =>
      match stx with
      | `(attr| kvtag $tag:str $val:str) =>
        return (tag.getString, val.getString)
      | _  => throwError "unexpected tag attribute"
    afterSet := fun declName val ctx => do
      IO.println s!"<<ATTR>> {declName}:{val}"
      -- dbg_trace s!"<<ATTR>> [{ctx.fileName}] {declName}:{val}"
  }

[Patrick Massot]

There is something a bit subtle going on here. In your afterSet definition, you consume too many arguments

[Patrick Massot]

You could use

initialize kvtagAttr : ParametricAttribute (String × String) ←
  registerParametricAttribute {
    name := `kvtag
    descr := "kvtag"
    getParam := fun _ stx =>
      match stx with
      | `(attr| kvtag $tag:str $val:str) =>
        return (tag.getString, val.getString)
      | _  => throwError "unexpected tag attribute"
    afterSet := fun declName val  => do
      let ctx ← read
      IO.println s!"<<ATTR>> {declName}:{val} {ctx.fileName}"
  }

[Patrick Massot]

There your do computation is in the Attr monad which can lift IO instructions.

[Kyle Miller]

Yeah, taking a third argument is breaking the API of the reader monad.

[Patrick Massot]

Exactly.

[Henrik Böving]

You are operating in AttrM right now. AttrM = CoreM and CoreM can run IO so you can run IO computation there. The issue as patrick says is that you consume too many arguments, that makes your function not be in CoreM anymore but instead in the monad of the remaining CoreM stack so Lean doesn't understand it can lift IO computation there anymore.

[Tudor achim]

OK, thanks all, this works now.

In the interest of understanding how to not have to ask these questions in the future, what's the main way to tell that that's what's happening from the source code of ParametericAttribute? Is it this line that makes it clear afterSet is only called with two arguments?

image.png

[Henrik Böving]

With this issue in particular I would say it is to understand how monad stacks work in Lean and that Reader and State monads are just functions. There isn't a need to read the code of the framework itself.

[Patrick Massot]

Look at the expected type in your original attempt: it says StateRefT' IO.RealWorld Core.State (EIO Exception) Unit. This looks really bad. You should never see such a naked monad. All the interfaces you are meant to use are nicely packaged into named monads defined using the abbrev command so that it's nice to read for you but Lean can see the underlying complexity. So the rule of thumb is: if you see such a thing then you took a wrong turn.

[Patrick Massot]

That being said, you clearly jumped into the deep end of Lean. What you do isn't expected from non-expert users. So really you shouldn't be afraid to ask questions.