[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Fri Jun 27 14:34:40 CEST 2014
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.
More information about the isabelle-dev