[isabelle-dev] scala-2.11.0
Makarius
makarius at sketis.net
Mon May 5 11:39:33 CEST 2014
Here is a funny presentation on the Future of Programming from "1973"
http://worrydream.com/#!/TheFutureOfProgramming
I could have put that on the thread "Remaining uses of Proof General",
because it touches recurrent problems of getting stuck with accidental
situations over decades, and the importance to unlearn old customs. But it
also fits here on the thread about scala-2.11.0 and actors.
The talk briefly contrasts old-fashioned "threads + locks" with the
brand-new actor model:
Carl Hewitt; Peter Bishop; Richard Steiger (1973). A Universal Modular
Actor Formalism for Artificial Intelligence. IJCAI.
As already explained, Scala had an on-board implementation of actors over
several years, but it is now deprecated. The replacement is the huge Akka
framework. So I discontinued that in Isabelle/Scala, and replaced it by a
plain "threads + locks" implementation of the more elementary concept of
Consumer_Thread.
That is basically a plain function with asynchronous input queue, and
simple means to apply it in synchronous mode (without result). If a
result is required it can be done with Future.promise, as seen here
http://isabelle.in.tum.de/repos/isabelle/annotate/bc50d5e04e90/src/Pure/Tools/simplifier_trace.scala#l139
for example.
The performance of the Consumer_Thread input queue (Mailbox) is much
better than that of the old actors, and resource allocation is more
predictable. I have started using that a bit more often now, e.g. in the
now asynchronous interpreter of the Scala console in Isabelle/jEdit
http://isabelle.in.tum.de/repos/isabelle/annotate/69531d86d77e/src/Tools/jEdit/src/scala_console.scala#l137
Makarius
More information about the isabelle-dev
mailing list