Re: [isabelle] Isabelle release candidate



Am 28/09/2011 17:55, schrieb Andreas Lochbihler:
> I have found the following inconveniences in the release candidate, but
> I consider none of them as release critical.
> 
> 1. The new induction method does not give the induction hypothesis the
> name IH (as advertised in the NEWS) when explicit parameter
> instantiations are given. Here's a silly example

Parameter instantiations can result in structural changes in the
hypotheses due to rewriting. It becomes pretty much impossible to figure
out at the end what is an induction hypothesis and what comes from the
side conditions. In such cases induction defaults to the old naming
schema. We would love to improve this in the future.

Tobias

> notepad begin
>   fix xs ys :: "'a list"
>   have "xs = ys"
>   proof(induction xs=="xs" rule: list.induct)
>     print_cases
>     oops
> end
> 
> 2. Undoing a proof over an oops in a notepad context (as above) does not
> work (at least with PG 3.7.1.1. and XEmacs; I haven't tested the other
> interfaces).
> 
> 3. partial_function sometimes does not check that the head of the
> equation is the same as the name of the constant to be defined, as in
> the attached example.
> 
> Andreas
> 
> 
> Am 27.09.2011 00:20, schrieb Makarius:
>> The next official Isabelle release is scheduled for October 2011. In
>> the 2-3
>> weeks before shipment there are traditional test releases, but this
>> time they
>> are called "release candidates" and announced to a wider audience.
>>
>> So Isabelle2011-1-RC1 is now available here:
>>
>> http://isabelle.in.tum.de/website-Isabelle2011-1-RC1/
>>
>> This enables users to try on their own machines, and see how their
>> applications
>> work with the coming release. Incompatibilites between the RCs and the
>> final
>> version should be neglibile.
>>
>> This gives an opportunity for last-minute fixes, but no feature
>> additions (the
>> de-facto feature freeze is usually 6 weeks before a release, so it is
>> long over).
>>
>> Feedback on problems can be posted on the list, or sent privately.
>>
>>
>> Makarius
>>
> 





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