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".
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
