Admin/lib/Tools/makedist_cygwin
author wenzelm
Thu, 10 Jan 2013 19:07:44 +0100
changeset 50807 c065f3d14197
parent 50806 c19dba2d7ffe
child 50811 d02b9918e4d4
permissions -rw-r--r--
clarified cygwin/isabelle scripts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50806
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
     2
#
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
     3
# DESCRIPTION: produce pre-canned Cygwin distribution for Isabelle
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
     4
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
     5
## diagnostics
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
     6
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
     7
PRG=$(basename "$0")
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
     8
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
     9
function usage()
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    10
{
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    11
  echo
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    12
  echo "Usage: isabelle $PRG"
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    13
  echo
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    14
  echo "  Produce pre-canned Cygwin distribution for Isabelle."
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    15
  echo
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    16
  exit 1
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    17
}
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    18
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    19
function fail()
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    20
{
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    21
  echo "$1" >&2
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    22
  exit 2
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    23
}
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    24
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    25
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    26
## arguments
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    27
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    28
[ "$#" -ne 0 ] && usage
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    29
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    30
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    31
## main
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    32
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    33
TARGET="$PWD/cygwin"
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    34
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    35
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    36
# download
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    37
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    38
[ ! -e "$TARGET" ] || fail "Target already exists: \"$TARGET\""
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    39
mkdir -p "$TARGET/isabelle" || fail "Failed to create target directory: \"$TARGET\""
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    40
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    41
perl -MLWP::Simple -e "getprint 'http://cygwin.com/setup.exe';" > "$TARGET/isabelle/cygwin.exe"
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    42
chmod +x "$TARGET/isabelle/cygwin.exe"
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    43
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    44
"$TARGET/isabelle/cygwin.exe" -h </dev/null >/dev/null || exit 2
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    45
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    46
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    47
# install
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    48
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    49
"$TARGET/isabelle/cygwin.exe" \
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    50
  --local-package-dir "$(cygpath -w "$TMP/cygwin")" \
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    51
  --root "$(cygpath -w "$TARGET")" \
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    52
  --packages libgmp3,perl,python,rlwrap \
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    53
  --no-shortcuts --no-startmenu --no-desktop --quiet-mode
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    54
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    55
[ "$?" = 0 -a -e "$TARGET/etc" ] || exit 2
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    56
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    57
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    58
# patches
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    59
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    60
for NAME in hosts protocols services networks
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    61
do
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    62
  rm "$TARGET/etc/$NAME"
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    63
done
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    64
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    65
ln -s cygperl5_14.dll "$TARGET/bin/cygperl5_14_2.dll"
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    66
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    67
rm "$TARGET/Cygwin.bat"
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    68
50807
c065f3d14197 clarified cygwin/isabelle scripts;
wenzelm
parents: 50806
diff changeset
    69
cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/." "$TARGET/isabelle/."
c065f3d14197 clarified cygwin/isabelle scripts;
wenzelm
parents: 50806
diff changeset
    70