On Fri, 7 Dec 2012, Florian Haftmann wrote:
Hi Makarius,
In Isabelle/7c8ce63a3c00 from today, the isabelle build dependency check
should be a bit faster, although I had to disable the parallelization
again, because it is unstable in scala-2.9.2 (in scala-2.10.0.RC3 it
appears to work).
http://isabelle.in.tum.de/reports/Isabelle/rev/ee729dbd1b7f#l1.310 looks
like a revival of the ancient »this belongs to foo« joke. Is this
supposed to stay?
"This belongs to foo" was indeed very odd when we had lots of that in the
bad old times of ML files as theory appendix, and without proper context.
Now the ML_file command does the right thing, without requiring separate
dependency declaration, but it is slow to discover in a large theory file.
For now the above change reduces the time for HOL from 3.5s to 2.4s on the
machine where I tried it. The "joke" in Divides saves approx. 150ms.
When I get better ideas to approach the slow dependency problem at some
later stage we can remove that again.
I did try throwing more cores at the problem, but it produced another bad
joke: 027d405951c8 and 7c8ce63a3c00. After spending some hours to get the
main operation for theory dependencies into a form where I can insert some
(Java) Futures, it started emitting NPE particles in an erratic way.
A move to scala-2.10.0 (when it is released) would reduce the time by
another factor 2.0 on 8 cores. But that is not decisive right now.
The selector in jEdit always has appeared pointless to me since it is
only in effect after a restart.
I have fine-tuned this to make some sense, without any real change yet. So
you can select any session you want, and after reboot and the implicit
build of it you get it.
There is still no on-line build manager within the IDE. It would be a big
improvement, because an already running JVM is much faster than one that
has just started on the command line. The JVM is like a huge Diesel
engine that requires pre-heating.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
