Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add test for nested comments. #84

Merged
merged 1 commit into from
May 18, 2022

Conversation

jkingdon
Copy link
Collaborator

As discussed on the mailing list.

@benjub
Copy link
Collaborator

benjub commented May 18, 2022

So I guess this settles the alternative given in metamath/metamath-book#233.
I'll modify mmverify.py to raise on $( $( $) (only one line to add). As for the EBNF grammar with the proposal I described there, I don't remember if we edit metamath.tex or leave it that way and edit the errata.md (or edit both).

@digama0 digama0 merged commit f7a3c72 into metamath:master May 18, 2022
@jkingdon jkingdon deleted the nested-comment-test branch May 19, 2022 02:01
@jkingdon
Copy link
Collaborator Author

So I guess this settles the alternative given in metamath/metamath-book#233. I'll modify mmverify.py to raise on $( $( $) (only one line to add). As for the EBNF grammar with the proposal I described there, I don't remember if we edit metamath.tex or leave it that way and edit the errata.md (or edit both).

To the extent that I was thinking about this at any level deeper than asking what metamath has always (for some value of always) done, I was just thinking that $( inside a comment is usually a mistake. But if people want to change the implementation/test to match the spec in the book, well we could discuss that although I guess the current implementation seems like the practical choice to me.

@tirix
Copy link

tirix commented May 19, 2022

BTW @jkingdon, which mailing list post were you referring to initially?
I see in this post from Mario :

Regular comments, parsed with the standard metamath lexer (i.e. whitespace separated everything) have the form '$(' token* '$)' where no token contains an embedded occurrence of '$)' or '$('.

Is that what you are referring to?

@jkingdon
Copy link
Collaborator Author

BTW @jkingdon, which mailing list post were you referring to initially?

I was thinking of https://groups.google.com/g/metamath/c/DDvCuVRev0M/m/fCo-hzvCAwAJ which is I think the message right above the one you linked to, which is almost written in test case format in the sense that it says in that "$( $( $)" returns an error in metamath.c.

@benjub
Copy link
Collaborator

benjub commented May 19, 2022 via email

@benjub
Copy link
Collaborator

benjub commented May 19, 2022

Fixed mmverify.py to be closer to metamath.c's behavior (see david-a-wheeler/mmverify.py#14). Now, my two questions remain:

  • Do you agree with my proposal to modify Appendix E of the Metamath book as proposed in Formal grammar (comments) metamath-book#233 ? Should I modify errata.md ? metamath.tex ? both ?
  • Do you agree that it is not necessary to go beyond in Appendix E (that is, we live with the fact that $( a$( $) is accepted by the grammar), and to consider the extra check done by metamath.c (and now mmverify.py as well) as an indication to the user that he probably forgot a space ?

@digama0
Copy link
Member

digama0 commented May 19, 2022

I think that the rule should be the one implemented in metamath.c: a comment must not contain a token that has a $( or $) substring.

@benjub
Copy link
Collaborator

benjub commented May 19, 2022

I think that the rule should be the one implemented in metamath.c: a comment must not contain a token that has a $( or $) substring.

Ahh, you drive a hard bargain ! But fair enough. What about:

_COMMENT ::= '$(' _WHITECHAR _COMMENT-CONTENT _WHITECHAR '$)' _WHITECHAR
_COMMENT-CONTENT ::= (_WHITECHAR | _PRINTABLE-CHARACTER)* -
      ((_WHITECHAR | _PRINTABLE-CHARACTER)* ('$(' | '$)') (_WHITECHAR | _PRINTABLE-CHARACTER)*)

This looks a bit complex. Or you have another suggestion ?
(Rk: if the file ends with a comment, there could be no trailing whitechar... These border cases are always annoying, but maybe there is a more elegant way to deal with them?)

Edit: or maybe,

_COMMENT ::= '$(' (_WHITECHAR+ PRINTABLE-SEQUENCE* _WHITECHAR+ '$)' _WHITECHAR
PRINTABLE-SEQUENCE ::= _PRINTABLE-CHARACTER+ - (_PRINTABLE-CHARACTER* ('$(' | '$)') _PRINTABLE-CHARACTER)*

(instead of the current production rule for PRINTABLE-SEQUENCE)

@david-a-wheeler
Copy link
Member

Who knew there was a price for formal exactness :-) ?

@david-a-wheeler
Copy link
Member

If you want a change to the spec in the book, that needs to be here:
https://github.com/metamath/metamath-book

@benjub
Copy link
Collaborator

benjub commented May 20, 2022

If you want a change to the spec in the book, that needs to be here: https://github.com/metamath/metamath-book

@david-a-wheeler : As I wrote above, I will do a PR, but as I asked above, I would like to know before if I should modify errata.md or metamath.tex or both ? (I'm going to move the conversation to: metamath/metamath-book#233, or open another issue.)

@david-a-wheeler
Copy link
Member

@benjub - at a *minimum, do errata.md. Bonus points if you also edit metamath.tex, but that should probably be a separate PR.

No one expected Norm to pass so soon, so book update plans are, well, unknown. Thankfully the licensing means that we can do an update without licensing problems.

It might be good to have a longer discussion how when/how to update the book.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants