[isabelle-dev] Towards release

[René Thiemann]

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é