Admin/lib/Tools/makedist_cygwin
author wenzelm
Fri, 24 Oct 2014 11:30:39 +0200
changeset 58780 1f8c0da85664
parent 57389 eb96243a25c5
child 60005 e1d8c5099bef
permissions -rwxr-xr-x
discontinued python from standard system environment;
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
57027
80ffda443738 updated cygwin;
wenzelm
parents: 53659
diff changeset
     7
CYGWIN_MIRROR="http://isabelle.in.tum.de/cygwin_2014"
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
53659
85ae414b0363 updated cygwin snapshot;
wenzelm
parents: 50958
diff changeset
    46
perl -MLWP::Simple -e "getprint '$CYGWIN_MIRROR/setup-x86.exe';" > "$TARGET/isabelle/cygwin.exe"
50806
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    47
chmod +x "$TARGET/isabelle/cygwin.exe"
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    48
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    49
"$TARGET/isabelle/cygwin.exe" -h </dev/null >/dev/null || exit 2
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    50
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    51
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    52
# install
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    53
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    54
"$TARGET/isabelle/cygwin.exe" \
50834
506342881c33 refer to cygwin mirror with static copy of setup.ini;
wenzelm
parents: 50811
diff changeset
    55
  --site "$CYGWIN_MIRROR" --no-verify \
50839
9cc70b273e90 prefer MS-DOS-style temp;
wenzelm
parents: 50838
diff changeset
    56
  --local-package-dir 'C:\temp' \
50806
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    57
  --root "$(cygpath -w "$TARGET")" \
58780
1f8c0da85664 discontinued python from standard system environment;
wenzelm
parents: 57389
diff changeset
    58
  --packages libgmp3,perl,perl_vendor,rlwrap,unzip,vim \
50806
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    59
  --no-shortcuts --no-startmenu --no-desktop --quiet-mode
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    60
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    61
[ "$?" = 0 -a -e "$TARGET/etc" ] || exit 2
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    62
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    63
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    64
# patches
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    65
50887
1cadc8a8b377 avoid odd copies of local configuration or backup files;
wenzelm
parents: 50839
diff changeset
    66
for NAME in hosts protocols services networks passwd group
50806
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    67
do
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    68
  rm "$TARGET/etc/$NAME"
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    69
done
c19dba2d7ffe more systematic makedist_cygwin;
wenzelm
parents:
diff changeset
    70
57048
7bd165c32e99 updated cygwin more thoroughly;
wenzelm
parents: 57027
diff changeset
    71
ln -s cygperl5_14.dll "$TARGET/bin/cygperl5_14_2.dll"
7bd165c32e99 updated cygwin more thoroughly;
wenzelm
parents: 57027
diff changeset
    72
50806
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
50958
af59600d8955 proper permissions;
wenzelm
parents: 50892
diff changeset
    80