RFC: generic attribute syntax

[aspiwack]

See rendered.

[aspiwack]

I wrote this a while back. Just unearthed it, and it seems to me that after all this time it still holds up pretty good in my eyes, which is a good start. I hacked a prototype at the time to ensure feasibility, but I can't find it at the moment. I'll put it online soon.

[herbelin]

Thanks for initiating the discussion, but if I had to vote for a syntax for attributes such as Program or Polymorphic, I would simply be happy with (extensions of) the existing one, so I would prefer that you remove my name in the sentence showing a parenthesis-based syntax (though it is true that I care for general consistency of syntax, as probably some of us have already noticed!).

For the record, there are examples of attributes in Isabelle here and in Lean here, though it is probably more about registering an effect of the definition for the sequel (as Hint does) than modifying the behavior of the command as we discuss here.

[cmangin]

Quick question about the syntax: wouldn't it clash with something like Goal (True).?

Also, it has been discussed a bit on Gitter, but what about attributes which are not idempotent, such as Fail (or even Time which should not be idempotent imo)? Would they become simple attributes, stay as vernacular commands, something else?

[maximedenes]

FTR, I started to work on the attributes mechanism. It will probably not be extensible by plugins in its first version. I think the syntax should be discussed last.

[ejgallego]

wrt to @cmangin comment, I think that Fail and Time should not be attributes, but "commands", similar to Abort etc...

My reasoning is as follows, for an input of Fail X (or Time X) , the execution of X is not modified (as opposed to attributes), but instead X is run unmodified and then the caller acts on the result.

[maximedenes]

Attributes should commute. Fail, Timeout and such do not.

[ejgallego]

Yup, I propose we call these kind of "meta" constructions "commands", but better alternatives are welcome.

[ppedrot]

I'd be in favour of a syntax that is not tied to the Definition command, because attributes make sense for any vernacular command in general. So it'd be better if it were uniform across the commands and it didn't disrupt the parser any further. I like for instance something that you would put above that command, like e.g.

#[attr₀(attr₁), attr₂]
Definition foo := nat.

EASY PARSING. That's one of the reasons for the introduction of attributes, remember?

[Zimmi48]

It will probably not be extensible by plugins in its first version.

Fine, but it is important that at some point it becomes user-extensible. So you should keep this in mind.

I'd be in favour of a syntax that is not tied to the Definition command, because attributes make sense for any vernacular command in general. So it'd be better if it were uniform across the commands and it didn't disrupt the parser any further.

👍

Local (de)activation of scheme generation

Something similar could be useful for locally disabling a warning, as in OCaml.

[aspiwack]

@herbelin says

I would prefer that you remove my name in the sentence showing a parenthesis-based syntax

Sure I removed it. Though you are on record making this very proposal.

@maximedenes says

FTR, I started to work on the attributes mechanism. It will probably not be extensible by plugins in its first version.

Good! I found my implementation and uploaded it here (old and unrebased): https://github.com/aspiwack/coq/tree/attributes . Feel free to steal any code there, it's already plugin-ready, I think. If you want a hand, I can lend a little of my time to contribute on your branch (but I'll certainly be slower than you).

I think the syntax should be discussed last.

What is there to discuss then? It's almost entirely a syntax thing. The rest, at least as designed here, is mostly trivial. Expect maybe the contract with plugins. Do you have extra thoughts that I have missed? If so please share them, I'm most excited to know!

@ejgallego says:

I think that Fail and Time should not be attributes, but "commands", similar to Abort etc...

I agree.

@Zimmi48 says:

Something similar could be useful for locally disabling a warning, as in OCaml.

Yes please! Though not something similar: the same thing.

@ppedrot says:

I'd be in favour of a syntax that is not tied to the Definition command, because attributes make sense for any vernacular command in general.
[…]
EASY PARSING. That's one of the reasons for the introduction of attributes, remember?

Well, the proposed syntax is certainly easy to parse. Except in the Goal case, as @cmangin rightly points out. Do we care? If so, we can't use a syntax just after the command name.

It was never the intention to tie the construction to the Definition keyword. But to all « declaration-like » keywords. It imposes more of a burden on the implementation of the parser, also on plugin writers who want to introduce an new keyword like this (they have to remember to add the appropriate attribute invocation on their keyword). On the other hand, I like that it makes the attribute really look first class: they are part of the definition, not a mere addition pasted on top.

