On 15/11/15 02:24, Makarius wrote: > On Fri, 13 Nov 2015, Rafal Kolanski wrote: > >> On 12/11/15 16:45, Japheth Lim wrote: >>> [...] >>> A lot of space could be saved if Isabelle saves heaps in this way. For >>> our L4.verified project we found a 7× reduction in size. >> >> I would like to add that the 7x reduction is from 50GB for a full build >> of all our heaps (i.e. regression test). This allowed me to keep using >> my 250GB SSD, whereas previously I was struggling with space issues for >> weeks. When Japheth committed this little change, my jaw just about hit >> the floor. >> >> No adverse effects so far. Thumbs up. > > I usually trust David Matthews doing great things. > > Just formally, any change to make it into the official producation > quality version of Isabelle needs some extra efforts. It happens > routinely that old questions in the vicinity of a new feature need to be > revisited. If this is not done, there is a slow degration of overall > structural integrity of the system. > > One needs to resist from an attitude like "works for me, all great, no > problems, just do it".
I never said "just do it". I said "thumbs up. That means the change caused very significant positive effects and I second the desire to have it looked at seriously in order to discover and mitigate any negative effects. I just have none to report. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev