[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Mon May 12 14:52:18 CEST 2014
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
* 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
More information about the isabelle-dev