Formal grammar (comments)

[benjub]

Comments should not nest, but the corresponding production rule in Appendix E reads:
_COMMENT ::= '$(' (_WHITECHAR+ (PRINTABLE-SEQUENCE - '$)')* _WHITECHAR+ '$)' _WHITECHAR

which allows for instance $( $( $) as a single comment (whereas metamath.c returns an error). A rule forbidding nesting would be:
_COMMENT ::= '$(' (_WHITECHAR+ (PRINTABLE-SEQUENCE - ('$(' | '$)')))* _WHITECHAR+ '$)' _WHITECHAR

That being said, the above fix is in order to conform to metamath.c. I wouldn't be opposed, if it makes the grammar simpler, to modify the program instead.

[david-a-wheeler]

Should we mandate that tools detect the $( ... $( ... case? I suspect many validators don't check for that.

[benjub]

Should we mandate that tools detect the $( ... $( ... case? I suspect many validators don't check for that.

I do not know if we should require it (for instance, mmverify.py does not check it, and is in accordance with the grammar rule currently in Appendix E). But this is a separate question from the above (which is about conformance of App. E with metamath.c).