Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.
On Tue, 22 Apr 2014, bnord wrote:
When inserting a new goal (have ...) into a proof, proof methods
belonging to later goals seem to be applied wrongly sometimes causing
them to loop and make my PC noisy after a while. ;)
The "show" already produces a syntax error but the later "by" is applied
anyhow yet to the wrong goal causing it to loop.
A student of mine is highly skilled in producing such situations in many
theorems simultaneously causing the editor to become very unresponsive.
IIRC, you have reported massive waste of CPU cycles and unresponsiveness
This can certainly happen, and the system could be smarter in the
scheduling of tasks. Such improvements are on the TODO list of
improvements (neither "issues" nor "bugs") for several years. The reason
why it is still not done, is lack of priority: I simply don't see really
bad effects so often.
Maybe it is just a problem of adjusting Isabelle multi-threading
parameters to your hardware. The above description sounds like you have
either very few cores (only 2) or a lot of virtual cores (due to
This archive was generated by a fusion of
Pipermail (Mailman edition) and