fleche: fix terminator tokens

[artagnon]

Add "end", and remove "..." and BULLET.

[Alizter]

Why remove ... and bullet?

[artagnon]

Try T2048.v on master and this branch. The error recovery codepath is broken with ... and bullet.

[Alizter]

@ejgallego I would like to understand the role of terminator tokens. As it stands, my assumptions are anything we can consider terminating a Coq "sentence". This is why the removal of such tokens doesn't make sense to me. However, if the role of these tokens is otherwise, we should make that clear in the code.

[artagnon]

The code is clear: we're just matching against the next token on Gramlib.Stream: BULLET isn't a terminator token because of |-, and I assume ... isn't different from three consecutive . s; I've never seen a ..., so I can't be sure.

[ejgallego]

First, I see 3 quite different kind of changes in this PR, that makes review pretty hard, please submit one PR for each change.

The parsing recovery heuristic is just a heuristic, however I'm unsure I understand the problem here, in particular why to remove ..., can we have a self-contained test-case?

[ejgallego]

Actually seeing your comment about |- , I think you have been bitten by a different bug, which is Coq parser getting broken due to coq/coq#12575

If you have coq-lsp loading in a file ssreflect, and then trying to parse a different file, you'll get plenty of errors.

Can you confirm the weird stuff happens after you restart the server with just one file open?

[artagnon]

I've re-added ..., but BULLET is problematic on T2048.v: I get syntax errors near |-.

[ejgallego]

I've re-added ..., but BULLET is problematic on T2048.v: I get syntax errors near |-.

The file should check without errors, are you sure it is not the problem I mentioned above?

[artagnon]

Yeah, it seems flaky; seemed to work better with my patch at the time of writing.

[ejgallego]

I'm afraid the issue that @artagnon has seen is orthogonal to this patch.

Files failing to parse properly is due to some yet unsolved bug with coq-lsp or Coq management of the parsing state.

Tok.BULLET is a valid (and worthwhile) parsing recovery point and should not be removed from the heuristic.

[ejgallego]

In particular @artagnon parsing will go mad when coq-lsp loads the ssreflect plugin in some other buffer, but the bug is general.

[ejgallego]

Yeah, it seems flaky; seemed to work better with my patch at the time of writing.

Restarting coq-lsp usually solves this if you don't load the ssreflect plugin (or any other syntax heavy plugin) first. So it seems that the problem is solved with the patch, but that codepath is never reached in the first place.

[ejgallego]

That bug is actually driving me crazy, I can reproduce reliably by loading ex0.v and then RTrigo.

Maybe Print Grammar will show what the problem is?

[artagnon]

Does this patch help?

[artagnon]

Nack, it doesn't. I just checked.

[ejgallego]

See coq/coq#12575 (comment) , somehow sometimes keywords disappear and that's what causes the problem, in particular you say that |- not being a keyword, the mess was giant.