On Fri, 27 Jun 2014, Peter Lammich wrote:
* If sledgehammer (both over panel and as command) is running, further
processing of the file is blocked/very slow. Thus, it is not possible
to run sledgehammer and, in parallel, continue exploration to find your
own proof. In PG, parallel sledgehammering works, and I used it
extensively. In Isabelle/jEdit I now think twice before I invoke
sledgehammer, because it just interrupts my workflow and I have to wait
for it to finish staring at the sledgehammer-window and doing nothing.
This sounds like some serious performance problem, and requires proper
reports on your hardware and system parameters.
In Isabelle2014 the Sledgehammer integration is in its third generation.
It is supposed to work without problems.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
