makarius at sketis.net
Mon Sep 2 11:18:12 CEST 2013
On Sat, 31 Aug 2013, Lawrence Paulson wrote:
> It doesn't always work in the panel either. Some lurking bugs maybe.
Can you be more specific? The word "bug" has no meaning at all.
The sledgehammer panel has had only 1-2 rounds of refinements so far, and
more precise observations by testers on this mailing list will be required
to make it work smoothly for the coming release.
> I'm not sure what you are allowed to do while sh is running.
You should be allowed to do anything you like -- it is fully asynchronous
and stateless. In the worst case the system will cancel some sledgehammer
request when you edit the command span that it is attached to. (There is
a fine point here, since the white space after a command belongs to it, so
editing that will remove the sledgehammer query operation as well.)
Problems that might be still there are most likely due to propagation of
interrupts in the huge stack of tools and system layers we have piled up.
So one needs to watch closely the status of "top" (or "top -o cpu" on Mac
OS X), especially for E Prover processes (e-1.8 from Isabelle/2b5580da3874
might have made this warning obsolete).
More information about the isabelle-dev