[notations] Warn about incompatible prefixes

[proux01]

Add a warning for notations with incompatible common prefixes, for instance

Reserved Notation "#0 #1" (at level 30).
Reserved Notation "#0 #1 #2" (at level 40).
(* Warning: Notations "#0 #1" defined at level 30 and "#0 #1 #2" defined at level 40 have incompatible prefixes. One of them will likely not work. [prefix-incompatible-level,parsing,default] *)

Reserved Notation "#20 #21 x #3 y" (x at level 30, at level 50).
Reserved Notation "#20 #21 x #34" (x at level 40, at level 50).
(* Warning: Notations "#20 #21 _ #3 _" defined at level 50 with arguments constr at level 30 and "#20 #21 _ #34" defined at level 50 with arguments constr at level 40 have incompatible prefixes. One of them will likely not work. [prefix-incompatible-level,parsing,default] *)

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

• Opened overlay pull requests.

[proux01]

@herbelin this is the first step toward the at existing level notation option we already discussed and that I'd like to add in a further PR.

[SkySkimmer]

Maybe the warning should explain what the consequences of incompatible prefixes are (I don't know myself)

[proux01]

Indeed, done, as well as the documentation.

[jfehrle]

wording and other suggestions

[jfehrle]

@SkySkimmer > Maybe the warning should explain what the consequences of incompatible prefixes are (I don't know myself)

IIUC the parser would only recognize one of the notations (and report syntax errors on the others), depending on the order in which the parser processes the rules defined for each notation (first one wins). Our parser really doesn't do lookahead--it looks at only the next symbol to make a parsing decision. Once the first token of a rule is accepted, the parser is unable to switch to a different rule. Not like LALR(k) parsers such as yacc and bison. (There is a hard coded exception to this behavior for command names.)

[SkySkimmer]

@jfehrle please don't guess

There is a hard coded exception to this behavior for command names

is certainly not true so I don't trust the rest of your post.

[proux01]

@coqbot run full ci

[jfehrle]

@SkySkimmer The exceptional code is Grammar.parser_of_token_list, which does multisymbol lookahead among prefixes containing only terminal symbols. Most relevant to command names, option names and tactic names and not used for most other nonterminals.

[herbelin]

Going to merge, after rebase and clean CI.

[proux01]

@herbelin rebased, CI green

[herbelin]

@coqbot merge now

[herbelin]

@coqbot merge now