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.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
