search

epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Print errors from parsing in a meaningful way #86

Open SimonGuilloud opened 1 year ago

SimonGuilloud commented 1 year ago

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

SimonGuilloud commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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

cache-nez commented 1 year ago

@vkuncak: working on it!