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:
"(!!P. P::bool) ==> PROP P"
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and