Dear Florian, >> - 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" begin fun bar :: "nat => nat" where "bar 0 = 0" | "bar (Suc x) = Suc (bar (f x))" end 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]. Cheers, René
signature.asc
Description: Message signed with OpenPGP
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
