Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
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
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
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
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
On 12/11/15 21:17, Lars Hupel wrote: Hi Japheth, 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. out of curiousity: How did you arrive at this number? Have you implemented incremental heaps for Isabelle? As I said, Poly/ML has supported this for a while. If you do not care about the compatibility issues (heap pathnames, and Makarius mentioned system stability concerns), the patch is quite simple: diff --git a/src/Pure/ML-Systems/polyml.ML b/src/Pure/ML-Systems/polyml.ML index 907c0f2..e0fec14 100644 --- a/src/Pure/ML-Systems/polyml.ML +++ b/src/Pure/ML-Systems/polyml.ML @@ -37,7 +37,8 @@ struct open ML_System; fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; -val save_state = PolyML.SaveState.saveState; +fun save_state file = +PolyML.SaveState.saveChild (file, length (PolyML.SaveState.showHierarchy ())) end; In L4.verified we are happy to use this patch for now, since no one in our group has run into the associated problems. Japheth 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. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
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. Rafal Kolanski. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
On Thu, 12 Nov 2015, Japheth Lim wrote: For a long time, Poly/ML has supported hierarchical heaps (PolyML.SaveState.saveChild). As I understand it, this feature was not used because it makes heaps no longer self-contained; moving them to a different path would break the loading process. Hierarchic heaps were once used in Isabelle, but discontinued since the persistency of mutable values was not properly supported. This has changed in various ways over the years, so it is something to be revisited eventually. David Matthews has kindly implemented a solution for that problem, allowing the application to specify all the paths in the hierarchy. See the announcement http://lists.inf.ed.ac.uk/pipermail/polyml/2015-November/001698.html I have seen that thread on the Poly/ML mailing list, and marked it as relevant. It remains to be seen if something happens before the coming release of Isabelle2016. Adding more and more features on the spot is always a temptation and a danger. Both Poly/ML and Isabelle/ML have changed significantly in the past few months, and the main priority is to wrap up for the release of both really-soon-now. For example, the native Windows support of Poly/ML can still crash in some situations. Pinning this down precisely has priority over optional add-ons. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
Hi all, Isabelle currently saves fully self-contained heaps. This is wasteful since a low-level session like HOL will be duplicated in every heap that depends on it. For a long time, Poly/ML has supported hierarchical heaps (PolyML.SaveState.saveChild). As I understand it, this feature was not used because it makes heaps no longer self-contained; moving them to a different path would break the loading process. David Matthews has kindly implemented a solution for that problem, allowing the application to specify all the paths in the hierarchy. See the announcement http://lists.inf.ed.ac.uk/pipermail/polyml/2015-November/001698.html 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. Japheth 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. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
