On Fri, 27 Jun 2014, Makarius wrote:
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.
This appears to be again one of these "problems are kept secret" situation
that has made Isabelle2013-1 a failure, and left many questions after
Isabelle2013-2 if the Isabelle release process still works.
It is important to note that I don't have any first-hand access to power
users who do serious testing. I do depend on proper problem reports,
beyond "there is a bug", "it does not work". Otherwise we need to stop
making Isabelle releases.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
