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

[Matthew Fernandez]

[Moved to Isabelle-dev, as Makarius pointed out this is not relevant to users of Isabelle.]

On 07/02/16 22:51, Rafal Kolanski wrote:
> On that note, could you
> send me your isabelle components mirror fallback mod?

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.
Obviously this is not immediately suitable for upstream.

diff --git a/l4v/isabelle/lib/Tools/components b/l4v/isabelle/lib/Tools/components
index 1ba484c..759b56f 100755
--- a/l4v/isabelle/lib/Tools/components
+++ b/l4v/isabelle/lib/Tools/components
@@ -41,6 +41,7 @@ function fail()

  INIT_SETTINGS=""
  COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY"
+NICTA_COMPONENTS_MIRROR="<NICTA-specific URL goes here>"
  ALL_MISSING=""
  LIST_ONLY=""

@@ -122,6 +123,20 @@ else
      elif [ -d "$FULL_NAME" ]; then
        echo "Skipping existing component \"$FULL_NAME\""
      else
+      # Optimistically try to retrieve this dependency from the NICTA mirror to
+      # save bandwidth. In the case of any failure -- including things like
+      # missing rsync or unconfigured SSH keys -- fall back on the usual logic.
+      if [ ! -e "${FULL_NAME}.tar.gz" -a -n "${NICTA_COMPONENTS_MIRROR}" ]; then
+        REMOTE="${NICTA_COMPONENTS_MIRROR}/${BASE_NAME}.tar.gz"
+        echo "Getting \"${REMOTE}\""
+        mkdir -p "$(dirname "$FULL_NAME")"
+        rsync --progress --rsh='ssh -o "NumberOfPasswordPrompts 0"' \
+          --timeout=10 "${REMOTE}" "${FULL_NAME}.tar.gz"
+        if [ $? -ne 0 ]; then
+          echo "Failed; falling back on Isabelle component repository"
+          rm -f "${FULL_NAME}.tar.gz"
+        fi
+      fi
        if [ ! -e "${FULL_NAME}.tar.gz" ]; then
          REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"
          echo "Getting \"$REMOTE\""

________________________________

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.