It turns out that with our collection of large Isabelle sessions that we run regularly, polyml heap image space is becoming a noticeable problem for us.
To give an impression, we are now daily generating hundreds of gigabytes of polyml heap images. We do this on SSDs, because they reduce build times significantly. For SSDs, hundreds of gigabytes is still a large percentage of total capacity. Raf noticed recently that simple fast compression such as LZO/liblzo works really well for disk heap images. We’re getting a size reduction to about 27% at speeds of about 400MB/s. Initially I thought we might write a little wrapper that compresses/decompresses as polyml writes/reads these images, but it’s awkward, duplicates path logic etc. Would this be something worthwhile to include directly in the polyml heap dumping process instead? That way it would not just benefit us, but everyone who uses Isabelle and other polyml-based sessions on SSDs. Cheers, Gerwin ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
