Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 22 2022 at 14:27):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,

consider the following record definition:

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"

Cheers,
René

Email Gateway (Aug 22 2022 at 14:28):

From: Makarius <makarius@sketis.net>
Bisection leads to

The first bad revision is:
changeset: 63253:9986559617ee
parent: 63241:f59fd6cc935e
user: haftmann
date: Mon Jun 06 22:22:05 2016 +0200
summary: clear distinction between different situations concerning
strictness of code equations

It is unclear to me, what happens here. Florian needs to look at it.

Makarius

Email Gateway (Aug 22 2022 at 14:29):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc

Email Gateway (Aug 22 2022 at 14:29):

From: Makarius <makarius@sketis.net>
Yes, we cannot do anything right now. The record package is lagging
behind many years and still awaiting proper localization.

Makarius
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC