[isabelle-dev] Towards release

[Lukas Bulwahn]

On 09/19/2011 01:56 PM, René Thiemann wrote:
> 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.
>
Alex seems to have fixed this issue with changeset 8b74cfea913a -- so, 
if you can get hold on any version >= 8b74cfea913a, you can report if 
there are further unresolved issues.
The mentioned changes of the code generator are also already in the 
repository.


Lukas

> Cheers,
> René