Hi Michael, with recent commits in HOL’s Git master, I found that I cannot easily interrupt the proof searching underly PROVE_TAC (or maybe also METIS_TAC). In another words, if I didn’t provide enough lemmas when calling PROVE_TAC [] and have caused the proof searching goes into infinite loops, I will *not* be able to interrupt HOL any more, by "Meta-H Ctrl-C” in Emacs, unless I do it early (still after calling PROVE_TAC but not that late somehow). Then I have to kill HOL process in Emacs, then restart it, replay my proof scripts so far.
Do you have any clue on the root causes? (I also want to know if other HOL users met the same issues, by CC to hol-info mailing list) Regards, Chun
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
