Documentation needed for the output of "Print Custom Grammar"

[bcpierce00]

(1) Is there someplace where Coq users can read about how to interpret the output of the "Print Custom Grammar" command?

(2) Could we put (at least a pointer to) it in the reference manual?

[Zimmi48]

In 8.12, there is a bit of explanation in the description of Print Grammar: https://coq.github.io/doc/v8.12/refman/user-extensions/syntax-extensions.html#coq:cmd.print-grammar
Is that sufficient? If not, what is missing? And should we link to it from the description of Print Custom Grammar? (I guess we should.)

[bcpierce00]

Thank you -- this is already helpful, though I didn't understand this part (which I think is related to things I didn't understand when trying to figure it out for myself -- the precedence and associativity are easy to guess): "SELF represents the tactic_expr nonterminal at level 5 (the top level)."

A slightly larger example might be even more helpful. (Also, this might be a good opportunity for illustrating the way grammars have to be "hand factored" for the parser.)

[Zimmi48]

cc-ing @jfehrle who authored this explanation

[jfehrle]

@bcpierce00:

"SELF represents the tactic_expr nonterminal at level 5 (the top level)."

Indeed, this is incorrect.

• On the left-hand side of a production, SELF means the next level in the Print Grammar output.
• On the right-hand side of a production, SELF means the next level within LEFTA levels and the current level within RIGHTA levels.
• In the middle of a production, SELF means the top level

In the doc, ltac_expr at https://coq.github.io/doc/master/refman/proof-engine/ltac.html#syntax corresponds to tactic:tactic_expr. The grammar in the doc has been edited significantly edited for readability. https://github.com/coq/coq/blob/master/doc/tools/docgram/fullGrammar summarizes the grammar as it appears in the source code, in which tactic_exprN corresponds to tactic:tactic_expr level N and SELF/NEXT have been substituted.

fullGrammar is generated automatically. The grammar we're using to update the doc is generated by applying a grammar-editing script to fullGrammar and inserted into the doc files 95% automatically. We're confident the resulting grammar is quite accurate for users and, we believe, far easier to read. We're still in the process of updating all the syntax in the documentation. The release notes for 8.12 mention which chapters have been updated so far. Those who plan to modify the parser will want to refer to fullGrammar.

Using 3 different names for same nonterminal is less than ideal. Once all the syntax in the doc has been updated, we'll look at making them more consistent, such as by

• changing nonterminal names in the source code to match the documented grammar when it won't cause compatibility issues
• updating nonterminal names that appear in Coq output and/or
• providing documentation of how to map between them

A slightly larger example might be even more helpful.

I'll update the doc with explanation similar to what I said above. Given that, what would you want to see in an example?

(Also, this might be a good opportunity for illustrating the way grammars have to be "hand factored" for the parser.)

Let me see what we can do. It shouldn't be too hard to cover this specific point. We don't have much in the way of developer documentation--not sure if that should be in the reference manual or
a separate document. Perhaps we could explain what is likely the most common developer need: adding command and tactic syntax for plugins.

I'll update the doc. If you'd like to review the changes before they're merged, let me know and I'll notify you when we have something ready.