TagAttribute

Stream: mathlib4

[Jireh Loreaux]

I'm clearly not understanding how to get tag attributes working. For instance, I try to register a new one in this file:

import Lean.Attributes

open Lean

/-- user attribute used to mark lemmas used by `continuity`. -/
syntax (name := continuity) "continuity" : attr

initialize continuityTag : TagAttribute ←
  registerTagAttribute `continuity "Tag for marking lemmas used by the `continuity` tactic"

and then use it here, but I get an error:

import Mathlib.Tactic.Topology.Attr
import Mathlib.Topology.Basic

attribute [continuity] continuous_id continuous_const -- unexpected attribute argument

[Floris van Doorn]

A TagAttribute can only be given to a declaration in the same file as where the declaration is defined (this allows TagAttributes to have to do almost no initialization when resolving imports).

[Floris van Doorn]

Also, you should remove the syntax line. Just

import Lean.Attributes

open Lean

initialize continuityTag : TagAttribute ←
  registerTagAttribute `continuity "Tag for marking lemmas used by the `continuity` tactic"

is enough

[Jireh Loreaux]

Oh, I guess a TagAttribute is not what I want then. How do I create an attribute which just acts like a flag?

[Floris van Doorn]

why is TagAttribute not what you want? It is the cheapest attribute that is just a flag. You just have to make Mathlib.Topology.Basic import Mathlib.Tactic.Topology.Attr and flag the declarations in that file.

[Kevin Buzzard]

But won't Jireh want to tag lots of lemmas from different files with his attribute?

[Kevin Buzzard]

Oh I see -- the idea is that the lemmas are all in different files, but you do the tagging all in one file?

[Jireh Loreaux]

No, that can't be the case.

[Jireh Loreaux]

Floris, did you mean "in that file, or in files imported by it"?

[Kevin Buzzard]

I mean, simp doesn't work like that -- imagine not being able to tag a lemma with @[simp] as you write it, but having to add it to some gigantic file with many imports which needs to be imported if you want to use simp.

[Jireh Loreaux]

Kevin, it wouldn't work anyway because then you would have circular dependencies.

[Floris van Doorn]

What I said was probably confusing. If you want to tag continuous_id with @[continuity], this has to be done in the file where continuous_id is defined. You can still write @[continuity] lemma continuous_id ....
Isn't that what you want?

[Kevin Buzzard]

(deleted)

[Jireh Loreaux]

I think I tried doing that in this file and still had the same error. I'll check in about an hour when I can sit down again at my machine.

[Kevin Buzzard]

Oh I had misread "in the same file as where the declaration is defined" as "in the same file as where the attribute is defined" :-)

[Jireh Loreaux]

Me too, Kevin

[Floris van Doorn]

Floris van Doorn said:

Also, you should remove the syntax line.

Did you do this?

[Jireh Loreaux]

Ah, not at the time, that's probably the issue

[Heather Macbeth]

Floris van Doorn said:

What I said was probably confusing. If you want to tag continuous_id with @[continuity], this has to be done in the file where continuous_id is defined.

@Floris van Doorn This isn't the only way, right? You can also tag things @[continuity] after the fact, it just has to be in a different file from where @[continuity] is defined. See !4#1740 for an example.

[Floris van Doorn]

@Heather Macbeth After a little bit of investigation, we are both right and we are talking about different things.

In Lean there is a notion of TagAttribute defined in Lean.Attributes, which you can declare using

initialize someName : TagAttribute ← registerTagAttribute `tagName "description"

If you then run attribute [tagName] id in a different file, you get the error

invalid attribute 'tagName', declaration is in an imported module

However, @Scott Morrison defined a separate notion in Mathlib.Tactic.TagAttr called TagExtension which you declare using register_tag_attr attrName. This is not implemented using TagAttribute, but instead with SimpleScopedEnvExtension. This is a type of attribute that is closer to what you are expecting in Lean 3: you can tag declarations in files different from where the declaration (that you're tagging) is defined, and (I think) you can tag things locally in a section or file, or locally remove the attribute. However, they are a little less efficient, since you have to collect all the declarations with this attribute whenever you execute the imports of a file, unlike TagAttribute.

So the problem is that we have two different notions that have the same name. @Scott Morrison can you please rename your type of attribute, so that it doesn't sound like TagAttribute? There are plenty of possible names: SimpleAttribute, MarkAttribute, NoArgumentAttribute, ... It is just confusing to have a difference between tag attributes and "tag" attributes.

[Floris van Doorn]

Or as Reid's emoji suggest LabelAttribute or just Label :smile:

[Scott Morrison]

!4#2124