search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.83k stars 646 forks source link

Design of attributes needs to be refined #8027

Closed maximedenes closed 3 years ago

maximedenes commented 6 years ago

7920 has raised many questions on:

  1. concrete syntax for attributes
  2. intended use cases
  3. further extensions in sight

It would be good to summarize and discuss them here before preparing PRs addressing those points.

ejgallego commented 6 years ago

We also agreed that discussion will mostly resume on September due to holidays; a few points off of my head:

maximedenes commented 6 years ago

scope, prefix vs suffix: What is the scope of attributes? Are we happy with vernacular-only attributes, or do we want a more refined scope as in OCaml. Also, prefix vs suffix; what do we prefer? Is that easy to implemented with the parser.

The scope of attributes is currently one vernac command. I think it is good as a first step. Do you think we should aim for more immediately?

About prefix vs suffix, I'm not sure what the question is. Do you want a poll among the team? We could certainly do that.

scope II: what should #[foo] Module Foo. do? Do we support some form of attribute inheritance?

This passes the foo attribute to the module vernacular. For example, scoping of Module will probably be relevant, as well as deprecation. We may think about a form of inheritance, but I'm not sure it is required in the first step. Again, feel free to comment on what you think is necessary.

payload: How do we write attributes with payload? What about special symbols [attributes may be used for some translation effort]

I'm not sure I understand what you mean here. Attributes can be written e.g. #attribute(foo = val). Is that what you mean by payload?

