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

Print errors from parsing in a meaningful way #86

Open
SimonGuilloud opened this issue Oct 27, 2022 · 4 comments
Open

Print errors from parsing in a meaningful way #86

SimonGuilloud opened this issue Oct 27, 2022 · 4 comments

Comments

@SimonGuilloud
Copy link
Collaborator

Error when parsing a statement or formula look like "Caused by: lisa.utils.Parser$ParserException: Unexpected input: )
", lost in the stack trace.
We should instead print meaningfull error messages before making the program fail, indicating the parsing of which formula caused the crash, and ideally, if it is in a proof, at which line

@cache-nez cache-nez self-assigned this Nov 1, 2022
@SimonGuilloud
Copy link
Collaborator Author

I'm working on an error reporting system. Key for the parser will be to throw a specific error right at the called function, not multiple levels bellow.

@cache-nez
Copy link
Contributor

Couple of comments for context:

  1. Whenever a program fails due to an uncaught exception, the exception type and message is displayed on top (followed by the stack trace). Hence the priority is to make the exception message include as much relevant information as possible (no need for separate prints).
  2. It is certainly useful to include the formula being parsed. However, it is difficult to add information beyond that, because the parser crashes once it cannot find a rule that matches the next token, and only provides this token along with error indication. So we can say that the parser couldn't parse this token in this formula [at this position -- to be added] but that's it.

@vkuncak
Copy link
Collaborator

vkuncak commented Nov 23, 2022

Sounds like a non-controversial step is to provide the position. Scallion should already have functionality for that.

@cache-nez
Copy link
Contributor

@vkuncak: working on it!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants