[isabelle-dev] Isabelle build and jedit startup

[Makarius]

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