Dear all, > There are still some improvements to the Haskell serializer and the code > generator I would like to get into the release. > After some discussions with Florian, the remaining changesets are about ready > and final, so I can probably commit them till this Wednesday. > Afterwards, the code generator is probably best checked against the two > largest executable formalisations (JinjaThreads and CeTA) -- I will try to > get the developers to re-run these with a current repository version or the > first pre-release version.
When reading this post (and since we will port to the new distribution in any way), I started to adapt our library to the upcoming version where I used the bundle http://www4.in.tum.de/~wenzelm/test/Isabelle_11-Sep-2011/download.html After some first adaptations I got stuck when at the first place where we use partial_function. It seems that the partial_function package is broken if polymorphic types are used. (which was not the case in Isabelle2011) partial_function(option) foo :: "nat list \<Rightarrow> unit option" where "foo x = foo x" works, but partial_function(option) foo :: "'a list \<Rightarrow> unit option" where "foo x = foo x" yields the following error message. *** exception THM 0 raised (line 1175 of "thm.ML"): instantiate: type conflict *** ?F :: (?'a2 list \<Rightarrow> unit option) \<Rightarrow> ?'a2 list \<Rightarrow> unit option *** \<lambda>foo. foo :: ('a list \<Rightarrow> unit option) \<Rightarrow> 'a list \<Rightarrow> unit option *** At command "partial_function" (line 216 of "/Users/rene/devel/rewriting/IsaFoR/Loops_Impl.thy") or if I output sorts *** exception THM 0 raised (line 1175 of "thm.ML"): instantiate: type conflict *** ?F\<Colon>(?'a2\<Colon>type list \<Rightarrow> unit option) \<Rightarrow> ?'a2\<Colon>type list \<Rightarrow> unit option :: (?'a2\<Colon>type list \<Rightarrow> unit option) \<Rightarrow> ?'a2\<Colon>type list \<Rightarrow> unit option *** \<lambda>foo\<Colon>'a\<Colon>type list \<Rightarrow> unit option. foo :: ('a\<Colon>type list \<Rightarrow> unit option) \<Rightarrow> 'a\<Colon>type list \<Rightarrow> unit option *** At command "partial_function" (line 216 of "/Users/rene/devel/rewriting/IsaFoR/Loops_Impl.thy") I think this is a triviality since it looks to me that one just has to replace ?a2 by 'a, but I do not know where to fix it. After that, I'm happy to test any further version, also repository snapshots. Cheers, René _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
