Convert Vernacular section of gallina chapter to use prodn

[jfehrle]

Work in progress. Please take a look at the added grammars and changed commands. But I also need your input on several things (below) so I don't end up having to do things twice.

[jfehrle]

First, would you delete the prodn_gallina branch I created by mistake in coq/coq?

1. For the section "The Vernacular":

• It looks like vernac_toplevel recognizes a single command and I don't see in the grammar how the tactics are invoked. Seems like I should invent a commands nonterminal for the documentation and replace the initial grammar.
• Should we mention or describe proof mode here or in the proof handling chapter?
• Include a general description of Local/Global, Polymorphic/Monomorphic flags here? Don't know how many commands actually accept these parameters. I'm leaning toward showing these flags only in the syntax for the commands that accept them (a bit of work to set up and maintain, but good for users).
• Where should we describe quoted_attributes for commands--not sure how many commands that applies to and whether it's a common enough feature to get into right here.

2. Assumptions section:

• Is it reasonable to describe all of Axiom, ... Variables in the same spot, perhaps with a table and brief text explaining the differences based on the mlg settings ("Axiom" -> { (NoDischarge, Logical))? And if so, then delete all the variants immediately after the grammar?

3. I renamed some cmd and cmdv's to, respectively xxxFixME and xxxVar. Should some of these (e.g. SubClassVar and VariableFixMe) become the primary description of those commands, or can the be together with their related commands that share syntax (other than the command name)?

4. Updating the cmds is fairly manual. I have code to compare the set of cmd's in the manual to those I get from the grammar, so there will be a reasonable automated check. For cmdvs, the problem is harder: I could create edits to generate all the cmdvs as extra hidden parts of the grammar and then check them as I can for the cmds, but the edits are tedious to set up. I think I'd prefer sharply reducing or even eliminating the cmdvs.

[jfehrle]

Also, should Let Fixpoint and Let CoFixpoint be documented together with, respectively, Fixpoint and CoFixpoint?

[Zimmi48]

I don't see in the grammar how the tactics are invoked

Tactics cannot be parsed outside of proof editing mode. Proof editing mode is activated when running some commands, like Lemma. The parser is then switched. There exist several proof modes, see relevant documentation:

• https://coq.github.io/doc/master/refman/proof-engine/proof-handling.html#switching-on-off-the-proof-editing-mode
• https://coq.github.io/doc/master/refman/proof-engine/proof-handling.html#proof-modes

Should we mention or describe proof mode here or in the proof handling chapter?

In the proof handling chapter.

Include a general description of Local/Global, Polymorphic/Monomorphic flags here?

The general description of Local / Global is here: https://coq.github.io/doc/master/refman/proof-engine/vernacular-commands.html#controlling-locality-of-commands
Seems like a completely random location.
Anyway, despite not being deprecated, these flags are mostly intended to be replaced by their equivalent attributes (#[local], #[polymorphic], etc.), so we should not focus on them, but rather on how to properly document attributes. Given that attributes have a standard syntax and can be given in any order (that's the whole point), we should not document them in the command syntax description like we used to do with flags (and like is done here: https://coq.github.io/doc/master/refman/language/gallina-extensions.html#canonical-structures). Instead, for each command, we should give the list of attributes it supports, and link to the documentation of said attributes. I'm thinking that attributes would deserve their own specific directive.

Is it reasonable to describe all of Axiom, ... Variables in the same spot

I would prefer to clearly separate Axiom / Parameter / Definition / Lemma / Fixpoint on the one hand, and everything that is relevant to sections, like Variable, Hypothesis, Context, Let, Let Fixpoint, on the other hand.

EDIT: but given the shared syntax, describing similar commands in a single place makes sense as well.

[jfehrle]

Anyway, despite not being deprecated, these flags are mostly intended to be replaced by their equivalent attributes (#[local], #[polymorphic], etc.), so we should not focus on them, but rather on how to properly document attributes. Given that attributes have a standard syntax and can be given in any order (that's the whole point), we should not document them in the command syntax description like we used to do with flags (and like is done here: https://coq.github.io/doc/master/refman/language/gallina-extensions.html#canonical-structures). Instead, for each command, we should give the list of attributes it supports, and link to the documentation of said attributes. I'm thinking that attributes would deserve their own specific directive.

That makes sense. It makes the presentation simpler and probably a bit less effort. But instead of creating a new directive, I would just add sentences just below the syntax presentation such as "You can prefix this command with Local" with a hyperlink on "Local". (Hmm, how you look up "Local" or "#[local]" in the index?)

#[local] seems like syntax only a mother could love :-(.

[jfehrle]

I would prefer to clearly separate Axiom / Parameter / Definition / Lemma / Fixpoint on the one hand, and everything that is relevant to sections, like Variable, Hypothesis, Context, Let, Let Fixpoint, on the other hand.

EDIT: but given the shared syntax, describing similar commands in a single place makes sense as well.

It looks like Axiom, Conjecture, Parameter are synonyms and that Hypothesis, Variable are synonyms, which I can reflect a little better.

Are Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property all synonyms? Seems like the variant for "Definition" just below the variant for "Theorem". Also "Let" is under both "Theorem" syntax and "Definition" syntax. Which is the right place?

Also, Example and Definition are equivalent but SubClass is different.

I think I'll seperate SubClass from Example and Definition. Are Example and Definition completely equivalent?

(Still need to update some of the variant commands...)

[jfehrle]

Updated. Probably better for you to respond to my comments rather than read the output closely.

[Zimmi48]

instead of creating a new directive, I would just add sentences just below the syntax presentation

Using a dedicated directive allows to create an index of attributes. Then we could write such sentences below the syntax presentation of the command, but it would be something like:

This command supports the following list of attributes: :attr:`local`, :attr:`global:,
:attr:`universes`, :attr:`deprecated`.

Note that when I'm talking about attributes, I'm not including ad-hoc syntax like Local (which are meant to be deprecated eventually).

It looks like Axiom, Conjecture, Parameter are synonyms and that Hypothesis, Variable are synonyms, which I can reflect a little better.

Yes

Are Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property all synonyms?

Yes (and Definition can also be used in place of all these keywords when no body is provided but does not share their syntax definition and does not support the with variant). Let can indeed be used to define a local (to a section) definition or theorem. It does not seem to support the with variant either, so should be really close to Definition.

I think I'll seperate SubClass from Example and Definition. Are Example and Definition completely equivalent?

Yes

[jfehrle]

Re: first part of #11423 (comment)

The section "The Vernacular" seems to me a logical place to introduce the major top-level features of the valid inputs to Coq--some of which are semantic and/or generated by code rather than done in the grammar (and BTW, not easy to fake in a context-free grammar). Specifically, mention that there are commands and tactics, starting with upper/lower case letters. Tactics are only valid when you're in a proof mode (leaving further detail to other chapters as you suggested). Also mention that commands can have attributes (linking to details on these elsewhere). And mention the existence of sections, which open and close like balanced parentheses. This is just to provide a grammatical overview of a few things to replace the useless grammar that's currently in this section.

Does this make sense? (And if not described here, then where?)

Are there any other general significant non-grammar features that would fit in here?

EDIT: I see we already covered much of this in #11423 (comment).

[jfehrle]

Re: Local/Global and #[local], #[polymorphic]

How do you get the list of all attributes and which commands/tactics they apply to? Currently it looks like you have to read lots of code to do so. That's not going to be easy to track or get right. Perhaps we could encourage someone to look at handling this better? At least file a PR?

If I create a directive for attributes, it would look like this, except it would say "Attribute":

What about indexing? AFAIK the number of attributes is small and doesn't merit its own special index. Perhaps it could show up in the full index. (And remember we discussed indexing tactical quite some time ago without resolution--the PR is still open.)

Local and #[local] would be separate entries. I'd rather not create an "attrv" just to handle Local, Global, Monomorphic and Polymorphic if it's not necessary.

EDIT: Are attributes meant to apply to tactics? If so, I don't think there's a way to specify them for Ltac/Ltac2. If that's right, we should open a PR.

Also, the grammar for attributes allows complex nesting, e.g. #[ foo (bar, zap (sis (boom (bah)))) ]. Is this really needed? Maybe needlessly complex?

[jfehrle]

What do you think about changing the grammar so that all commands syntactically accept attributes? These commands are the exceptions. Right now "Local Quit." gives a syntax error whereas "Local Proof" gives a semantic error. Simpler to have it completely consistent and simpler to document accurately).

vernac_toplevel: [
| "Drop" "."
| "Quit" "."
| "BackTo" num "."
| "Show" "Goal" num "at" num "."
| "Show" "Proof" "Diffs" OPT "removed" "."
| vernac_control
]

vernac_control: [
| "Time" vernac_control
| "Redirect" string vernac_control
| "Timeout" num vernac_control
| "Fail" vernac_control
| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) vernac
]

[jfehrle]

Also vernac_control (shown above) permits a variety of curious things like "Time Time reflexivity." Also it appears that the vernac must be a tactic. Maybe we could tighten this up a bit?

[Zimmi48]

Responding to #11423 (comment):

Does this make sense?

It does, thanks!

How do you get the list of all attributes and which commands/tactics they apply to? Currently it looks like you have to read lots of code to do so. That's not going to be easy to track or get right. Perhaps we could encourage someone to look at handling this better?

I don't know and maybe @SkySkimmer can answer this.

In any case, attributes are just like options and flags. They are not part of the grammar, they just have a generic mechanism to parse them. If we must track them manually to start with (like we do for warning, error messages, flags and options) so be it.

If I create a directive for attributes, it would look like this, except it would say "Attribute":

No, not like this! The attribute is just local here. The #[ ] syntax is just there to list attributes, but certainly not part of the attribute itself. You can list multiple attributes within a single #[ ].

the number of attributes is small and doesn't merit its own special index

It is bound to grow, and it definitely deserves its own index. The whole point is to replace all the ad hoc flags that we have for a number of commands. A number of flags or options would also deserve to get a corresponding attribute to be set locally.

remember we discussed indexing tactical quite some time ago without resolution--the PR is still open

Just because we couldn't agree on what a tactical is.

Local and #[local] would be separate entries. I'd rather not create an "attrv" just to handle Local, Global, Monomorphic and Polymorphic if it's not necessary.

Local, Polymorphic, etc are not attributes. Attributes are a generic mechanism supporting such modifiers without actually having to extend the syntax anymore.

Are attributes meant to apply to tactics?

Tactics do already support attributes. You can in fact add #[] in front of any command or tactic. But no specific attribute can be applied to a tactic as of today.

Also, the grammar for attributes allows complex nesting

This is a very simple grammar whose purpose is to capture whatever attribute we may want to define in the future. Why would we put an arbitrary bound to the level of nesting?

What do you think about changing the grammar so that all commands syntactically accept attributes? These commands are the exceptions. Right now "Local Quit." gives a syntax error whereas "Local Proof" gives a semantic error. Simpler to have it completely consistent and simpler to document accurately).

Once again, Local is not an attribute. But similarly you cannot put a #[] in front of a Fail. This is intended and should be kept that way. Drop, Quit, BackTo, Show Goal are internal commands that allow a UI to communicate with Coq. Not meant to be used by a user. Vernac controls such as Time, Redirect, Timeout, Fail are special because their order matters.

Also, a bit off topic, the classifications in the index should be clearer. For example, "tacn" should be "tactic", ...

Sure, feel free to improve this in another PR.

[SkySkimmer]

Local, Polymorphic, etc are not attributes.

They are parsed as attributes.

[Zimmi48]

From a user's perspective, attributes are what one finds within #[ ]. Local, Polymorphic, Program are interpreted exactly the same as #[ local ], #[ polymorphic ], #[ program ] and I guess this is what you mean by "they are parsed as attributes". Nevertheless, they are not parsed by the attribute nonterminal.

[jfehrle]

Let's not get hung up the semantics of "attribute". I doubt the user cares to make a sharp distinction between the syntax #[ local ] and Local. They just want the command to be local. I think both need to be documented for now. I planned to refer to the latter as "legacy attributes" to provide some distinction.

It is bound to grow, and it definitely deserves its own index. The whole point is to replace all the ad hoc flags that we have for a number of commands. A number of flags or options would also deserve to get a corresponding attribute to be set locally.

It's trivial to add or remove the index. I don't see a lot of value when I only count 7 current attributes. The attributes accepted by any command are quite specific to each command. Why would the user want to look up "polymorphic" by itself? The attribute description won't say what commands it can be used with. But as we discussed, each command will list the attributes it supports, so if you see #[ universes(polymorphic) ] foo you can find a hyperlink for polymorphic under foo.

This is a very simple grammar whose purpose is to capture whatever attribute we may want to define in the future. Why would we put an arbitrary bound to the level of nesting?

It's not so simple. What's the difference between #[ foo ] #[ bar ], #[ foo, bar ] and #[ foo (bar) ]? Do we need to explain that? I expected attributes would just be present or absent. Or are they tree-structured? Why doesn't attr_value have an = for both productions? How about #[ foo (bar, zap (sis (boom (bah)))) ] - the grammar seems needlessly complex.

Also note that every command accepting an attribute will need to refer back to the section giving the general syntax for attribues #[ attribute ] because that's gonna be obvious without it.

But similarly you cannot put a #[] in front of a Fail. This is intended and should be kept that way. Drop, Quit, BackTo, Show Goal are internal commands that allow a UI to communicate with Coq. Not meant to be used by a user. Vernac controls such as Time, Redirect, Timeout, Fail are special because their order matters.

But why? What could be simpler than saying that all commands can have attributes instead of only a subset? Consistency is simpler to explain and maintain.

Your thoughts?

[jfehrle]

Also, I think there is another challenge: I think "Local" has slightly different meanings for different commands. If so, it's not going to be easy/possible to write up "Local" in one place.

[Zimmi48]

What's the difference between #[ foo ] #[ bar ], #[ foo, bar ] and #[ foo (bar) ]?

There's no difference between #[ foo ] #[ bar ] and #[ foo, bar ]. I don't know if we want to keep both. I guess it doesn't hurt so much. #[ foo(bar) ] is different: bar is a sub-attribute of foo.

I expected attributes would just be present or absent.

Sometimes they take values.

Or are they tree-structured?

Well, yes.

Why doesn't attr_value have an = for both productions?

= is for string values, meaning you can put any string on the right. On the other hand, attributes and sub-attributes must be defined.

How about #[ foo (bar, zap (sis (boom (bah)))) ]

This example is only theoretical since these attributes do not exist. Note that it is not the user who can decide to nest attributes, but only the attribute designer. E.g. universes can take sub-attribute polymorphic. But you cannot use the sub-attribute polymorphic inside deprecated, which expects only note and / or since.

the grammar seems needlessly complex

When I see your screenshot, I find it pretty simple, and I doubt that you could simplify it while still supporting whatever attributes already exist.

Also note that every command accepting an attribute will need to refer back to the section giving the general syntax for attribues #[ attribute ] because that's gonna be obvious without it.

I am not sure I understand this sentence, but isn't it exactly the same for flags and options?

What could be simpler than saying that all commands can have attributes instead of only a subset? Consistency is simpler to explain and maintain.

Do not consider these internal / toplevel commands Drop, Quit, etc. as commands. I wouldn't mind documenting them without the .. cmd:: directive if you think it would clarify things. @gares even suggested that we could change their syntax to something more like OCaml's #use if it helps to clarify that they should not be confused with normal commands.

Regarding Time, Redirect, ..., they should not be listed as commands either. They should appear in the grammar. They could be described in the same section as attributes if you wish.

[Zimmi48]

Also, I think there is another challenge: I think "Local" has slightly different meanings for different commands. If so, it's not going to be easy/possible to write up "Local" in one place.

This is unfortunate, we have no choice but to document the Local / Global modifiers as having various semantics depending on the command. This is actually already done as of today: https://coq.github.io/doc/master/refman/proof-engine/vernacular-commands.html#coq:cmd.local

[jfehrle]

Do not consider these internal / toplevel commands Drop, Quit, etc. as commands. I wouldn't mind documenting them without the .. cmd:: directive if you think it would clarify things. @gares even suggested that we could change their syntax to something more like OCaml's #use if it helps to clarify that they should not be confused with normal commands.

I certainly don't plan to do anything with these in this PR. But it's overkill to invent a new category of non-commands in the documentation. It just makes the doc more convoluted and confusing to users. It should be sufficient to document them as commands and to mention their special differences in the associated text for each. I expect users will think of them as commands no matter what we call them.

Regarding Time, Redirect, ..., they should not be listed as commands either. They should appear in the grammar. They could be described in the same section as attributes if you wish.

I see this the same as Drop. At the moment I have

While I need to add some more words relating ltac_expr and tactics, this is the logical place where Time et. al. would go in the grammar. I think it's not important enough to put here; documenting them as commands with some explanation should be sufficient. Users will think of them as commands no matter what we write.

[jfehrle]

Updated. Please take a look.

[Zimmi48]

I don't see a definition anywhere in the doc for universes(template) or universes(notemplate).

They are documented here: https://coq.github.io/doc/master/refman/language/cic.html#coq:flag.auto-template-polymorphism

This confirms IMHO the importance of providing an index for attributes. But this can come later on.

[Zimmi48]

@jfehrle Rather than trying to explain exactly what I wanted you to do for the inductive type introduction, I've pushed a commit doing the changes myself. Let me know if you are OK with that. Afterwards, the PR will need some squashing and we can merge.

[jfehrle]

Although the wording is repeated in a couple places, I prefer the original because it's one less hyperlink to get to the info you need. What do you think?

[Zimmi48]

We can go back to the original wording, but then the list of supported attributes should be kept.

[jfehrle]

Updated. Your changes look good, they read pretty well. Nonetheless, I thought some of the wording and details could be improved. Please take a look. I plan to squash after I hear back from you.

[Zimmi48]

Thanks, I've only noticed this one small issue.

[jfehrle]

Also changed the first paragraph under "cmd:: Inductive" to:

This command defines one or more
inductive types and its constructors. Coq generates destructors
depending on the universe that the inductive type :n:`@ident` (inside :n:`@ident_decl`) belongs to.

[jfehrle]

Squashed and marked ready for review.
I will update "Extensions of Gallina" next.

[Zimmi48]

What about simply "depending on the universe that the inductive type belongs to"?

[Zimmi48]

Similar to the question you raised in the Gallina chapter, this should either read "This commands supports the same attributes as the Inductive command" or it should be fixed to list the actual full list of attributes that this command supports.

[jfehrle]

I listed all the attributes. I have the same text for these commands:

finite_token: [
| "Inductive"
| "CoInductive"
| "Variant"
| "Record"
| "Structure"
| "Class"
]

It may be tedious to get all the attributes right and correct in the doc. Eventually we should come up with a semi-automatic way to extract the relevant attributes for each command. Probably means creating some common code to check attributes.

[Zimmi48]

Indeed, some future work in sight!

[Zimmi48]

Note that the error in the refman is in master, not in this PR.

[Zimmi48]

Given that this PR has been pretty much already reviewed, I announce my intention of merging it on Friday if no more comments by then.

[Zimmi48]

The fix has been merged in master.

[Zimmi48]

@jfehrle Could you fix the PR according to the last few comments I made before I merge this?

[jfehrle]

Updated, addressed your comments in #11423 (comment).

[jfehrle]

Thanks for your help!

[jfehrle]

What does it mean to be a "simple sort"? Is that different from @sort? If so, that should be defined--I can do that in the other PR. And :n:`sort` should be :n:`@sort` (?)

[Zimmi48]

It's just a sort. I think it is written a simple sort as opposed to a complex type.