Syntax error in startup commands for 8.9

[hendriktews]

When I start Coq 8.9, I see in *coq*:

Welcome to Coq 8.9.1 (June 2019)

<prompt>Coq < 1 || 0 < </prompt>Add Search Blacklist "Private_" "_subproof". 

<prompt>Coq < 2 || 0 < </prompt>Set Suggest Proof Using. 

<prompt>Coq < 3 || 0 < </prompt>.
Toplevel input, characters 26-27:
> .
> ^
Error: Syntax error: illegal begin of toplevel:vernac_toplevel.

<prompt>Coq < 3 || 0 < </prompt>Set Printing Depth 50 . 

I believe the syntax error comes from this line: https://github.com/ProofGeneral/PG/blob/f0f0476d07401aba2cf428a71f7ee960cd1b3154/coq/coq.el#L1823 which adds coq-diffs to proof-assistant-settings, which eventually adds an empty string, to which proof-shell-invisible-command adds a point. @erikmd have you checked this code with 8.9? For how long do we want to support 8.9?

[Matafou]

8.9 is only 2 years old. Let us not drop it until one or two years from now imho.

[erikmd]

Indeed, we definitely want to support 8.9; and while there's already some logic to ensure the Set Diffs are only used for 8.10+, it appears to be incomplete indeed… thanks @hendriktews for noticing this! do you think it is easy to avoid sending this empty string? (I didn't take a look again yet)

[hendriktews]

Instead of filtering proof-assistant-settings for empty commands, I would suggest to not add coq-diffs to proof-assistant-settings for Coq < 8.10.