Re: [isabelle] Isabelle2014-RC1 available for testing



Dear all,


Am 27.07.2014 um 21:10 schrieb Makarius <makarius at sketis.net>:

> in anticipation of the Isabelle2014 release in August, the first official release candidate Isabelle2014-RC1 is now available for testing:
> 
>  http://isabelle.in.tum.de/website-Isabelle2014-RC1
> 
> Some enthusiasm for testing is important to keep up with the high levels of system sophistication and user expectation that we have seen in recent years. Observations and problems of release candidates may be discussed here on isabelle-users

I observed a problem with datatype_new which was not present in Isabelle2014-RC0


theory Test
imports  
  Main
begin

typedef ('a,'b)com = "(UNIV :: ('a * 'b)set)" by auto

datatype_new ('q,'f) foo = Bar 'f "'q list" "('q,unit)com" 

***       [| a = local.foo.Bar x1 x2 x3; b = local.foo.Bar y1 y2 y3; R x1 y1;
***          x2 = y2; x3 = y3 |]
***       ==> thesis |]
*** ==> thesis
*** Proof failed.
***  1. !!x1 x2 x3 x1a x2a x3a.
***        [| R x1 x1a; list_all2 op = x2 x2a; x3 = x3a;
***           !!x1b x2b x3b y1 y2 y3.
***              [| x1 = x1b; x2 = x2b; x3 = x3b; x1a = y1; x2a = y2; x3a = y3;
***                 R x1b y1; x2b = y2; x3b = y3 |]
***              ==> thesis;
***           b = local.foo.Bar x1a x2a x3a; a = local.foo.Bar x1 x2 x3 |]
***        ==> thesis
*** The error(s) above occurred for the goal statement (line 8 of "~/Test.thy"):
*** [| local.foo.rel_foo R a b;
***    !!x1 x2 x3 y1 y2 y3.
***       [| a = local.foo.Bar x1 x2 x3; b = local.foo.Bar y1 y2 y3; R x1 y1;
***          x2 = y2; x3 = y3 |]
***       ==> thesis |]
*** ==> thesis

end

A hg bisect delivers f9dd8a33f820 as first problematic revision.

Kind regards,
René

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.