[isabelle-dev] Avoid pollution of global code setup

Lars Hupel hupel at in.tum.de
Thu Mar 23 11:11:20 CET 2017

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


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


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.

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

More information about the isabelle-dev mailing list