[isabelle-dev] Remaining uses of Proof General?

[Makarius]

On Tue, 29 Apr 2014, Thomas Sewell wrote:

>>  Back to the actual technical questions.  What are the main performance
>>  bottle-necks here? Printing of intermediate goal states?  Or applying
>>  intermediate steps repeatedly?
>
> I suspect that the problem is not that the printing or the intermediate 
> calculations are taking too long. It's that printing the output the user 
> wants to see is waiting on some other computation finishing, creating 
> the sensation of lag.
>
> Some evidence to back this up: I tried an adjustment a while ago in 
> which I had the goal state print incrementally. Even if some of the 
> subgoals took a while to print, you'd see the line with "goal (12 
> subgoals)" immediately, and then the subgoals as they were formatted. 
> The short summary is that this helped a little sometimes, but I often 
> still saw an empty Output panel for seconds after moving the cursor to a 
> line that the continuous checker had already processed.

Fast rewind to the start of this sub-thread, with the standard procedure 
according to Tim the Enchanter:

    * What are your exact hardware parameters: CPU, main memory?

    * What is your operating system?

    * What are your ML system settings, e.g. as shown by "isabelle build -?" ?

    * What are your JVM settings: ISABELLE_JAVA_SYSTEM_OPTIONS and
      JEDIT_JAVA_OPTIONS ?

    * What are the options "threads" and "parallel_proofs" ?

To put this into proper context some clues about the actual applications 
would also help to put obscure speculations into the bright light of 
empirical science.


 	Makarius