[isabelle-dev] scala-2.11.0

[Makarius]

On Mon, 5 May 2014, Gottfried Barrow wrote:

> I guess it's basically the same, in that the JVM is started up each time, 
> which takes about 2 seconds, whether for Scala or JRuby. A short script that 
> uses a C-based language, like Perl, is just the cost of the bash call, which 
> is about 200ms.

On a Unix system that would be 2ms .. 20ms.  On Windows any external 
process is a bit expensive, which is the reason why I have "internalized" 
almost everything in the past 5 years or so, either into Isabelle/ML or 
Isabelle/Scala.

The ping-pong between the two processes has a latency of approx. 20ms 
(which is a builtin timeout), and very light load.  Throughput is quite 
high (100 .. 1000 MB/s).


>>  Here is a quick invocation of JVM functionality from inside Isabelle/ML:
>>
>>  ML {*
>>    Invoke_Scala.method "java.lang.System.getProperty" "java.home"
>>  *}
>
> I tried `Invoke_Scala.method "println" "'hello world'"`, but I got a 
> "Malformed method name" error, no matter how I tried to qualify "println".
>
> "Invoke_Scala.method" wouldn't help, because I need to run complete scripts, 
> though short scripts, not call single methods.

That is why I pointed to 
$ISABELLE_HOME/src/Tools/jEdit/src/scala_console.scala before -- it shows 
how to turn the Scala compiler into a plain method String => String.
This is the meaning of the word "interpreter".


> except for all the Isabelle developers, who are now thinking that life 
> is unfair, because of the need to learn yet another programming 
> language.

Isabelle/Scala is only for Isabelle system programming, the real hard 
Isabelle tool implementations are still done in Isabelle/ML.

Isabelle/Scala is also not just "Scala", but a stylistic restriction to 
something that approximates Isabelle/ML as much as feasible.  5 years ago, 
I was more in favour of actual Scala style, but that has diverged a lot in 
recent years.  And the quick and easy actor library replacement shows that 
Isabelle/ML has something to give to the Scala environment -- I just 
ported existing ML modules for that.


 	Makarius