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

HOL_ERR source locations #1342

Closed digama0 closed 1 week ago

digama0 commented 1 week ago

This was mentioned as a TODO in Feedback.sml, and I need it for some error reporting work I'm doing. Adds a source_location field to error_record, and migrates most uses of the HOL_ERR constructor to either use incomplete pattern matching or mk_HOL_ERR instead.

mn200 commented 1 week ago

Looks good! Can merge when the CI is also good.

binghe commented 1 week ago

Looks good! Can merge when the CI is also good.

This time only OT build was successful:)

mn200 commented 1 week ago

Awesome: thanks!