[isabelle-dev] Localized record package [was: next release]

Thomas Sewell Thomas.Sewell at nicta.com.au
Thu Jan 14 15:16:13 CET 2016

Right. There was a plan here to investigate before the release, but the timing didn't work out.

Anyway, here's a modified record.ML that builds on Isabelle 2015 (which was stable and available). The only problem I've seen with it in my testing is failures in code_export. Yes, I haven't tested it exhaustively yet.

The code_export failure can be seen in the attached test theory, it's that there's no code equation for the constant

My understanding of the record code generator setup is that we've gone too deep somehow, the tuple-based type definition isn't meant to appear anywhere, the code generator is meant to pretend that "<recordname>_ext" is a datatype constructor. I'm not really sure how to investigate what's gone wrong.

OK, I attach the new version, the diff, and the test theory.

From: Makarius [makarius at sketis.net]
Sent: Friday, January 15, 2016 12:47 AM
To: Florian Haftmann; Thomas Sewell
Cc: isabelle-dev at mailbroy.informatik.tu-muenchen.de
Subject: Re: [isabelle-dev] Localized record package [was: next release]

On Thu, 14 Jan 2016, Florian Haftmann wrote:

> Hi Thomas,
>> There is some interest here at Data61 (NICTA that was) in having a
>> localised record package in Isabelle-2016. I've done the initial
>> implementation and got the parts of the package I understand working
>> within locales etc, but something goes wrong with the code generation
>> aspect. Is there anyone who understands how to debug the code generator
>> who'd have time to look at that?
> I am very sympathetic towards localized records, but this appears a too
> major change to be done so shortly before the next release.

I am also interested in a properly localized record package, for about 7
years. Since it is so huge an complex, it still did not happen until

The release train for Isabelle2016 is about to depart within a couple of
days, so it is pointless to consider changing anything there.  As usual,
big changes happen *after* a release not before it.  And even then, it can
take more than one release cycle to get it really through.



The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: record.ML
Type: application/octet-stream
Size: 91214 bytes
Desc: record.ML
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160114/131cfc73/attachment-0003.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: record-diff
Type: application/octet-stream
Size: 30122 bytes
Desc: record-diff
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160114/131cfc73/attachment-0004.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Test.thy
Type: application/octet-stream
Size: 290 bytes
Desc: Test.thy
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160114/131cfc73/attachment-0005.obj>

More information about the isabelle-dev mailing list