[isabelle-dev] Avoid pollution of global code setup

[Lars Hupel]

Dear Isabelle developers,

I'm currently running some trials for my custom code preprocessor.
Internally, I use the "deriving" mechanism to obtain a linear ordering
for some of my types. While doing that, I noticed that just importing

  "$AFP/Datatype_Order_Generator/Derive"

pulls in code setup for natural numbers (in a way with which I can't
deal yet). In my case, the fix was simple; I just had to change the
import to

  "$AFP/Datatype_Order_Generator/Order_Generator"

The code setup came in via "$AFP/Collections/Lib/HashCode". I've created
a patch to afp-devel which removes the code setup there.

This is a potentially far-reaching change because we currently don't
test for concrete code setup, and this might introduce silent
performance regressions in generated code. I've spoken to Peter and he
seems okay with it as long as the code setup is retained in all other
places in the AFP (see attached patch).

Before pushing this patch to the AFP I wanted to make sure that nobody
else is affected by this change.

Cheers
Lars
-------------- next part --------------
A non-text attachment was scrubbed...
Name: code_target.patch
Type: text/x-patch
Size: 3745 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170323/a3b66dc1/attachment.bin>