[isabelle-dev] sledgehammer

[Makarius]

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).


 	Makarius