Re: [isabelle] Disk usage in ~/.isabelle/contrib



On Sun, 7 Feb 2016, Matthew Fernandez wrote:

When Isabelle detects that it is missing a component (Poly/ML, JDK, etc.) it fetches a tarball of this to ~/.isabelle/contrib and then decompresses it here. Each tarball contains necessary files for all supported platforms. I.e. in the extreme, a component like Poly/ML contains subdirectories for 32-bit Linux, 64-bit Linux, 32-bit Mac OS, 64-bit Mac OS and 32-bit Cygwin. My question is, why is Isabelle fetching all these things that will remain unused on my platform? Is this the result of a "disk space and bandwidth are free" mode of thought?

None of this is relevant for proper Isabelle distributions (releases or intermediate snapshots made with "isabelle makedist"). All required components are bundled, and shrunk to the requirements of specific platforms.

In contrast, the key purpose of cumulatively loaded components is to work with the Isabelle repository, e.g. for testing or continued development. This often happens with different platforms with a shared contrib directory.

It is also important to be able to walk through the history and have the correct components available. Admin/components within the repository specifies what is required at each point. This explains, why "isabelle components" works monotonically, without ever deleting anything.


Or a decision made for ease of packaging?

Isabelle component management is already quite advanced: all efforts are put into proper end-user bundles. The administrative tool "isabelle makedist_bundle" delivers separate platform-specific bundles -- the ones from the Isabelle download site.

People hooked on the repository need to decide themselves which components they want to keep and which they want to delete. I routinely dispose huge jdk things, when I have reasons to believe that I won't need them aany time soon.


My interest is driven by one of my machines where disk space *is* an issue. A quick scan of ~/isabelle/contrib reveals 2.7GB of files I could easily do without.

I have 20GB of local contrib stuff on a fast SSD. It used to be 40GB a few weeks ago, before I cleaned it up a little.


The remaining question is: How is this relevant to isabelle-users at all?

Why not use the shrink-wrapped official release? (This is not a rhetoric question, but the key question on this thread.)


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.