[isabelle-dev] mira disk usage

Lars Noschinski noschinl at in.tum.de
Sat Sep 1 09:30:28 CEST 2012


On 01.09.2012 01:15, Gerwin Klein wrote:
> I guess the problem is that build -b produces heap images for all sessions. These are many, and each image is hundreds of MB. The previous setup had images for selected base sessions only and no images for the rest (almost everything).

The "AFP" session in mira does only produce the base images, AFAICS:

$ ls AFP_c5dd6e9db74c4e9fadb373ec946c413a/polyml-5.4.1_x86_64-linux/
Collections                HOL-Nominal      Jinja               Pure
Group-Ring-Module          HOL-Probability  LatticeProperties 
Refine_Monadic
HOL                        HOL-Word         List-Infinite       Simpl
HOL-Multivariate_Analysis  HOLCF            Nat-Interval-Logic  log

> ps: "isabelle build" takes about 5 sec on my system to figure out dependencies (I think). Should this be faster?

I guess this time is spent hashing the dependencies to figure out, 
whether they have changed -- at least, it is not time based.

I know that Git uses stat info as a first step and only if this changes 
proceeds reading the file.

   -- Lars



More information about the isabelle-dev mailing list