jrh13 / hol-light

The HOL Light theorem prover
Other
435 stars 78 forks source link

Add `use_file_raise_failure` flag to control raising Failure #83

Closed aqjune closed 1 year ago

aqjune commented 1 year ago

This patch adds a flag that sets whether use_file must raise Failure if loading the file did not succeed. If set to true, this helps (nested) loading of files fail early. However, propagation of the failure will cause Toplevel to forget bindings ('let .. = ..;;') that have been made before the erroneous statement in the file. This leads to an inconsistent state between variable and defined constants in HOL Light.

jrh13 commented 1 year ago

I like the idea of making this controllable, since both behaviors can be useful.