search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
630 stars 142 forks source link

Report error locations on unhandled exceptions #1306

Closed digama0 closed 2 months ago

digama0 commented 2 months ago

PolyML keeps track of the location of every exception (the position of the raise keyword), and this information is very useful for debugging, so let's show that. In VSCode it also enables the ability to click in the terminal to go directly to the error.

A few other locations had to be adjusted to use reraise to avoid clobbering the location information.

mn200 commented 2 months ago

Awesome! I didn't know PolyML's exception module was so rich.