How do we reconcile the syntax of payload with options [it seems bad to have Set Warnings +foo and #[enable(foo_warning)] as both valid commands.

#[enable(foo_warning)] is not a valid command.

Dissonance with the actual syntax: indeed that's a concern, attributes look unnatural in the current style and that may be a problem for users.

What do you suggest for a more natural syntax? We can easily change it.

use cases? What attributes do we expect to have. So far, we haven't proposed many new things in this area; what about deriving-style definitions? etc...

I think it is reasonable to consolidate the existing use cases (locality, polymorphism, program, deprecation,...) before introducing others, but feel free to suggest some if you think we should add support for them now. I'm not sure what you mean exactly by deriving-style definitions.

maximedenes commented 6 years ago

@herbelin Independently of the heated meta-discussion on the merge of the PR (in which a miscommunication seems to have happened, but should be addressed in parallel), feel free to raise here your concerns about the current implementation / syntax and suggest alternatives. Once consensus is reached, it should be easy to adjust the current implementation.

ejgallego commented 6 years ago

The scope of attributes is currently one vernac command. I think it is good as a first step. Do you think we should aim for more immediately?

About prefix vs suffix, I'm not sure what the question is. Do you want a poll among the team? We could certainly do that.

Well, certainly suffix/prefix would have an effect on the syntax, a non trivial one I guess; and indeed, it we plan to have more than vernac-command level attributes this needs to be discussed.

Imagine expression-level attributes, then prefix becomes a bit unwieldy.

This passes the foo attribute to the module vernacular.

Well here the question is that attributes now are living in the vernac AST and they are not using the CAst system. This seems like a fundamental design choice that was not considered. In fact, it is incorrect to call them attributes, but they name used in the implementation "vernac flag" seems more appropriate.

Is that what you mean by payload?

Payload can be more general see PPX for examples https://github.com/ocaml-ppx/ppx_import#with-replacements

What do you suggest for a more natural syntax? We can easily change it.

I do think OCaml's syntax seems a bit more natural, but that's a hard thing to state now. I'd rather define functionality and scope first, and more use cases.

I'm not sure what you mean exactly by deriving-style definitions.

Oh, for example you may want to do [@@deriving eqdec, rect, ind], etc... as to derive principles for types. Also, it could be a good way to implement math-comp style classes, etc... many uses come to my mind.

SkySkimmer commented 6 years ago

We should have a list of attributes in the refman like for commands, errors, etc.

herbelin commented 6 years ago

Coming back to this issue, I must confess that I don't see how to make progresses in a way which bring general satisfaction, considering how the positions seem antagonistic.

Personally, I'm still shocked both by the syntax and by what I consider to be a confusion between logical features (Polymorphism, Program, ...) and meta-data (deprecation, silencing a warning, ...).

Now, if I remember correctly, most people expressed that they don't care about the syntax, except @ejgallego and me on one side, and @Zimmi48 on the other side who told me offline that he likes the #[...] syntax. So, maybe, I and @ejgallego can just propose a syntax and try to rally @zimmi48 at it.

Also, besides me (and maybe @ejgallego), no one seem bothered by putting in the same bag features and meta-data.

Obviously, OCaml attributes and Rust attributes are the source of inspiration here. So, seeing both meta-data and logical modifiers as the same kind of objects seem to be part of a contemporary way of thinking. Is it really what we want and need, I'm not sure, but maybe should we follow the move and experiment, like OCaml and Rust are experimenting, and see in a couple of years if we were right or not.

Ideally, in order for me to feel what approach will optimally answer the needs of most of us, I would be interested that everyone gives a little word about what is important for him/her (without restriction to core developers), for instance whether it is precisely important to put in the same unifying bag logic and metadata, whether it is important that the syntax is made different from the current one (up to accepting modifiers in any order) or if it can be the same, etc.

Indeed, if it is globally ok that we reuse the existing syntax for logical modifiers, we could just concentrate on the syntax of metadata, which is really the new feature, and having an OCaml- or Rust- inpired syntax for that, as in:

# Set Warning "-notation-overridden"
Notation "x + y" := (mult x y) : nat_scope.

or, for the cases of several metadata

# Deprecate since 8.8.0, use "*"
# Set Warning "-notation-overridden"
Notation "x ++ y" := (Nat.add x y) : nat_scope.

Actually, with such a freedom in the syntax for providing metadata, we could also address a couple of needs which are notoriously missing, which we currently put into comments, but which would deserve obeying a precise syntax so as to be processed mechanically, e.g.:.

# Contributor: Pierre Untel
# Reference: Bar & Dregt, 1984, 3.1.11
# Revised: 23/5/2018
Definition diamond R := ...

So, shortly, there are a lot of opportunities to seize and we need to all express what we have in mind so as to make progresses.

Additionally, wrt some of @ejgallego's remarks above, doing so that #Set Warnings "+foo" in front of Section or Module extends to the whole module or section seems natural and convenient.

About reconciling the syntax of Set Warnings "+foo" and #[enable(foo_warning)], the above proposal is an answer.

Zimmi48 commented 6 years ago

Thanks for starting this discussion again Hugo!

Now, if I remember correctly, most people expressed that they don't care about the syntax, except @ejgallego and me on one side, and @Zimmi48 on the other side who told me offline that he likes the #[...] syntax. So, maybe, I and @ejgallego can just propose a syntax and try to rally @Zimmi48 at it.

I will be easy to rally. For instance, this alternative syntax that you are proposing looks good to me. If the last questions are only about syntax, we could also consider doing a poll / survey and advertising it on Coq-Club. We could also use the month of beta to finish converging on the syntax.

There was a strong need for a well-parenthesized syntax that was expressed by @ppedrot but I suppose your syntax proposal answers to this need (the left-parenthesis being the # and the right parenthesis the -required- newline).

I also understand your concern of a confusion between logical features and meta-data although it is hard to set a limit: setting a warning to fatal changes the behavior for real. As for the need for attributes, it emerged first for things like turning the positivity check off, a logical feature, and from a protest that the parser was becoming too big.

gares commented 6 years ago

the left-parenthesis being the # and the right parenthesis the -required- newline

What about nesting? (attributes can have arguments, the current syntax allows that). Do you want to use indentation for that?

Zimmi48 commented 6 years ago

Do you want to use indentation for that?

Oh no please.

ppedrot commented 6 years ago

I don't think that you can easily use the newline as a token without fundamentally rewriting the lexer though...

gares commented 6 years ago

Oh no please.

Then you really need a syntax with parentheses. I don't see how the current proposal scales to nested "attributes" (that is a tree).

vbgl commented 6 years ago

Indeed, it seems sensible not to mix comment-like metadata and semantically relevant modifiers. The first are comments; the last attributes. Whether or not we would like to have a formal syntax for comments and whether these formal comments should be handled specially by dedicated tools (e.g. coqdoc) is an interesting but different question.

I agree that the name of a contributor or a link to a reference document belongs to this first kind: comments. However, deprecation or warning-disabling annotations are not mere comments. They do change the semantics of the command. A deprecated tactic behaves differently as a non-deprecated one (ceteris paribus): it emits a warning message, fails if that warning is turned into an error, etc. In that respect, they are similar to a locality annotation, for instance.

The current concrete syntax is not satisfying. Number sign, square brackets and parentheses, commas, …; that’s a lot of annoying symbols. It could be definitely better. That being said, I believe it is easy to evolve the syntax, e.g. based on feed-back from users.

Let me recall that attributes form a forest (i.e., a list of trees): it is not just an association list. Therefore I quite don’t get the “proposal” from Hugo. Would you mind making it a bit more precise (e.g. sketching a grammar rule)? Thanks.

Also I don’t understand Théo’s opinion: accepting ASCII art at the end of lines but not at the beginning. Spacing, apart from being one means of separating words/sentences/tokens/… is mostly used similarly to comments: to improve overall readability. Not to surreptitiously change the meaning of a command.

Zimmi48 commented 6 years ago

I don't have a strong opinion. My comment was just meant to:

  1. encourage the discussion
  2. state that I didn't care particularly about the syntax (I'm not the one to convince)

I don't pretend to be informed enough to do the most relevant comments in this discussion. As long as we get attributes in 8.9, I'm happy.

SkySkimmer commented 6 years ago

Why are attributes trees? If using just lists lets us make the syntax nicer it may be worth considering.

vbgl commented 6 years ago

Using a tree makes the language for attribute values general enough so that there is no need to design a new syntax and implement the corresponding parser for each attribute.

ppedrot commented 6 years ago

To restate my position: I don't have a strong opinion on the actual syntax as long as it is easy to parse (as in having a formally simple to describe grammar) and (in particular) well-parenthesized. It also needs to be generic enough to handle arbitrary payloads (in particular tree-like structures) and be extensible.

As examples, JSON, S-expressions, XML and Bencode fit the bill, in a decreasing order of human-friendliness.

herbelin commented 6 years ago

So, if I understand correctly the point of view expressed by @vbgl and @ppedrot (and maybe @gares), the discussion is about a standard tree syntax as in deprecated(since="8.9.0", note="use ""idtac"" instead") vs an ad hoc syntax per attributes, like e.g. "Deprecated"; "since"; v = token_lexing_version_in_X_dot_Y_dot_Z_format; OPT [ msg = string ], with @vbgl and @ppedrot advocating for a standard syntax generic to all attributes. Is that correct?

Additionally, @vbgl makes the point that I should not mix meta-data which do not have a semantic impact (which he calls comments) and meta-data which have a possible semantic impact. If I combine his distinction with mine, we then have three categories: inert meta-data (as in comments), then a kind of metadata which I could tentatively call meta-attribute (or management attributes, any better idea?), and finally a kind of attribute which is clearly logical, i.e. which has an impact on the "logical" contents of the development (trying to define "logical" as pertaining to typing rules).

As an argument to think at "meta-attributes" as virtually closer to "comments" than to "logical attributes", let me imagine an attribute which says #Prerequisite: diamond has attribute "Reference: Bar & Dregt, 1984, 3.1.11" and which would be a failure if the theorem diamond does not have the expected attribute.

About annotations spreading over several lines, several conventions are possible, like having a \ at the end of the line, or expecting the same indentation + 1 character, and probably other possible conventions.

herbelin commented 6 years ago

Time is running. I'll suppose that the absence of reaction to my last message holds for an approval of the description of the situation.

Then, how to proceed? A syntax easy to parse vs a human-friendly syntax?

For instance, will one be easier to remember? In both cases, the key components of the syntax (e.g. since, or note) shall have to be remembered, so probably not a big difference. An ad hoc syntax could also be more precise (e.g. enforcing the parsing of 8.8.0 vs parsing an arbitrary string "8.8.0") but, in practice, this shall mainly differ in an error message at parsing vs at interpretation time.

@ppedrot, @vbgl (and @gares?), I'm trying to understand why you think that an easy-to-parse syntax is better? Is it that you think Coq went to far in developing ad hoc syntaxes and that we should stop these excesses? Is it that you fear that a specific syntax for each attribute would not scale?

Zimmi48 commented 6 years ago

Time is running.

I think it is OK to change the syntax between the beta release and the final release (this has been done before). Not to say that we should wait the last moment to solve this issue.

Then, how to proceed? A syntax easy to parse vs a human-friendly syntax?

That's indeed very often the dilemma. LISP for instance chose to go all the way towards parsability at the price of readability and the result is that many people (me included) hate the LISP syntax. But many languages achieved a better trade-off: a parser that is still simple enough and yet a syntax that is acceptable and readable for most humans.

the key components of the syntax (e.g. since, or note) shall have to be remembered

Conceptually, they are not necessarily part of the syntax itself. BTW, I think it would help if the documentation of the attribute system included a grammar.

An ad hoc syntax could also be more precise

I think this is indeed what @ppedrot is trying to avoid.

in practice, this shall mainly differ in an error message at parsing vs at interpretation time.

With our current parser, parsing error messages are pretty terrible so the learner would benefit for a simpler (less human but more consistent) syntax that can be learned quickly to get as quickly as possible to a world of interpretation-time error messages only.

Is it that you think Coq went to far in developing ad hoc syntaxes and that we should stop these excesses?

I think this is indeed a perception that is shared by a large share of the developers. @ppedrot being on the front-line on this topic.

gares commented 6 years ago

I'm trying to understand why you think that an easy-to-parse syntax is better?

At the cost of being trivial: because it's easy.

And yes, I hate the not-invented-here syndrome. Picking the syntax of attributes already tested in language X, Y or Z instead of the current one is an option I would evaluate. Inventing a new one is just a loss of time.

herbelin commented 6 years ago

@zimmi48:

I think this is indeed a perception that is shared by a large share of the developers. @ppedrot being on the front-line on this topic.

Can you give examples which feed this perception. For instance, it seems that @ppedrot considers that the diversity of ad hoc tactic syntaxes crossed the red line, but is this the same for you, or for @vbgl?

herbelin commented 6 years ago

@gares:

And yes, I hate the not-invented-here syndrome. Picking the syntax of attributes already tested in language X, Y or Z instead of the current one is an option I would evaluate. Inventing a new one is just a loss of time.

Do you then hate ssreflect syntax :smile:

herbelin commented 6 years ago

@gares: Also, do you regret that ocaml and haskell did not adopt sml syntax? Do you regret that sml syntax did not adopt lisp syntax?

Of course, it is a pain to see languages with close concepts adopt different syntaxes (fn, fun, lambda, ..., or ->, =>, etc., etc.) but in some cases, experimenting something new is worth. It might be successful, it might not. For instance, Agda invented ( x : A ) -> B and this starts to become more and more popular. It has the advantage over Π, or forall, or all to exhibit a natural symmetry with A -> B and it also scales very well to other connectives, giving ( x : A ) & B, ( x : A ) ⊸ B, ( x : A ) ⊕ B, ( x : A ) ⊗ B, ...

ppedrot commented 6 years ago

@herbelin Weren't you lamenting the fact that the revised OCaml syntax never caught on? Its main motivation was easier parsing, by providing well-parenthesized constructs...

Zimmi48 commented 6 years ago

Can you give examples which feed this perception. For instance, it seems that @ppedrot considers that the diversity of ad hoc tactic syntaxes crossed the red line, but is this the same for you, or for @vbgl?

I'm much less radical than @ppedrot on this question but I dislike ad-hoc syntax when they come at the price of inconsistency. And we have many such syntax inconsistencies in Coq (cf. #7971, #8265 and #6567, etc.)

herbelin commented 6 years ago

@ppedrot, revised syntax: the result of political forces in presence decided differently...

@zimmi48: #7971, I agree (but I don't think that the inconsistency was on purpose). #8265, #6567: yes, the syntax could be made closer. By the way, about the difference of semantics, if the syntax of Theorem with were (Co)Inductive Theorem with (or a variant), and that (Co)Inductive Theorem would be allowed without with to mean a proof which starts with fix or cofix, would you find it more consistent with Fixpoint?

Zimmi48 commented 6 years ago

By the way... would you find it more consistent with Fixpoint?

Yes.

but I don't think that the inconsistency was on purpose

No indeed, I think such inconsistencies are never on purpose but arise from the lack of a unified and restricted syntax.

SkySkimmer commented 6 years ago

Attributes have an extensible syntax but the interpretation is not so extensible right now, it has to fit into the static record type Vernacinterp.atts. Where do we want to go with that?

vbgl commented 6 years ago

First, the atts record can have a field that contains the forest of unknown attributes. Then, each interpretation function which receives this record as argument can use it (and implement a second layer of parsing). Finally, a separate pass (between parsing and interpretation, probably before the STM classification) should check that commands only receive attributes they support.

herbelin commented 6 years ago

@vbgl: I had a look at the code which interprets the attributes (in Vernacentries) and, expanding on @skyskimmer's question, I'd like to understand better where we want to go with attributes. But first, I want to apologize that I did not participate to the discussion on the design of your PR, and I hope that my remarks shall not look like arriving like Offenbach's carabiniers!

vbgl commented 6 years ago

  1. Yes, the set of attributes is meant to be extensible. This is why the parser is generic and correctly handles future attributes. Also, the user can learn now how to read and write commands with attributes, even if they do not know yet what the attributes are and what they will do. I believe this is a great advantage over having one specific syntax for each attribute and one very interesting question for every pair of attributes: how do their syntax interact?

    Indeed, there are a few questions to sort out: what happens when an attribute is repeated? with several arguments? are these arguments merged? in a general way or specifically to each attribute? …

  2. Concerning the second layer of parsing, I don’t see how a command could vastly benefit from it: the generic syntax should be general enough. I thought you might be the one to highlight some cases where the generic syntax would be inappropriate and an ad-hoc syntax preferable.

  3. Should an attribute be available for all commands (even the ones yet to be introduced, e.g., in a plug-in) or only for a few? I think that both make sense. In any case, there should be somewhere a table of what command is compatible with what attribute (and a check, as we mentioned). Should an attribute declare the (closed or open) set of commands it knows about or a command declare the attributes it supports?

    Again, both make sense. Here are two examples. An attribute like “instance” or “coercion” which has a definite behavior on every constant that is defined by the execution of a command may be defined on its own and declared to similarly support Definition, Fixpoint, Theorem, Instance. On the other hand an attribute like “local” (taking as argument a named scope) will be interpreted differently by each command supporting it; each of these commands should therefore explicitly declare to support this attribute.

Zimmi48 commented 5 years ago

Am I correct to think that now that @SkySkimmer's PR #8515 is merged, the only aspect of the attribute design that remains to debate is the syntax? (I need to admit that I haven't followed this whole discussion too closely.)

