Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.



When inserting my previous example 6 times I get no feedback in the sixth version. (The first four loop the fifth yields feedback the sixth doesn't. I have two cores with four threads, I've set parallel proofs to two.)

I'd tag a single looping thread as undesirable and would understand tagging thins with "meaningless" words as artistic freedom.

I just reported this to make sure it's on such a list and maybe increase it's relative priority a little.

Best
    Benedikt


Am 22.04.14 13:53, schrieb Makarius:
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).


    Makarius





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