[isabelle-dev] Avoid pollution of global code setup
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
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...
Size: 3745 bytes
Desc: not available
More information about the isabelle-dev