[isabelle-dev] [isabelle] Disk usage in ~/.isabelle/contrib

[Matthew Fernandez]

On 13/02/16 01:41, Makarius wrote:
> On Mon, 8 Feb 2016, Matthew Fernandez wrote:
>
>> A patch (not against the current tip) that pulls from a local mirror in preference to fetching remotely is as follows.
>> This may also be useful for other Isabelle devs looking to pull from a local mirror in preference to always hitting TUM.
>
> It is unclear to me what is the problem here. The settings variable ISABELLE_COMPONENT_REPOSITORY points to
> http://isabelle.in.tum.de/components by default, but that may be changed in $ISABELLE_HOME_USER/etc/settings in the
> usual way.

There is no problem. The motivation for this tweak (or spice as it seems to now be called on this mailing list) was that
it was simple for us to mirror the components on an internal machine that all users had SSH access to. The machine in
question doesn't run a web server, so retrieving components via rsync was simpler than going through the necessary
channels to get approval to modify the server's daemons. As far as I'm aware, the server's directory is periodically
updated from the TUM directory via wget/curl, so no magic required there. Perhaps, for most people, straightforward
mirroring of the TUM site is preferable, in which case I hope my post has not caused confusion or distraction.

> The remaining task is to maintain a complete mirror of http://isabelle.in.tum.de/components (which is presently at 12GB
> total). Some rsync setup should to the job, although we don't have that on the standard Isabelle rsyncd, as far as I can
> see. It should be possible to rsync via ssh for anyone who has access to TUM.
>
> Note that /home/isabelle/components contains a few non-world-readable files that are not accessible via HTTP and are not
> meant to be published, due to odd licenses of the tools in question.
>
>
>      Makarius

________________________________

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.