Re: [isabelle] Efficient_Nat and Imperative-HOL, strange import-order dependent bug
No, you don't. For this particular case, just make sure that every theory with an
export_code imports Efficient_Nat at the end of its imports list. AFAIK, the merge is
performed even if some anchestor theory has already imported Efficient_Nat, so you can
always force the declarations from Efficient_Nat again.
It probably means that I have to restructure my theory tree such that
export_code is only performed in leave-theories, where I can safely
Efficient_Nat violates the locality principle, because it changes some setup of Isabelle
that can be accessed in other ways. Such non-monotonic changes result in non-trivial
merges and often cause trouble sooner or later. IIRC, Imperative_HOL respects locality in
that the whole setup is declared once and for all, so if everything is based on the single
entry point Imperative_HOL.thy, everything should be fine.
I only hope that Imperative_HOL does not make
changes that get overwritten, too, as this would mean that no non-leaf
theory could be based on Imperative_HOL.
This archive was generated by a fusion of
Pipermail (Mailman edition) and