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

You are completely correct, Makarius. I forgot that we (Data61) were using a repository snapshot, rather than a release.
Apologies for the confusion. Some further clarification inline below.

On 07/02/16 23:57, Makarius wrote:
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.

Yes, I was not suggesting that "isabelle components" should ever delete older components.

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

Entirely correct. Sorry.


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.

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