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



On Wed, 23 Apr 2014, Thomas Sewell wrote:

I'd just like to add that this problem can be compounded by some other issues, such as one we mentioned before where a diverging "blast" can slow down jEdit. On rare occasions I've had to go hunting for blasts and fastforces in the future part of my theory just to get enough CPU back to work on the problem I have.

That is unrealated to thread scheduling. It is merely the oldest trick that tools can play on the front-end to bomb it, by emitting vast amounts of "potentially useful" tracing information.

That is already resolved for the coming release, see also
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-December/msg00138.html
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-December/004919.html

A prover that is running efficiently on more and more cores poses extra challenges on the front-end. But even with single-threaded Proof General, the danger had been there all the time. When I discovered an easy workaround with "nice" on Unix in 2006, it was too late: the single-core era had already ended and that crude process priority trick was useless, except on my last 1-core laptop.


	Makarius




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