search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
336 stars 68 forks source link

Open quotes in comments triggers a parsing error #737

Closed YaZko closed 7 months ago

YaZko commented 7 months ago

It seems like an orphan quote insight of a comment is incorrectly handled at the moment. I.e. I expect the following to trigger no error nor warning, but it displays all of the file after the quote as a parsing error.

On 2.1.0+coq8.19.

Definition x := 9.

(* " *)

Lemma foo : x = 9.
reflexivity.
Qed.

Best, Yannick

YaZko commented 7 months ago

Actually I have just been informed that as much as I hate it, it seems to be Coq's expected behaviour! It's still a bit of an unpleasant interactive experience so VSCoq could maybe try to wiggle around it, but it's technically not its fault :)

coqc tmp\'.v
File "./tmp'.v", line 3, characters -2--2:
Warning: Not interpreting "*)" as the end of current non-terminated comment
because it occurs in a non-terminated string of the comment.
[comment-terminator-in-string,parsing,default]
File "./tmp'.v", line 8, characters -43-0:
Error: Syntax Error: Lexer: Unterminated string
rtetley commented 7 months ago

Ah cool ! I was about to test it out on other IDEs and see what happens there, but I believe that handling this would require parsing comments, and is related to: #728 Thanks for reporting !

rtetley commented 7 months ago

I'm closing this as it is not technically a vscoq issue.