On 14-05-05 15:37, Makarius wrote:
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".
I think that occurred to me after the fact
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
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
On Mon, 5 May 2014, Gottfried Barrow wrote:
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
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
The problem seems to be HyperCTL. From the log:
Run out of store - interrupting threads
Failed to recover - exiting
/tmp/isabelle-isatest/isabelle_script3270098471353362986: line 8:
/mnt/nfsbroy/home/isatest/afp/isadist/Isabelle_04-May-2014/lib/scripts/timestop.bash:
No such file or directory
Hy
Am 05.05.2014 um 11:17 schrieb Johannes Hölzl :
> Has anybody an idea why the AFP test for Probabilistic_Noninterference
> fails?
>
> When I build it on my machine
Same on my machine, and same for Selection_Heap_Sort, Native_Word, and
Launchbury: All work fine on my machine.
(HyperCTL has been
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 im
On Mon, 5 May 2014, Thomas Sewell wrote:
The basic assumption is that each proof task does not run too long, and if
it does it is something to be improved in the application to make it more
smooth. In contrast, Proof General makes it more easy to produce huge and
heavy proof scripts that ca
I use "isabelle afp_build Probabilistic_Noninterference" to build it,
which includes the document generation. So it is possible that the
document generation on the macbroy2 is different from my setup.
Looking into the reports attached to the status email, I also see that
the log for Probabilistic_
Has anybody an idea why the AFP test for Probabilistic_Noninterference
fails?
When I build it on my machine with either the combination in the email
(i.e. AFP acd2cc051b4f and Isabelle 52e5bf245b2a) or a recent hg version
(AFP a0a65428715f and Isabelle d940ad3959c5) it works without problems.
-
Could it be the document preparation?
Dmitriy
Am 05.05.2014 11:17, schrieb Johannes Hölzl:
Has anybody an idea why the AFP test for Probabilistic_Noninterference
fails?
When I build it on my machine with either the combination in the email
(i.e. AFP acd2cc051b4f and Isabelle 52e5bf245b2a) or a
12 matches
Mail list logo