If that's correct, can we first confirm if everyone is supportive of the idea that the ability to have nested attributes is important enough to constraint the syntax to support this in a generic way?

If we can first agree on this, then what about listing a few example syntax that would satisfy this requirement, and then submitting them to a vote through Coq-Club (it might be a good idea to wait a bit before having this vote that more examples of attributes are available).

mattam82 commented 5 years ago

@Zimmi48 I think that's the situation indeed after reading this whole thread again.

I also think that nesting and a generic syntax, easy to parse and process shall be found.

Somehow the #[ ] is a bit scary looking in combination with Coq's syntax. In Equations I used a postfix Equations(noind noelim) foo (x : nat) ... syntax for flags but I don't think that would play well with e.g. a deprecated attribute, and putting the attributes after the command is a no go. So if we put them before the command, I would suggest considering the @[ ] syntax, that Lean adopted apparently https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html#attributes They also have an explicit attribute [blah] syntax for those allergic to symbols. In this case the semantics seem slightly different (mainly hint database addition declarations). Maybe a similar alternative could be added in Coq as well, e.g. Attributes [program, polymorphic] Definition foo.

herbelin commented 5 years ago

If that's correct, can we first confirm if everyone is supportive of the idea that the ability to have nested attributes is important enough to constraint the syntax to support this in a generic way?

