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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and