Re: [isabelle] Isabelle2016-1-RC3: problem with records



Am 27.11.2016 um 15:24 schrieb Makarius:
> On 25/11/16 14:15, Thiemann, Rene wrote:
>>
>> record foo = 
>>   a :: bool
>>   a' :: bool
>>
>> It compiles with Isabelle 2016, but not with Isabelle 2016-RC3.
>> In the release candidate there is a name clash of internal variables
>> in the record construction which seem to be generated by just adding
>> a prime (â):
>>
>> Duplicate variables on left hand side of equation, in theorem:
>> equal_foo_ext_inst.equal_foo_ext âa = ?a, a' = ?a', â = ?moreâ âa = ?a', a' = ?a'', â = ?more'â â
>> ?a = ?a' â ?a' = ?a'' â ?more = ?more'
>> Failed to define record "foo"

The problem is more fundamental than anticipated:

> declare [[record_codegen = false]]
> 
> record foo = 
>   a :: bool
>   a' :: bool
> 
> thm ext_inject

âa = ?a, a' = ?a', â = ?moreâ =
âa = ?a', a' = ?a'', â = ?more'â â
(?a â ?a') â
(?a' â ?a'') â ?more = ?more'

I. e. the rule for injectiveness already carries a name clash (?'a used
for both arguments).  The mentioned changeset just reports the
consecutive failure concerning code equations explicitly.

A glimpse at the code guides to line record.ML:1586 that explicitly
mentions that a a' deficiency

	val inject_prop =  (* FIXME local x x' *)

where the comment was added in b5d1873449fb about 5 years ago.

The code behind seems to date back to 2004.

This particularly means that such record declarations are likely to
never have worked properly â and definitely do not produce a proper
inject rule in Isabelle2016, which I have checked explicitly.

For the moment I am inclined not to risk a last minute change to that
ancient record package layer, although the resulting error message is,
admittedly, cryptic.

Cheers,
	Florian





-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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