*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes*From*: Jasmin Blanchette <jasmin.blanchette at inria.fr>*Date*: Wed, 18 Nov 2015 14:02:08 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <DE66FD44-D591-4599-90D7-8A3614A60D12@inria.fr>*References*: <564B1075.5060706@in.tum.de> <C67DA37B-EEE3-4BBD-9CEE-6AB41FF48ACE@inria.fr> <564B6249.8080603@in.tum.de> <564B6466.4070200@in.tum.de> <564C2743.7080809@inf.ethz.ch> <564C3C4F.9050400@in.tum.de> <9E245509-0BC3-4A1D-A2AE-0D5999744F36@inria.fr> <564C45BA.5000601@in.tum.de> <DB7D90EF-8B43-43AB-B220-ACD633CDF884@inria.fr> <564C685B.2020203@in.tum.de> <DE66FD44-D591-4599-90D7-8A3614A60D12@inria.fr>

> 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

**Follow-Ups**:

**References**:**[isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Manuel Eberl

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Jasmin Blanchette

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Manuel Eberl

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Manuel Eberl

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Andreas Lochbihler

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Manuel Eberl

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Jasmin Blanchette

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Tobias Nipkow

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Jasmin Blanchette

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Tobias Nipkow

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Next by Date: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Previous by Thread: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Next by Thread: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Cl-isabelle-users November 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list