Re: [isabelle] Efficient_Nat and Imperative-HOL, strange import-order dependent bug



Hi Peter,

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
import Efficient_Nat.
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.

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

Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.