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

[Thomas Sewell]

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
  <recordname>_ext_Tuple_Iso

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
today.

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.


        Makarius

________________________________

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>