[isabelle-dev] scala-2.11.0

[Makarius]

On Wed, 23 Apr 2014, Makarius wrote:

> I am presently considering to discontinue actors altogether, and merely 
> use the thread task pool, explicit threads, and typed channels between 
> them.  But I also need to see how Akka actors do it today, to get a few 
> more ideas, before trimming it down to the simplest possible approach.

I have done this now in Isabelle/e1317a26f8c0 (and the row of changes 
before it).

After looking at the approx. 500 pages Akka manual, its sources, and the 
sources of scala.concurrent, I learned a lot how big industrial-strength 
concurrency frameworks are done these day.  Akka does have a purpose (e.g. 
for the Twitter server infrastructure), but not for us -- we are just 
doing a little shared-memory multiprocessing with one machine and two 
processes.

So most of the PIDE "operating system" functionality is now re-implemented 
by more basic means, in just 48 hours.  It is interesting that this can be 
done, but that is mostly a port of existing Isabelle/ML modules from 
src/Pure/Concurrent.  The resulting Scala/PIDE sources are more concise, 
and the implementation presumably more robust and efficient.


This means we no longer depend on the deprecated scala.actors library at 
all.

That was a fine master / PhD project by Phillip Haller some years ago, but 
it is no longer actively maintained.  In the early years of PIDE, I spent 
a lot of energy to isolate its hidden performance problems, e.g. due to 
the use of standard mutable structures from Java like
http://www.docjar.com/html/api/java/util/concurrent/LinkedBlockingQueue.java.html
instead of the more canonical queue that is now a hybrid Isabelle module
http://isabelle.in.tum.de/repos/isabelle/annotate/f2ffead641d4/src/Pure/Concurrent/mailbox.ML
http://isabelle.in.tum.de/repos/isabelle/annotate/f2ffead641d4/src/Pure/Concurrent/mailbox.scala

The Isabelle/ML Mailbox uses our canonical Queue implementation, and the 
Isabelle/Scala the same canonical Queue from the scala.collection library, 
which explains the meaning of the word "canonical".  The Mailbox started 
as a toy example some years ago for concurrent programming in ML, but 
seems to perform quite well in the Prover IDE.


In the coming weeks / months we need to watch out for new problems that 
were inevitably introduced by such substantial changes of the PIDE 
mechanics.  I also need to start thinking about "converging" towards the 
release this summer.


 	Makarius