abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
90 stars 18 forks source link

Missing line numbers in error messages #40

Open lambdacalculator opened 9 years ago

lambdacalculator commented 9 years ago

Using 2.0.3, I notice that a couple of error messages do not provide information on either the offending source file or line and character numbers:

There may be other error message (as I seem to recall) that also do not report source file/line numbers.

chaudhuri commented 9 years ago

Thanks for the report. Unfortunately Abella does not keep source positions in the AST currently. This has been on my list of things to add for a while. Let me take another stab at it.

Caveat: it may come after the impending 2.0.4 release.

lambdacalculator commented 9 years ago

But Abella does report line numbers and character ranges on other types of errors, such as syntax errors and typing errors.