Email Gateway (Aug 19 2022 at 13:00): Email Gateway (Aug 19 2022 at 13:00):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
I do this with "Auto Methods" checked in the PIDE options:
theorem
"(!!P. P::bool) ==> PROP P"
oops
The processes Isabelle2013-2.exe and poly.exe start taking close to 100%
of my CPU, and don't give up. The PIDE gets unresponsive, and I have to
terminate everthing.
With "Auto Methods" unchecked, I can use "try0" and they go into
overdrive, but they slowly shut down over about 10 seconds.
As a side note, I can run Sledgehammer, and the ATPs can be at over 96%
of the CPU, but the PIDE never gets unresponsive.
I attach a screen shot.
For anyone interested, here's what I use to look at "Trueprop", which is
shown in the screenshot:
notation Trueprop ("_\<Colon>\<^sub>T" [1000] 1000)
Forgetting about brackets, typing, and Trueprop can sometimes result in
me expending negative mental energy. Confused neurons, mucking about in
the grey matter, too many to count, connecting the most embarrassing of
logical dots.
Thanks,
GB
131213_for_all_bool_hangs_pide.png
Email Gateway (Aug 19 2022 at 13:02):From: Makarius <makarius@sketis.net>
"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
Email Gateway (Aug 19 2022 at 13:04):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 12/16/2013 10:25 AM, Makarius wrote:
The particular problem above is "blast" failing repeatedly in a rather
noise way....
I now have a practical example that causes the PIDE to go off and not
come back, which is because of auto, blast, and declare commands.
declare[[show_sorts=true]]
lemma "(!!f. !!a. f = (%a. a | f a) ==> (f a = a)) ==> False"
apply(auto)
oops
I haven't completely figured it out, but it seems
"declare[[show_sorts=true]]" puts it over the edge. With it "false",
Isabelle2013-2.exe will jump up to about 50% of the CPU, but recover.
With it "true", after "auto" runs long enough, the PIDE becomes
unresponsive, and it can't recover. It may not be particular to
"show_sorts".
Using "apply blast" creates a bunch of messages, but it still proves the
theorem, so it's the interaction between auto and blast.
I suppose it's just more of the same. I attach and include a theory with
variations that work or don't work.
...You can try something like this:
theorem "(!!P. P::bool) ==> PROP P" by blast
e.g. with "isabelle tty" on the Terminal.
I tried the theorem in tty mode. It goes into a loop after getting to 6:
"PROOF FAILED for depth 6". If you're telling me that blast will prove
"(!!P. P::bool) ==> PROP P", that would be important to know.
Regarding that other list, I use Sourcetree on Windows for github.com.
It's easy to install and use, and has way more features than the GitHub
Windows application. It allows me to keep from having to know much.
I do my part as an imaginary power-user, a logical cult-of-one, peering
out from the curtains of my compound, waiting for the NSA and that
ex-KGB agent, Vladimir Putin, to arrive at any moment.
Regards,
GB
(********************)
theory i131214a__isaU_Trueprop_False_meta_eq_auto_hangs_PIDE
imports Complex_Main
begin
declare[[show_sorts=true]]
declare[[show_brackets=true]]
declare[[show_question_marks=true]]
notation Trueprop ("_∷⇩T" [1000] 1000)
(*With "Auto Methods" off, auto goes off and doesn't come back, if it's
allowed
to run very long.*)
lemma "Trueprop False == (!!f. !!a. f = (%a. a | f a) ==> (f a = a))"
apply(rule equal_intr_rule)
(apply(auto))
oops
(*This direction with auto is the problem. I need to terminate it within
less
than about 5 seconds when I have "show_sorts=true".*)
lemma "(!!f. !!a. f = (%a. a | f a) ==> (f a = a)) ==> False"
(apply(auto))
oops
(No problem with blast to prove ==, instead of auto.)
lemma "Trueprop False == (!!f. !!a. f = (%a. a | f a) ==> (f a = a))"
apply(rule equal_intr_rule)
apply(blast)
apply(blast) (Failure messages here.)
done
(This direction with blast is okay, though there are failure messages.)
lemma "(!!f. !!a. f = (%a. a | f a) ==> (f a = a)) ==> False"
apply(blast) (Failure messages here.)
done
(The other direction with auto is okay.)
lemma "False ==> (!!f. !!a. f = (%a. a | f a) ==> (f a = a))"
apply(auto)
done
end
i131214a__isaU_Trueprop_False_meta_eq_auto_hangs_PIDE.thy
Last updated: Apr 25 2024 at 01:08 UTC