Admin/lib/Tools/makedist_cygwin
author wenzelm
Tue, 02 Aug 2016 11:49:30 +0200
changeset 63578 e8990d0e3965
parent 63490 9416333a17c2
child 64344 c1695143de35
permissions -rwxr-xr-x
tuned;
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
50834
506342881c33 refer to cygwin mirror with static copy of setup.ini;
wenzelm
parents: 50811
diff changeset
     5
## global parameters
506342881c33 refer to cygwin mirror with static copy of setup.ini;
wenzelm
parents: 50811
diff changeset
     6
61827
31054660f285 current Cygwin snapshot in preparation of release;
wenzelm
parents: 60005
diff changeset
     7
CYGWIN_MIRROR="http://isabelle.in.tum.de/cygwin_2016"
50834
506342881c33 refer to cygwin mirror with static copy of setup.ini;
wenzelm
parents: 50811
diff changeset
     8
506342881c33 refer to cygwin mirror with static copy of setup.ini;
wenzelm
parents: 50811
diff changeset
     9
50806
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    10
## diagnostics
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    11
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    12
PRG=$(basename "$0")
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    13
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    14
function usage()
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    15
{
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    16
  echo
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    17
  echo "Usage: isabelle $PRG"
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    18
  echo
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    19
  echo "  Produce pre-canned Cygwin distribution for Isabelle."
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    20
  echo
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    21
  exit 1
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    22
}
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    23
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    24
function fail()
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    25
{
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    26
  echo "$1" >&2
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    27
  exit 2
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    28
}
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
## arguments
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    32
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    33
[ "$#" -ne 0 ] && usage
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
## main
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    37
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    38
TARGET="$PWD/cygwin"
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    39
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    40
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    41
# download
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    42
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    43
[ ! -e "$TARGET" ] || fail "Target already exists: \"$TARGET\""
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    44
mkdir -p "$TARGET/isabelle" || fail "Failed to create target directory: \"$TARGET\""
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    45
63490
9416333a17c2 prefer curl: presumably more portable and versatile;
wenzelm
parents: 61889
diff changeset
    46
type -p curl > /dev/null || fail "Cannot download files: missing curl"
9416333a17c2 prefer curl: presumably more portable and versatile;
wenzelm
parents: 61889
diff changeset
    47
curl --fail --silent "$CYGWIN_MIRROR/setup-x86.exe" > "$TARGET/isabelle/cygwin.exe" || \
9416333a17c2 prefer curl: presumably more portable and versatile;
wenzelm
parents: 61889
diff changeset
    48
  fail "Failed to download \"$CYGWIN_MIRROR/setup-x86.exe\""
50806
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    49
chmod +x "$TARGET/isabelle/cygwin.exe"
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    50
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    51
"$TARGET/isabelle/cygwin.exe" -h </dev/null >/dev/null || exit 2
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    52
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    53
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    54
# install
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    55
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    56
"$TARGET/isabelle/cygwin.exe" \
50834
506342881c33 refer to cygwin mirror with static copy of setup.ini;
wenzelm
parents: 50811
diff changeset
    57
  --site "$CYGWIN_MIRROR" --no-verify \
50839
9cc70b273e90 prefer MS-DOS-style temp;
wenzelm
parents: 50838
diff changeset
    58
  --local-package-dir 'C:\temp' \
50806
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    59
  --root "$(cygpath -w "$TARGET")" \
63490
9416333a17c2 prefer curl: presumably more portable and versatile;
wenzelm
parents: 61889
diff changeset
    60
  --packages curl,nano,perl,perl-libwww-perl,rlwrap,unzip \
50806
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    61
  --no-shortcuts --no-startmenu --no-desktop --quiet-mode
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    62
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    63
[ "$?" = 0 -a -e "$TARGET/etc" ] || exit 2
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    64
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    65
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    66
# patches
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    67
50887
1cadc8a8b377 avoid odd copies of local configuration or backup files;
wenzelm
parents: 50839
diff changeset
    68
for NAME in hosts protocols services networks passwd group
50806
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    69
do
60005
e1d8c5099bef updated Cygwin near 1.7.35-1;
wenzelm
parents: 58780
diff changeset
    70
  rm -f "$TARGET/etc/$NAME"
50806
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    71
done
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    72
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    73
rm "$TARGET/Cygwin.bat"
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    74
50811
wenzelm
parents: 50807
diff changeset
    75
wenzelm
parents: 50807
diff changeset
    76
# archive
wenzelm
parents: 50807
diff changeset
    77
50834
506342881c33 refer to cygwin mirror with static copy of setup.ini;
wenzelm
parents: 50811
diff changeset
    78
DATE=$(date +%Y%m%d)
506342881c33 refer to cygwin mirror with static copy of setup.ini;
wenzelm
parents: 50811
diff changeset
    79
tar -C "$TARGET/.." -cz -f "cygwin-${DATE}.tar.gz" cygwin