Several issues seem interleaved.

The first question is aesthetics. I personally find a syntax such as [# universes(template) ] inconsistent with the syntax design choices made in Coq, and I think @ejgallego had a similar feeling. Other apparently don't have this feeling. Facing that, I don't see how to find a consensus (polling users?).

The second question is a question of motivation. I'm defending the idea that any individual "attribute" concept deserves spending time at thinking at a cool syntax for it. On the other side, I feel that others are somehow bored, or maybe saturated, or maybe indifferent, or maybe discouraged, by the questions of syntax. They prefer to renounce to their own idea of aesthetics to avoid what they believe would lead to endless subjective discussions.

The next question is technical. To support new VERNAC EXTEND with new kinds of attributes, we need to give a syntax to these attributes. If we take a generic syntax, no worry for the VERNAC EXTEND developers, they do not have to think at a syntax for its attributes, it is hard-wired (they still have to think to the name of the attribute though). If we expect any new attribute to come with its own syntax, the developers shall have to define some ATTRIBUTE EXTEND rule defining the syntax. I feel that this is what some of us wants to avoid. They find simplicity more valuable than the intellectual satisfaction of brain-storming a "natural", or "aesthetic", or "to the point" syntax. Is that a correct feeling or do I miss the point?

In particular, we are now well experimented to implement new EXTEND-style grammar and in particular to implement an ATTRIBUTE EXTEND if we want it. But what I don't see is the motivation for it.

Another question is, I would say, cultural. There seems to be a general cultural interest these days in the concept of attribute, with a tendency to wonder if any possible variation to a standard software behavior couldn't be seen as an attribute (one sees the concept of attribute e.g. adopted by ocaml, rust, lean, ...). This is a common form of social behavior, and a useful one, especially in the world of research, because it helps to explore all ramifications of the concept until we start seeing the limits, and developed new, more refined concepts.

I was "born" at a time when this concept did not pervade as it does now, and this is probably one of the reasons I have difficulties to put a notion such as deprecation in the same category as a notion such as polymorphism, and, as a consequence, I don't mind having different kinds of syntax for them. But maybe, I'm missing the interest of having a uniform syntax for both deprecation and polymorphism.

Another question is human. For some reasons, the way attributes have been developed and discussed led to a crystallisation of positions to a point where the search for a common position becomes very hard. I feel powerless with respect to this.

Attributes [program, polymorphic] Definition foo.

I'd be more comfortable with such a syntax which I find more consistent with the current design. Then, there will be the requirement to allow nesting also.

I don't know if it is time to summarize or if we should wait for more discussions. At least, I'd be glad to have an answer to the following questions: is my feeling that the current syntax is not particularly aesthetic and consistent only mine (and the one of @ejgallego)? Is the silence of several of us on expressing their own idea of aesthetics the sign of a wish to avoid syntax discussions which are feared to be endless and subjective anyways? How to precisely avoid subjectivity and collect spontaneous user feedback on the current generic syntax? Can we feed the discussion by imagining more complex kinds of attributes than the "deprecated" one, which seems to be the more complex we have currently?

herbelin commented 5 years ago

While the topic is hot, I played a bit with deprecation. Let me report on a few behaviors I observed and ask if this is on purpose. In particular, what is the intended meaning of the since field? Since we can call Coq with a specific version compatibility number, shouldn't it be at least for that reason interpreted? Here is what I got:

#[deprecated(since="JC")] Tactic Notation "f" constr(a) := exact a. (* shouldn't it be an error *)
#[deprecated(since="8.11")] Tactic Notation "g" constr(a) := exact a.
Goal True.
f 0.
(* Warning: Tactic Notation f (constr) is deprecated since since JC *)
g 0.
(* Warning: Tactic Notation g (constr) is deprecated since since 8.11 *)
(* shouldn't it be no warning? In particular, if I call coq with a specific version
   compat, shouldn't it be used to decide if the warning should be emitted or not*)

Probably not a big deal to add a test if ever this behavior is not intended.

I also observed the following:

#[deprecated(since="8.4.0")] Definition b := 0.
Check b.
(* No warning, but I guess it should? Or do I miss something? *)

In any case, giving the ability to deprecate is a very good feature.

SkySkimmer commented 5 years ago

I also observed the following:

[deprecated(since="8.4.0")] Definition b := 0.

Definition silently ignores the deprecated attribute. We could fairly easily make it error with "unsupported attribute", or with more difficulty implement deprecation for definitions.

mattam82 commented 5 years ago

Indeed Hugo, I think you have it right saying that most of us want a simple syntax that's easy to parse and process, and hoping to reach consensus on aesthetics can be exhausting. Also, there are clearly antagonistic positions on syntax and to me that's just a fact of life. I don't particularly like #[] either, but we could as @Zimmi48 proposed poll the devs and the users about the different options we have, starting with the generic one in the beta, and see if there is a clear trend to inform our decision. Can we agree on this process, ending it with a vote among the core development team if need be?

About the difficulty to implement per-attribute syntax, I guess I would be good to have @ppedrot 's opinion.

From my point of view, polymorphism/monomorphism can well be an attribute, I'll rarely use it because I usually have Set Universe Polymorphism on. Same for Program, I'll usually use Set Program Mode instead. I think we should not focus on those two which modify the typechecker behavior. I rather see attributes as a mechanism to uniformly treat local/global/export? instance, coercion, hint(hintdb), derive(eq_dec) etc.

SkySkimmer commented 5 years ago

Attributes [program, polymorphic] Definition foo.

That certainly feels more Coq-like, but I think at some point we want to have inline attributes (this is partly what the CAst stuff was meant to enable) and there it seems less likely to work (we not going to write fun (x: Attributes [foobar] bla) => ...). I don't remember what inline attributes were considered desirable though. In ocaml we've used "locally disable this warning". In fact while I'm mentioning inline attributes, we should probably consider them with significant priority in this discussion.

Since we have the . delimiter if we only attached attributes to toplevel commands a syntax like [foo, bar] Command could work fine (if the # is what's bothering people). Maybe something like

[Instance, Polymorphic] Lemma paths_trans {A} : Transitive (@paths A).

I have no clue about syntax for inline attributes (especially since just about anything is liable to collide with notations).

Another question is, I would say, cultural. There seems to be a general cultural interest these days in the concept of attribute, with a tendency to wonder if any possible variation to a standard software behavior couldn't be seen as an attribute (one sees the concept of attribute e.g. adopted by ocaml, rust, lean, ...). This is a common form of social behavior, and a useful one, especially in the world of research, because it helps to explore all ramifications of the concept until we start seeing the limits, and developed new, more refined concepts.

I think that's a misunderstanding of the lean view of attributes (although that's only from my reading of the link to their doc in https://github.com/coq/coq/issues/8027#issuecomment-435947135). I read lean attributes more as flags which get attached to arbitrary globals. As they say:

But some commands have other effects on the environment, either assigning attributes to objects in the environment, [stuff that's not talking about lean attributes]

This seems very clearly separate from kernel mechanisms (such as universe polymorphism). Instead you have some environmental map global -> attribute set which attributes may modify as they wish.

gares commented 5 years ago

If you want the same syntax to be parsable everywhere just introduce a new keyword eg attr in place of or as an alternative to #. Within constr both # and attr could appear already, but renaming attr is, for the user, simpler than changing his notation using #.

I personally prefer a short and discrete kwd or a symbol to Attributes the point being that what matters is what follows it.

Zimmi48 commented 5 years ago

Yes, I suggested polling users and yes, I think we need more examples of attributes to feed the discussion. I regret that attributes made it into 8.9 in the current state of affairs but as long as we add some note in the manual saying "The attribute mechanism is very experimental and is likely to evolve in Coq 8.10 (including the syntax).", this should give us more freedom to take the time to collect unsolved questions, alternative syntax and prepare a poll to users (unless a consensual solution emerges). I think no one is radically attached to #[ in particular.

gares commented 5 years ago

But to me it is also true no one came up with a clearly better proposal... so maybe it means that the current syntax is not so bad after all (if it was bad one would easily find a better one).

I'm not so sure polling users about a syntactic matter would help converging. Especially with an open question. You could say "option a, b and c: which one you prefer?", but I don't think we have more than "option a" here.

I don't think encouraging users not to use attributes is wise. I'd rather encourage them to use them, and if it turns out to be a wrong syntax, given that it is parsable easily, we can always provide a little tool to turn #[ into @[ or whatever we may come up with. If it was possible to do that for terms in the v8 transition, I'm pretty sure we can do that for attributes.

Zimmi48 commented 5 years ago

I'm not so sure polling users about a syntactic matter would help converging. Especially with an open question. You could say "option a, b and c: which one you prefer?", but I don't think we have more than "option a" here.

Yeah, I'm talking of a poll with a closed question. That's why I was saying that we need to gather proposals first.

I don't think encouraging users not to use attributes is wise.

OK, but there has not been any concerted strategy wrt the communication to adopt. In any case, in 8.9 the attributes do not bring much feature-wise.

herbelin commented 5 years ago

But to me it is also true no one came up with a clearly better proposal... so maybe it means that the current syntax is not so bad after all (if it was bad one would easily find a better one).

I would not say that but rather that noone came up yet for a case of attribute which requires more than the existing syntax (except deprecation for which I personally think that a syntax such as e.g. #[Deprecated since version x.y.z ("some comment")], or #Deprecated since version x.y.z ("some comment") (which incidentally is closed), or Deprecated [since X.Y.Z] Tactic Notation ..., etc. (there are many possibilities which would marry well with the current style of syntax).

For the record, the existing syntax is to list attributes the ones after the others as in Local Polymorphic Program (and for the record, it is technically not an obstable to make the parser accept them in any order).

About the current syntax, to my knowledge, I heard only @zimmi48 expressing an opinion on it, which is that he was not finding clear what the main word was in a list of words such as Local Program Definition. So we could indeed add, say, brackets and get [Local Program] Definition.

On the other side, to push things at the extreme, we could also consider that Definition is an attribute which is selected among a number of possible values such as Theorem, Lemma, Example, etc., and to then accept Local Definition Program with the words in any order.

I don't think encouraging users not to use attributes is wise.

This sentence is ambiguous. Again, there are already attributes, which are called Local, Polymorphic, etc. and we never discouraged users to use them. The only effective attribute which is not covered by the current syntax is deprecation. So, certainly, we should encourage users to use deprecation but maybe should we first give it a real meaning and not to stay with the current unclear situation which, at best, doesn't check the version, as in Tactic Notation, and, at worst, is a silent noop as in Definition.

So, to let the discussion advance, I urge us to list the (new) attributes which we want to eventually provide. Otherwise, we shall not be able to convince anyone that #[local] is better than Local.

(Edited to clarify the meaning of a word which was interpreted as hurting.)

maximedenes commented 5 years ago

the current "joke"

I don't find particularly respectful to use the word "joke" to describe the work of others. I myself very often refrain from using words that come to my mind, but if others don't, I won't bother much longer...

herbelin commented 5 years ago

In fact while I'm mentioning inline attributes, we should probably consider them with significant priority in this discussion.

A typical inlined attribute would/could have been dont-check-guard in fixpoints.

Definition silently ignores the deprecated attribute. We could fairly easily make it error with "unsupported attribute", or with more difficulty implement deprecation for definitions.

Would warning about the deprecation at the time of requesting the name in the nametab be a good way to proceed?

herbelin commented 5 years ago

@maximedenes: First I'm not qualifying the work of others as "joke". I'm very happy of the work done on attributes which really improves on the existing. I'm only qualifying of "joke" to pretend that we have a deprecation attribute while it does not work.

Moreover, I used the word "joke" as a provocation (as I said it explicitly). Apparently it worked (as a provocation) but unfortunately not as the expected result of the provocation. The expected result is that someone responsible really considers that "deprecation" works before telling that it should be used.

ejgallego commented 5 years ago

Indeed as with many other project in Coq attributes didn't have an easy birth, due to a variety of reasons, but IMHO the situation is improving quickly, in particular thanks to @SkySkimmer and @ppedrot work on coqpp + the attributes PR.

Still indeed the main problem seems like we never defined the use cases clearly enough, in particular the handling of Coercions, Obligations, Local, etc... is already problematic in the core layers to some extent, so indeed starting from the syntax won't get us very far if the base is lacking orthogonality.

Regarding the syntax I am not sure I like Rust as a model too much; first, because it is not really a functional programming language, second because even if hyped it is largely a newcomer and yet immature, and third because we are not sure the use cases overlap.

Even so, I think the current proposal is acceptable, and should provide a good basis for further development; but it could be well the case that attributes shall remain "experimental" for 1 or 2 releases more until we reach a consolidated implementation.

ejgallego commented 5 years ago

I myself very often refrain from using words that come to my mind, but if others don't, I won't bother much longer

Indeed the choice of word is unfortunate, while we can all agree that the roadmap for attributes implementation suffered of serious problems; we should remain positive and try to move ahead. Using provocation is not the best way to achieve that IMVHO.

On the other hand it seems to me that "threatening" to use bad comments because a person did a bad comment lacks soundness at most reasoning levels. We all are not perfect however we should aim to de-escalate IMO, not to retaliation.

gares commented 5 years ago

What is the link between attributes and coqpp?

Zimmi48 commented 5 years ago

A typical inlined attribute would/could have been dont-check-guard in fixpoints.

Indeed, I think that's the plan for #7651.

I would not say that but rather that noone came up yet for a case of attribute which requires more than the existing syntax

Well, about the need for nested attributes, if I understood correctly, there was the proposal to change the polymorphic / monomorphic / template / notemplate attributes into sub-attributes of a universes attribute. This sounds like a good proposal to me.

Regarding the deprecated attribute, even if I agree with Emilio's comment on the choice of words, I must say that I am not happy that #8075 which I opened almost four months ago did not get any answer and #8382 which I opened more than two months ago did not find any answer in Coq 8.9.