Re: [isabelle] "(!!P. P::bool) ==> PROP P" with auto methods hangs PIDE



On Fri, 13 Dec 2013, Gottfried Barrow wrote:

I do this with "Auto Methods" checked in the PIDE options:

theorem
 "(!!P. P::bool) ==> PROP P"
oops

With "Auto Methods" unchecked, I can use "try0" and they go into overdrive, but they slowly shut down over about 10 seconds.

"Auto Methods" is generally a bit fragile: it tends to suck up a lot of CPU resources for various reasons, that are not fully sorted out yet. It was a somewhat dormant feature over a few years, but now shows up in the PIDE interaction model, with slightly different side-conditions.


The particular problem above is "blast" failing repeatedly in a rather noise way. You can try something like this:

 theorem "(!!P. P::bool) ==> PROP P" by blast

e.g. with "isabelle tty" on the Terminal.


For the *next* release, we should avoid such noise and denial of service on the front-end. Even terminal emulators occasionally get into a pitch with arbitrary volume of output.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.