lib/Tools/install
author wenzelm
Mon, 20 Nov 2006 23:47:10 +0100
changeset 21426 87ac12bed1ab
parent 16653 c12c2f411f77
child 26577 50f47cc2af72
permissions -rwxr-xr-x
converted legacy ML scripts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10504
diff changeset
     1
#!/usr/bin/env bash
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     2
#
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     3
# $Id$
9788
wenzelm
parents: 7934
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     5
#
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
     6
# DESCRIPTION: install standalone Isabelle executables
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     7
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     8
9788
wenzelm
parents: 7934
diff changeset
     9
PRG=$(basename "$0")
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    10
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    11
function usage()
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    12
{
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    13
  echo
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    14
  echo "Usage: $PRG [OPTIONS]"
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    15
  echo
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    16
  echo "  Options are:"
7887
eedfff88ee40 tuned usage;
wenzelm
parents: 6545
diff changeset
    17
  echo "    -d DISTDIR   refer to DISTDIR as Isabelle distribution"
eedfff88ee40 tuned usage;
wenzelm
parents: 6545
diff changeset
    18
  echo "                 (default ISABELLE_HOME)"
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    19
  echo "    -p DIR       install standalone binaries in DIR"
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    20
  echo
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    21
  echo "  Install Isabelle executables with absolute references to the current"
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    22
  echo "  distribution directory."
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    23
  echo
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    24
  exit 1
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    25
}
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    26
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    27
function fail()
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    28
{
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    29
  echo "$1" >&2
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    30
  exit 2
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    31
}
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    32
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    33
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    34
## process command line
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    35
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    36
# options
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    37
6450
990e6e2dee26 improved usage;
wenzelm
parents: 6417
diff changeset
    38
NO_OPTS=true
990e6e2dee26 improved usage;
wenzelm
parents: 6417
diff changeset
    39
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    40
DISTDIR="$ISABELLE_HOME"
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    41
BINDIR=""
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    42
16653
c12c2f411f77 isatool install: removed KDE option;
wenzelm
parents: 15856
diff changeset
    43
while getopts "d:p:" OPT
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    44
do
15856
674ff97ce0ef removed -a option;
wenzelm
parents: 15848
diff changeset
    45
  NO_OPTS=""
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    46
  case "$OPT" in
5404
wenzelm
parents: 5403
diff changeset
    47
    d)
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    48
      DISTDIR="$OPTARG"
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    49
      ;;
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    50
    p)
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    51
      BINDIR="$OPTARG"
15733
75b9219980d3 Add RDISTDIR option used by Isabelle RPM.
aspinall
parents: 15574
diff changeset
    52
      ;;
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    53
    \?)
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    54
      usage
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    55
      ;;
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    56
  esac
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    57
done
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    58
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    59
shift $(($OPTIND - 1))
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    60
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    61
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    62
# args
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    63
9788
wenzelm
parents: 7934
diff changeset
    64
[ "$#" -ne 0 -o -n "$NO_OPTS" ] && usage
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    65
15848
3001067227af restored AUTO_BASH/PERL -- beware of ./configure!
wenzelm
parents: 15733
diff changeset
    66
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    67
## main
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    68
6459
1d13a86bfa6c fixed ISABELLE_HOME/lib/logo/isabelle-tiny.xpm;
wenzelm
parents: 6450
diff changeset
    69
echo "referring to distribution at $DISTDIR"
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    70
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    71
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    72
# standalone binaries
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    73
6082
590f9e3bf4d8 configure AUTO_BASH, AUTO_PERL;
wenzelm
parents: 5404
diff changeset
    74
#set by configure
15848
3001067227af restored AUTO_BASH/PERL -- beware of ./configure!
wenzelm
parents: 15733
diff changeset
    75
AUTO_BASH=bash
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10504
diff changeset
    76
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10504
diff changeset
    77
case "$AUTO_BASH" in
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10504
diff changeset
    78
  /*)
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10504
diff changeset
    79
    BASH="$AUTO_BASH"
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10504
diff changeset
    80
    ;;
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10504
diff changeset
    81
  *)
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10504
diff changeset
    82
    BASH="/usr/bin/env bash"
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10504
diff changeset
    83
    ;;
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10504
diff changeset
    84
esac
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    85
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    86
if [ -n "$BINDIR" ]; then
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    87
  mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    88
11550
915c5de6480f smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents: 11127
diff changeset
    89
  for NAME in isatool isabelle-process isabelle-interface
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    90
  do
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    91
    BIN="$BINDIR/$NAME"
15856
674ff97ce0ef removed -a option;
wenzelm
parents: 15848
diff changeset
    92
    DIST="$DISTDIR/bin/$NAME"
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    93
    echo "installing $BIN"
15848
3001067227af restored AUTO_BASH/PERL -- beware of ./configure!
wenzelm
parents: 15733
diff changeset
    94
    rm -f "$BIN"
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10504
diff changeset
    95
    echo "#!$BASH" > "$BIN" || fail "Cannot write file: $BIN"
9788
wenzelm
parents: 7934
diff changeset
    96
    echo >> "$BIN"
wenzelm
parents: 7934
diff changeset
    97
    echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
wenzelm
parents: 7934
diff changeset
    98
    chmod +x "$BIN"
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    99
  done
11550
915c5de6480f smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents: 11127
diff changeset
   100
  for NAME in Isabelle isabelle
915c5de6480f smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents: 11127
diff changeset
   101
  do
915c5de6480f smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents: 11127
diff changeset
   102
    BIN="$BINDIR/$NAME"
915c5de6480f smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents: 11127
diff changeset
   103
    echo "installing $BIN"
15848
3001067227af restored AUTO_BASH/PERL -- beware of ./configure!
wenzelm
parents: 15733
diff changeset
   104
    rm -f "$BIN"
15856
674ff97ce0ef removed -a option;
wenzelm
parents: 15848
diff changeset
   105
    cp "$ISABELLE_HOME/bin/$NAME" "$BIN" || fail "Cannot write file: $BIN"
11550
915c5de6480f smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents: 11127
diff changeset
   106
    chmod +x "$BIN"
915c5de6480f smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents: 11127
diff changeset
   107
  done
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
   108
fi