search

jrh13 / hol-light

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

Recursively fail when loading a file with errors #61

Closed mpu closed 1 year ago

mpu commented 4 years ago

When a file is loaded with a standard loading function (loads, loadt, or needs) errors are merely flagged with a message on the terminal but the loading function itself does not fail. This means that if a.ml loads b.ml then c.ml, and b.ml has errors, c.ml will be loaded when HOL is most likely in a broken state. To avoid this behavior, this PR makes use_file itself fail when the loaded file has errors.

aqjune commented 1 year ago

I think this patch is helpful for pinpointing the failure point when loading some .ml file using loadt. If e.g., a.ml contains two loadt commands, this patch makes the first loadt immediately stop and not go through the second loadt.

aqjune commented 1 year ago

In theory this patch should not affect proofs that already succeed - may I ask whether my understanding is right?

mpu commented 1 year ago

I think this patch is helpful for pinpointing the failure point when loading some .ml file using loadt.

Yes that is the point.

In theory this patch should not affect proofs that already succeed - may I ask whether my understanding is right?

I believe so.

jrh13 commented 1 year ago

Actually, having used it for a bit, I'm no longer so convinced.

The problem is that I quite like being able to keep the parts of a load that worked before an exception. For example, if you have the following in a file:

let identifier_a = GSYM ADD_ASSOC;;

let identifier_b = fail();;

let identifier_c = ADD_ASSOC;;

and do loadt "...that file..." then you end up in a state where you even lose the binding of identifier_a. I would prefer to avoid that. Maybe one can still have the "fast fail" on first error recursively while not rolling back the binding state? But I'm not quite sure how.

aqjune commented 1 year ago

Another observed problem was that definition of constants were still there whereas bindings were rolled back, causing to (kind of) an inconsistent state. I opened this PR - https://github.com/jrh13/hol-light/pull/83 - to add a control flag for the failure.

mpu commented 1 year ago

It makes most sense in batch mode, maybe a bit less in an interactive setting.