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
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
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
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
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.
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
