Re: [isabelle] Real time in generated code
On Tue, 21 Jan 2014, marco caminati wrote:
However, I would also like this code to be triggered by time events at
runtime. For example, I would like the code to output its values every
second. A simple way I had in mind was to add an argument to the
specification of my function representing time, and then to plug a time
counter into that argument, but I'm digressing.
Andreas Lochbihler has already given some hints that this is probably just
a question how to wrap the Isabelle-generated Scala code into something
that lies outside the image of your original Isabelle/HOL specifications.
So it is mostly about some timer or thread programming on the JVM, using
Scala to access regular Java APIs.
Googling, I found references to timeap/timeit and to Time.now ().
timeap/timeit are from Isabele/ML.
Time.now is from Standard ML and it is OK to use in Isabelle/ML as well
(this is not always the case for such SML basis library things).
2) I am only familiar with Isar, but I understand that to use these
approaches I should embed ML code in it, right? In this case, is
there a good primer to descend from the Isar layer to the underlying
Step 0 is to get the basic mental model about Isabelle right, including
some elementary terminology. Isabelle is a framework of many different
languages: Isabelle/Pure, Isabelle/HOL, Isabelle/ML, Isabelle/Scala, ...
Isabelle/XYZ according to your own imaginations if you like.
Some of these languages are intertwined, and embeded into each other in
certain ways, but it does not make sense to speak of "layers" or to
"descend" -- especially not for the special pair Isabelle/Isar versus
The canonical picture to keep in mind is
http://en.wikipedia.org/wiki/File:Yin_and_Yang.svg -- sometimes this one
also helps: http://en.wikipedia.org/wiki/File:Klein_bottle.svg
You can learn more about Isabelle/ML in the "implementation" manual that
is included in Isabelle, e.g. Documentation panel in Isabelle/jEdit.
There is also a tiny example at the bottom of the same panel:
src/HOL/ex/ML.thy. It includes some bits of HOL -> ML code generation,
but not Scala.
That is an interesting pastime, but it is probably irrelevant to your
This archive was generated by a fusion of
Pipermail (Mailman edition) and