Just to follow up my previous post, the first problem also appears under mosml. The behaviour would result if the Interrupt exception were being caught during the proof step and not propagated. The tactic I am using is SIMP. Grepping the HOL sources reveals many places where an arbitrary exception is caught and not propagated. This would prevent Interrupts from being propagated. There has also been some effort to ensure that general exceptions are not caught (e.g. HOL_ERR is caught rather than a general exception).

Given that there are many potential places in HOL where Interrupt could be caught and not thrown, is there any reason to believe that the HOL code is not wrong in these places?

The second problem, where polyml loses the ability to call system functions, remains.

T

2008/5/12 Tom Ridge thomas.ridge@cl.cam.ac.uk:

Dear All,

I have been using HOL with Scott Owens' new port to polyml. To interrupt a proof that takes a long time, I hit ctrl-c. I get the polyml #> prompt straightaway. However, if I type f (raise an exception) then nothing happens for a long while. This time seems to increase the longer the interrupted proof step has been running.

Eventually the system seems to return, but it is not clear whether an exception has been raised or not. Certainly the goalstate is now different. On the other hand, the goal state should not result if the proof step completed (but this is likely some erroneous behaviour at the HOL level).

There is another problem though. The HOL/polyml top-level is usable for cut-and-pasting. However, I can't invoke any commands that involve system calls, otherwise I get a "Function system failed" message (from libpolyml/process_env.cpp). This is a problem because the xemacs sml mode writes commands to a temporary file and "use"s them into the top-level.

Does anyone have any ideas what might be causing these two problems?

Thanks

Tom