[isabelle-dev] Remaining uses of Proof General?

[Makarius]

On Fri, 27 Jun 2014, Makarius wrote:

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

We did not yet revisit this systematically.  Are there remaining 
observations with sledgehammer and other query operations via the 
canonical GUI panels?  Lets say in Isabelle/2f46999395e2 from today.

Oddly, people are still seen using 'find_theorems' etc. inlined into the 
source text.  That was an intermediate approach from several years ago. If 
it is still used today, what are the remaining resons for it?


 	Makarius