[isabelle-dev] Towards the Isabelle2017 release
Rene.Thiemann at uibk.ac.at
Mon Aug 28 10:28:38 CEST 2017
>> - There have been some changes w.r.t. code-generation which now lead
>> to runtime exception in the generated code. For instance, now
>> I get code like
>> “f x = Code.abort …”
>> whereas in 2016-1 there was a proper code like
>> “f x = some ordinary right-hand side”
>> We did not yet isolate the problem and will report later.
> OK, I will dig into this after you have isolated it. Might be well that
> this only occurs on certain theory merges.
The problem seems to be a change wrt. locale interpretations.
Consider the following code:
locale foo = fixes f :: "nat => nat"
assumes f_mono[termination_simp]: "f x <= x"
fun bar :: "nat => nat" where
"bar 0 = 0"
| "bar (Suc x) = Suc (bar (f x))"
definition com where
[code del]: "com = foo.bar id"
interpretation foo id
rewrites "foo.bar id = com"
unfolding com_def by (unfold_locales, auto)
lemma "com 5 = 5" by eval
export_code com in Haskell
This works perfectly fine in Isabelle 2016-1, and especially
the [code del] is required to make the final export_code and eval succeed.
In contrast, in a recent development version, the [code del] still is accepted,
but the export_code will deliver “com _ = error …” and the “eval” will fail.
The solution is easy: remove the previously required [code del].
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 842 bytes
Desc: Message signed with OpenPGP
More information about the isabelle-dev