[isabelle] Disk usage in ~/.isabelle/contrib · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 22 2022 at 12:50):

From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Hi all,

The latest candidates for the upcoming Isabelle release contain some changes to reduce disk usage of heap images. So I
thought it might be a good time to ask other disk usage related questions. None of the below is intended to be
interpreted as a request for changes to the upcoming release; just questions seeking clarification.

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? Or a decision made for ease of
packaging? None of this is meant as a criticism, I would just like to understand the motivation(s).

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. A minimal first step to reducing this in future would seem to be to download
the tarballs to a temporary location, then delete them after decompressing. Is there a need for them to persist? Perhaps
there are some deeper issues I'm not aware of here.

Thanks,
Matt

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.

Email Gateway (Aug 22 2022 at 12:50):

From: Rafal Kolanski <xs@xaph.net>
I always carry a large bag of workarounds and little hope of upstream
changes. So while your question awaits a more comprehensive answer, some
observations:

you can delete the .tar.gz files in contrib, they don't get
re-downloaded as long as the component itself exists
inside the jdk directories, you can delete the platforms you don't
need; e.g. jdk-8u72 is 1.4GB, but its x86_64-linux dir is only 353MB
everything else doesn't occupy much space - closest candidate is
polyml weighing in at a whopping 83MB

The above can be written into a script, although since component updates
happen about twice a year I haven't bothered. On that note, could you
send me your isabelle components mirror fallback mod?

Raf.

Email Gateway (Aug 22 2022 at 12:51):

From: Makarius <makarius@sketis.net>
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

Email Gateway (Aug 22 2022 at 12:51):

From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
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.

Email Gateway (Aug 22 2022 at 12:51):

From: Makarius <makarius@sketis.net>
So what are the reasons for people at Data61 using a repository snapshot?
I thought that vice had been given up in 2005.

Or is it an official Isabelle release that has been "spiced up" by local
patches?

In the latter case, I recommend to produce a proper release locally, with
a name that is derived from the official one, but different from it.
E.g. like this:

hg tag Isabelle2016-Data61
Admin/Release/build -O -r Isabelle2016-Data61

This works in Linux and Mac OS X (e.g. Mountain Lion), but the latter is
required to produce macos bundles. Linux can produce only linux and
windows bundles, and the fonts of documentation is bad, because Gerwin and
Tobias like strange fonts.

Makarius

Email Gateway (Aug 22 2022 at 12:51):

From: Gerwin Klein <Gerwin.Klein@nicta.com.au>

On 8 Feb 2016, at 10:06 AM, Makarius <makarius@sketis.net> wrote:

On Mon, 8 Feb 2016, Matthew Fernandez wrote:

You are completely correct, Makarius. I forgot that we (Data61) were using a repository snapshot, rather than a release.

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

Entirely correct.

So what are the reasons for people at Data61 using a repository snapshot?
I thought that vice had been given up in 2005.

Or is it an official Isabelle release that has been "spiced up" by local patches?

It is precisely that. It just looks like a repository setup for locals.

In the latter case, I recommend to produce a proper release locally, with a name that is derived from the official one, but different from it. E.g. like this:

hg tag Isabelle2016-Data61
Admin/Release/build -O -r Isabelle2016-Data61

This is difficult from a configuration management point of view. Like in the Isabelle repository itself we want to be able to go back to old versions in history and have a link from our proofs to precisely the Isabelle version (change id, including any spice) and configuration that was applicable there. It’s also very useful to have the Isabelle repository directly there, to be able to study history, and to manage any additional spice as version-controlled branches.

This means we effectively deal with a Isabelle repository setup. I’m happy with that trade-off, but some of us are more perfectionist ;-) I think with the information so far, we can optimise our setup, though.

This works in Linux and Mac OS X (e.g. Mountain Lion), but the latter is required to produce macos bundles. Linux can produce only linux and windows bundles, and the fonts of documentation is bad, because Gerwin and Tobias like strange fonts.

Interesting. Do you mean the Concrete Maths font? I haven’t had any issues with it so far.

Cheers,
Gerwin

Email Gateway (Aug 22 2022 at 12:51):

From: Makarius <makarius@sketis.net>
As I have pointed out some years ago, the document in question is
prog-prove. On Debianistic Linux systems (e.g. Ubuntu) the result looks
very ugly, with low-resolution bitmap fonts.

I guess the problem is this combination:

\usepackage[T1]{fontenc}
\usepackage{ccfonts}
\usepackage[euler-digits]{eulervm}

Email Gateway (Aug 22 2022 at 12:52):

From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Thanks, will investigate. Tobias and I are mostly building on Macs, so we don’t see the Linux version often.

I’m at a summer school this week. Do we need this for the release or do I have time?

Cheers,
Gerwin

Email Gateway (Aug 22 2022 at 12:52):

From: Makarius <makarius@sketis.net>
This is not relevant for the release. In the past few releases I always
made sure that documents are built on Mac OS X.

Makarius

Email Gateway (Aug 22 2022 at 12:52):

From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Ok.
Gerwin

Last updated: Apr 25 2024 at 16:19 UTC