[isabelle-dev] scala-2.11.0

[Gottfried Barrow]

On 14-05-05 10:48, Makarius wrote:
> Here I guess you mean something like the isabelle_scala_script 
> wrapper, which is indeed very slow on startup for two reasons:

No, I meant something like ML{*Isabelle_System.bash "jruby 
my_script.rb"*}, where I was using scala instead of jruby.

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.

It's only important if I'm working as with a REPL, but for longer 
scripts, which would be the main end use, it's not important. It would 
be annoying with Scala, but I can use Cygwin Ruby for working on a 
script, with have JRuby in my distribution folder for use by other 
people, and for my use also.

> 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".

Here, I start to summarize the situation, where what I say is also 
related to what you said in your latest email.

"Invoke_Scala.method" wouldn't help, because I need to run complete 
scripts, though short scripts, not call single methods.

At this point, If I don't use Scala, it will only be because I've 
decided Ruby/JRuby is a better choice for my needs, which comes down to 
two needs, data processing, Ruby being the better, and more modern 
choice, over Perl and Python.

The second need is computation using exported/imported code. With 
computation, I like the simplicity and signature/structure format of ML, 
and I'm pretty sure, from things I've read and seen, that Scala 
sometimes doesn't work with the code generator, because of its 
preference for non-curried functions, among other things.

Startup speed is not an issue. A new i7 will speed things up, and you 
most likely will someday tie Scala into something similar, and better, 
than what I'm doing.

> That gives you a String => String function invocation interface from 
> ML to Scala.  It is an easy exercise to use the YXML and XML.Encode / 
> XML.Decode modules to pass structured data back an forth.

What is data processing but the processing of strings? So, executing a 
complete script through bash, and getting a string back fits in with 
what scripting languages are good for. But to call single methods, and 
get strings back for each call, is not optimal.

> It is a reasonably easy exercise, to invoke the Scala compiler on some 
> source script on the spot, e.g. see the scala_console.scala in the 
> Isabelle/jEdit source directory.
>
> It is probably more than an exercise to invoke the Scala compiler in a 
> way that it produces nice IDE markup for the source text.

The bigger benefit of programming in Scala, in addition to its power, 
would be to semi-directly use global variables that can be used by 
Isabelle/ML, where the context here is users, rather than Isabelle 
product developers.

I assume, from what you've said up until now, and by what you haven't 
said in the past, that's not possible right now. I believe it's 
inevitable that you'll eventually create an interface between Scala and 
ML to do that.

Now, I go into unofficial marketing mode.

Earlier, I had found "Invoke_Scala.method" from doing some searches, and 
then, after experimenting with it a little, I forgot about it.

At this point, I halfheartedly look at Scala in case it could still be 
the right choice, but I don't think it is, except for all the Isabelle 
developers, who are now thinking that life is unfair, because of the 
need to learn yet another programming language.

Ultimately, I'm looking out for my needs, but it's in my nature to 
imagine I'm the marketing guy for a commercial product called Isabelle, 
where Isabelle is definitely a commercial-grade product.

You have Scala covered, and its use in Isabelle, and among programmers 
in general, is only going to get bigger.

Isabelle/ML, being tied in Poly/ML, Poly/ML being tied into C, C++, and 
assembly, is fundamental, it's fast, and it's not going to go away, but 
only get a little bigger for a time, and then go away after many years.

There are other languages to be called through bash, other than Perl and 
Python, such as Perl 6, Groovy, Haskell, Pure, and the three languages 
listed on the functional-ruby page, Erlang, Clojure, and Go, where I 
looked at Erlange for about 3 minutes, Go not at all, and Clojure for 
about 5 minutes, where I saw Clojure's Lisp-like syntax, with the 
obnoxious use of parentheses, though Clojure is undoubtedly still an 
important language.

In all this, to stay focused, I ask myself, "Do I want to prove 
mathematics, with a little bit of computation, or do I want to move into 
programming?"

My former decision to use only ML was an attempt to try and stay in 
mathematics, but I think I might can manage some use of Ruby, because a 
little extra work to set it up will pay off.

If I wanted to move into programming, I would set things up in the PIDE 
for maybe 3 languages, in addition to ML, and then show people how to 
use them in Isabelle, which would end up also teaching me how to use 
them. Eventually, I would heavily lock onto two of them.

That would be losing my focus.

ML for sound logic and speed. Scala for infrastructure and heavy 
machinery. Ruby for easy and fast scripting, with it's streamlined 
syntax. That's some heavy market coverage, and any language that works 
good, when called through bash, is potentially in the market, if someone 
makes a few tweaks to make it work, and shows people how to use it.

Thanks,
GB