[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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