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

Poor error message when a the proof end token is missing #1077

Open
Alidra opened this issue Apr 9, 2024 · 0 comments
Open

Poor error message when a the proof end token is missing #1077

Alidra opened this issue Apr 9, 2024 · 0 comments

Comments

@Alidra
Copy link
Member

Alidra commented Apr 9, 2024

When a proof is started with begin but end is missing at the end of the proof (whether the proof is completed or not), Both the Lambdapi command line and Lsp show the message Unexpected token: "". while it should be end missing.
For instance, with the following file

verbose 3;
constant symbol T : TYPE;
opaque symbol trivial : T → T → T → T
≔ begin

The command line check command produces :

Checking "somefile.lp" ...
verbose 3
somefile.lp:2:0-25
symbol T : TYPE
[somefile.lp:5:7] Unexpected token: "".

Moreover, in Vscode (and probably with Emacs too), the console doesn't show the log messages (despite console 3; at the beginning of the file) except the last one which is Unexpected token: "".

@Alidra Alidra self-assigned this Apr 9, 2024
@fblanqui fblanqui added lsp Issues related to Language Server Protocol parsing error message and removed lsp Issues related to Language Server Protocol labels Apr 11, 2024
@fblanqui fblanqui changed the title Erronous message when a the proof end token is missing Poor error message when a the proof end token is missing Apr 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants