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 before.

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 hyperthreading).


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