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
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.
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
IIRC, you have reported massive waste of CPU cycles and
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