[isabelle] Real time in generated code
I am using Isabelle/HOL to produce executable Scala code from suitable specifications.
I can get some code returning the value of some function upon a given argument.
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.
In general, how do you exploit machine's clock at runtime?
Googling, I found references to timeap/timeit and to Time.now ().
1) Would any of these approaches be useful for the problem stated above?
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 ML layer?
This archive was generated by a fusion of
Pipermail (Mailman edition) and