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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to