[isabelle-dev] scala-2.11.0

[Gottfried Barrow]

On 14-05-05 04:39, Makarius wrote:
> Here is a funny presentation on the Future of Programming from "1973"
> http://worrydream.com/#!/TheFutureOfProgramming

Makarius,

What's funny is that during the first minute of the video, I thought 
someone had inserted a laugh-track for what we would think is funny, but 
after they stopped laughing at the right points, and after I searched on 
"Bret Victor" to see how old he would be these days, I figured out, and 
saw, that it was done in 2013.

This email here is related to your "Notes on Isabelle/Scala systems 
programming":

https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2014-April/005266.html

https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2014-April/005267.html

It's about your general emphasis on Scala, the PIDE Scala console, and 
to my own programming language choices.

I could write the "long version" here, but I try to make this the "short 
version" (though it's not that short).

I'm a user of Isabelle, and that's all I ever want to be, no matter how 
much programming I might do, and user's needs are different than 
developer's needs.

If I was the unofficial manager of Isabelle software developers, then I 
would be pushing big time for my devs to make the move into Scala.

However, I'm the unofficial marketing guy, and a user, and it appears in 
this iteration of analysis, the right choice for "my group" is a 
combination of Ruby/JRuby for data processing, and Isabelle/ML for 
computational use of code generated export/import code, and for general 
control of Ruby/JRuby.

The context of all this is doing programming in a THY with bash calls, 
with bash being used in a ML{...}, and bash being used in the definition 
of other outer-syntax commands. You let "the cat out of the bag" by 
telling me how to use bash, both in ML, and by defining an outer syntax 
command. I'm glad you did.

Here, in keeping with the "forward looking" theme of the Bret Victor 
video, I make an audacious claim:

CLAIM: My use of Ruby/JRuby in a THY, which can partly be described as 
"using a REPL with an archived log," will move Isabelle/PIDE out of the 
niche market of theorem assistants, and into the mainstream of 
programming IDEs, where a big use of it will be for education.

It's actually not important that it's through me that programmers get 
exposure to all this, and it's not important that Ruby/JRuby becomes the 
language of choice for this.

Cutting this short(er), part of my reject of Scala was because external 
calls to the JVM are slow, which is important for "REPL use", but I 
figured out it's not of ultimate importance, which led to me installing 
and using JRuby in my own distribution folder.

This is my latest iteration, and when I come back to a language I've 
rejected, I come back with info that I keep and use from old iterations, 
such as the tips you gave me, part of which is a more educated use of 
the master directory, and switching to a file-based scheme.

I cut this short(er). From looking at this next link over the weekend, 
the speed of JRuby compared to Scala made me first think, "The choice is 
obvious, because of the speed of Scala."

http://benchmarksgame.alioth.debian.org/u32q/benchmark.php?test=all&lang=jruby&lang2=scala&data=u32q

But little things can make one language a better choice over another, 
for a given context. For sophisticated infrastructure and heavy 
machinery, Scala is obviously a better choice for running the PIDE, part 
of "obvious" being that you use it.

But, for scripting, whereas Scala only facilitates scripting, Ruby "is" 
a scripting language, as described by the author:

http://en.wikipedia.org/wiki/Ruby_%28programming_language%29#Early_concept

"Little things," like the specific way Ruby implements file includes, 
can be important.

Here's something important that gives me pattern matching in Ruby, 
Erlang style:

https://github.com/jdantonio/functional-ruby

I got it working by semi-magic. First, in PIDE, I executed "gem install 
functional-ruby" under Cygwin, and then I unmagically copied over the 
gem files to my JRuby distribution folder.

It finally occurred to me to do it semi-magically by starting a console 
Windows, and then execute "gem install functional-ruby" in the Windows 
console.

I'm just a user, which is what Isabelle needs more than developers. 
After this, I make a point of checking out of this.

I make my appearance to say, "Makarius, I understand your emphasis, and 
I've thought about it, and I agree that Isabelle developers should move 
into Scala, for what my opinion's worth. But if you see me doing 
Ruby/JRuby in PIDE, I've explained why, as of this iteration, and the 
use of Ruby in PIDE will make us both famous, or at least, it'll make 
you famous."

When I abandoned Scala, I was bummed, because Scala was going to 
increase my economic value, and get me a potential job as a programmer, 
not that I want a job. If I had to get a job, I'd rather be a graduate 
student getting a pittance of $10,000 a year, plus tuition costs, which 
would be no pittance to me.

By learning Ruby, I'm back to learning something of economic value, more 
so, I think, than even Scala.

The market. When my interests coincide with the interests of those in 
the mass market, that's not a bad thing.

Regards,
GB

Pertinent snippet:

> 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