That being said, I think we can boil down the question of whether it should be attached to every vernacular (probably at the beginning of the invocation) or tied to declarations to the following question: do we want attributes on tactics?

Minor consideration: [<attributes>] Fail Definition … may change failure status depending on attributes, which looks a bit weird. Fail Definition (<attributes>) will too, but it doesn't look that weird.

Also, I just found a question that does need answering: how do we treat attributes on Lemma foo : Bar.? Do they affect the entire interactive definition? Only the definition of the type? Only the type and the registration at Defined/Qed?

[maximedenes]

Good! I found my implementation and uploaded it here

Thanks, I'll have a look.

What is there to discuss then? It's almost entirely a syntax thing.

Well, the implementation, the API, the migration strategy?

whether it should be attached to every vernacular

I think every vernacular should be able to support attributes (but wouldn't have to). Don't forget that modifiers like Local/Global make sense for Set, for instance.

Minor consideration: [] Fail Definition … may change failure status depending on attributes

I think that doesn't look so strange when you think.

Also, I just found a question that does need answering: how do we treat attributes on Lemma foo : Bar.? Do they affect the entire interactive definition?

I'd say yes, isn't it what Polymorphic does for instance?

[ejgallego]

I think we can distinguish two classes of command modifiers:

• modifiers that can be applied without requiring any knowledge of the command proper [maybe locality in the future, control vernacs, syntax stuff such as deriving, etc...]
• modifiers that require the command being modified being aware of the modifier internally.

So for the first class, it is OK to have a common syntax and have the interpretation layer take care of it. However, for the second kind of commands, it should be the command itself who should declare its capabilities at registration time, as there is not way for the command to read the future and IMHO we don't want to implement a defadvice system yet.

IMO, depending on the capability set, the corresponding parsing rules should be added, etc...

[SkySkimmer]

I never really understood this CEP. Is it just a syntax for setting options locally to a command?

[aspiwack]

@SkySkimmer I wouldn't put it this way. Using a similar language, we could say that it is a way to give an option syntax to vernacular commands. It can be used to locally set options (in the sense of Set) locally to a vernacular command. In fact we may want to think of a generic way to do this, and make sure it's included in the proposal.

But it is not the only usage. We already have options to command, currently, like Program for Definition. But we have to roll bespoke syntax for each of them, and it is the opinion of some of the participants in this thread it has become unsustainable. Therefore the proposal for a generic syntax once and for all.

By the way, I know that work has been happening on this (@maximedenes you are overseeing this right?), but it may not be quite the same as what I proposed here. So I'd like to take the opportunity of this comment to say that I'm still maintaining this proposal, and that any suggested change is welcome (there are a handful of suggestion above, but the activity here has been to low for me to incorporate). It'd be super nice the work that is being implemented to reflect the content of this proposal, so any planned deviation should be reported here.

Anyway, back on topic, @SkySkimmer if you have any suggestion of rewording of the motivation section to make the purpose clearer: please share!

[Zimmi48]

@vbgl has been doing the work. Cf. most recent discussions in rocq-prover/rocq#7651 and rocq-prover/rocq#7644.

[SkySkimmer]

But it is not the only usage. We already have options to command, currently, like Program for Definition. But we have to roll bespoke syntax for each of them, and it is the opinion of some of the participants in this thread it has become unsustainable. Therefore the proposal for a generic syntax once and for all.

But that is locally setting the Program Mode option.

ie let's say we make a syntax for locally setting options, such that

[Foo Bar, !Bar, Baz Bli "bloop"] Definition ...

means

Set Foo Bar. Unset Bar. Set Baz Bli "bloop".
Definition ...
(* reset options to whatever they were before *)

Would that be different from attributes and if so how?

[ejgallego]

@vbgl has been doing the work.

Umm, I think indeed that we suggested Vicent to implement attributes but we don't really have a design document of many parts of the system other than some brief chat a few months ago. It looks to me indeed that we should stop doing more "attribute" work until we have a clearer picture of the global design.

The strongly-typed vernac classification is related but quite orthogonal to attributes per-se; I think that design is clear apart from some GADT-technical problems that arose, but indeed, for the attributes story, many details seem to be missing.

[Zimmi48]

Indeed, the view that attributes are just a way to set an option locally looks like a reasonable approach... It could lead to a much simpler design.

[Zimmi48]

But in this view, you can no longer raise an error when an attribute makes no sense for a command.

[aspiwack]

Umm, I think indeed that we suggested Vicent to implement attributes but we don't really have a design document of many parts of the system other than some brief chat a few months ago. It looks to me indeed that we should stop doing more "attribute" work until we have a clearer picture of the global design.

The idea that we ought to have a full-blown design before implementing is optimistic. Let's not stop a good implementation effort just because we don't know 100% where we're going: sometimes the quickest way to discover difficulties in a design is to just try it out.

To me the purpose of proposals such as this one is to make conscious design choices. They don't need to be made before implementing. But this avoids making design choice by accident. Plus it allows careful review of the design independently of the implementation itself (mostly to make sure that there is no place left for accidental design).

Would that be different from attributes and if so how?

Let me answer by a question: is (λx y. u) v w the same thing as temp := y; y := w; (λx. u) v; y := temp?

To be a little more explicit. It is always possible to make this sort of transformation, but not necessarily natural (or desirable).

Yet another way to cast your question is: should every attribute have a corresponding option? It's not necessarily a bad idea, but we should be careful about this.

Example attributes which we may want to consider:

• Local vs Global vs notion?
• Register this definition as hint

Also, if we use options to parametrise vernac commands, then there is no room for plugin to extend the behaviour of an existing vernac command.

To be clear: these are all ok choice. But we need to be conscious of the choice we are making.

[Zimmi48]

Register this definition as hint

👍

BTW, it is indeed funny to me to read the critic of a lack of design document for the rare occurrence where there was a CEP. On the contrary, the initial PR adding attributes in the AST (a major PR that was heavily compatibility-breaking) was lacking such document and it was far from obvious to other developers what the pursued goal was...

[ejgallego]

BTW, it is indeed funny to me to read the critic of a lack of design document for the rare occurrence where there was a CEP. On the contrary, the initial PR adding attributes in the AST (a major PR that was heavily compatibility-breaking) was lacking such document and it was far from obvious to other developers what the pursued goal was...

I think that precisely what we are doing here is critizising the lack of design for the AST changes, as we are continuing that roadmap and somehow it is being implied that such changes were supported by this CEP which were not. Maybe I am getting lost in all the confusion, or I am missing something.

That being said, the PR modifying the AST was properly reviewed, well justifyed IMHO [it fixed a concrete class of problems], and far from a major compatibility break. However, in order to continue with that line of refactoring, it seems indeed we have some thinking to do first. For example, most attributes seem to pertain definitions, other are about options; so a global vernac system doesn't seem to be the most efficient one.

[ejgallego]

for the rare occurrence where there was a CEP

Well that would be offtopic but I do believe that actually properly documented PRs may make a better system than CEPs, so far the success of CEP is at best moderate, and in quite a few cases they came after-the -PR.

[Zimmi48]

I would rather say that the current attribute work piggy-backs on the "generic attribute in AST" changes. Maybe there is a misunderstanding due to the same name being used in both case. But indeed, I don't think that extending this "generic attribute in AST" feature was the only way to proceed to implement the present CEP.

[Zimmi48]

That being said, I personally care more about the user-side feature itself than the implementation.

[Zimmi48]

Despite the actual feature having some small differences from the initial proposal in this CEP (syntax, program attribute not yet split into multiple sub-attributes), this CEP has very much been concretized. In order to reduce the list of open CEPs, I propose to merge it (as is).

[gares]

agreed

[aspiwack]

Please go ahead. I don't appear to have merge powers anymore.

I'm very happy to read that next time I will be using Coq, there will be an attribute syntax for me to enjoy 🙂

[Zimmi48]

I'm very happy to read that next time I will be using Coq, there will be an attribute syntax for me to enjoy 🙂

The syntax was introduced in Coq 8.9, but with only one new feature associated with it (the deprecated attribute), then in 8.10 there was an attribute for template polymorphism. In 8.11, the refine attribute for Instance was introduced and Section was extended to support the universe polymorphism attribute. In 8.12, the documentation of attributes was much improved, with a new index of attributes and with an explicit presentation of the syntax of new and legacy attributes, and more prefixes were turned into legacy attributes (with a corresponding "new" syntax). Since this version, legacy attributes can be passed in any order. Finally, in 8.13, boolean attributes were introduced and the initial discussed use case (the ability to disable locally positivity or guard checking) got its attribute!