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
