lib/Tools/install
author blanchet
Sun, 21 May 2017 21:37:31 +0200
changeset 65885 77d922eff5ac
parent 63995 2e4d80723fb0
child 79059 ae682b2aab03
permissions -rwxr-xr-x
added one more simplification to help replay
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
#
9788
wenzelm
parents: 7934
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     4
#
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
     5
# DESCRIPTION: install standalone Isabelle executables
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     6
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     7
9788
wenzelm
parents: 7934
diff changeset
     8
PRG=$(basename "$0")
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     9
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    10
function usage()
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    11
{
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    12
  echo
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    13
  echo "Usage: isabelle $PRG [OPTIONS] BINDIR"
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    14
  echo
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    15
  echo "  Options are:"
7887
eedfff88ee40 tuned usage;
wenzelm
parents: 6545
diff changeset
    16
  echo "    -d DISTDIR   refer to DISTDIR as Isabelle distribution"
eedfff88ee40 tuned usage;
wenzelm
parents: 6545
diff changeset
    17
  echo "                 (default ISABELLE_HOME)"
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    18
  echo
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    19
  echo "  Install Isabelle executables with absolute references to the"
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    20
  echo "  distribution directory."
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    21
  echo
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    22
  exit 1
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    23
}
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    24
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    25
function fail()
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
  echo "$1" >&2
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    28
  exit 2
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    29
}
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    30
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    31
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    32
## process command line
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    33
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    34
# options
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    35
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    36
DISTDIR="$ISABELLE_HOME"
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    37
BINDIR=""
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    38
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    39
while getopts "d:" OPT
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    40
do
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    41
  case "$OPT" in
5404
wenzelm
parents: 5403
diff changeset
    42
    d)
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    43
      DISTDIR="$OPTARG"
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    44
      ;;
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    45
    \?)
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    46
      usage
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    47
      ;;
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    48
  esac
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    49
done
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    50
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    51
shift $(($OPTIND - 1))
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    52
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    53
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    54
# args
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    55
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    56
[ "$#" -ge 1 ] && { BINDIR="$1"; shift; }
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    57
[ "$#" -ne 0 -o -z "$BINDIR" ] && usage
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    58
15848
3001067227af restored AUTO_BASH/PERL -- beware of ./configure!
wenzelm
parents: 15733
diff changeset
    59
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    60
## main
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    61
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    62
echo "referring to distribution at \"$DISTDIR\""
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    63
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    64
mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\""
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    65
63995
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 62588
diff changeset
    66
for NAME in isabelle isabelle_java isabelle_scala_script
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    67
do
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    68
  BIN="$BINDIR/$NAME"
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    69
  DIST="$DISTDIR/bin/$NAME"
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    70
  echo "installing $BIN"
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    71
  rm -f "$BIN"
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    72
  echo "#!/usr/bin/env bash" > "$BIN" || fail "Cannot write file: $BIN"
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    73
  echo >> "$BIN"
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    74
  echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    75
  chmod +x "$BIN"
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 29143
diff changeset
    76
done