Open clarksmr opened 2 years ago
Indeed pg is far from perfect at splitting a file into commands. This case is known #357. Along with at least those: #612, #592, #58. We definitely need to make things better int his particular case because it probably happens very often.
Environment: Mac, Emacs 27.2, Coq 8.13.2, PG 20220310.2253; also VS Code 1.65.2, VSCoq 0.3.6; Coq_Platform_2021.09.0; and the online Scratchpad jsCoq 0.15.0, Coq 8.15.0.
Steps to reproduce:
Expected behavior: The \<dot>\<rbrace> tokens should result in an error:
Error: Syntax Error: Lexer: Undefined token
.Actual behavior: The code is compiled without error.
Explanation: VSCode, CoqPlatform, the online Scratchpad, and coqc all exhibit the expected behavior and reject the code. Only PG accepts the code without error.
Examples:
Terminal transcript with coqc:
Screenshot with PG:
Related: #83 seemed to have the same root cause, but I'm opening a new issue because this isn't about Software Foundations, and that issue is a bit hard to find by searching for the error.