[isabelle] "Stuck" (i.e. looping) prover issues
Since there is a thread going about various kinds of hanging, I would
like to ask about behavior that I have experienced (with Isabelle2014).
Basically the symptom is that the prover becomes unresponsive, though JEdit
does still respond. Often, the entire buffer becomes highlighted in pink,
and many times it is impossible to continue without exiting JEdit
(thereby exiting the prover) and restarting. While in the stuck state,
the prover (Poly process) exhibits constant CPU consumption. It does not
appear to be a thrashing issue because the disk traffic is low and CPU
I have only rarely seen this problem on my home system, which is a year-old
i5 processor with four cores (I am running Ubuntu 14.04 LTS) and 8GB RAM.
However, it occurs much more often on my office machine, which is a venerable
32-bit, one-core system with 2GB (also running Ubuntu 14.04 LTS).
In fact, it is pretty much impossible to use "try" on that machine because
it almost always results in a stuck prover. Once the situation has arisen,
attempting to delete the "try" from the JEdit buffer does not successfully
cancel the ongoing proof attempt.
I would be interested to know what I should be looking for in order to try
to solve this. When I noticed it this morning on my home system, it appeared
to be because there were several threads occupied by various proof attempts
(I think "blast") that did not terminate. In this particular case I was
able to recover by erasing the "by blast" lines, but when things are truly
stuck (especially on the one-core system) this does not help.
Another situation I have gotten into that produced similar symptoms is when
I inadvertently created recursive simplifier rules. However, I don't think
this is usually the issue.
My question is: is it supposed to be possible for prover threads to hang
around indefinitely (purple mark in right margin and proof method highlighted
in purple) without timing out in some reasonable period? If so, why,
and what should I look for to try to fix the problem? If not, then this would
seem to be an issue that should be looked into.
Thanks for the help.
- Gene Stark
This archive was generated by a fusion of
Pipermail (Mailman edition) and