Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes



> But your argument that this feature was not documented and seemed crazy to you and that thus you felt free to change it shows a cavalier attitude towards source code.

For the record: I did not change the source code. The code for the new package had to be rewritten from scratch (a few hundred lines), and we had to choose how to design it. Compatibility was a high concern, but I failed to realize that this apparently minor issue would have any impact at all on existing formalizations (failing to think that anything of the form "0 <= ..." is trivial to prove), while leading to (in my eyes) a cleaner approach. Implementing the old approach wouldn't have been harder; but it just felt "uglier" and "wrong". Now I know better.

Overall, we managed to achieve very high levels of backward compatibility and actually pulled it off. The ongoing "Nominal2" vs. "Nominal" is reminder of how hard it is to subsume and replace an existing Isabelle package. We (I) have made bona fide errors along the way, but I think our record is remarkable and deserves more praise than criticism.

Jasmin





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