lib/Tools/version
author wenzelm
Tue, 05 Nov 2019 14:28:00 +0100
changeset 71047 87c132cf5860
parent 67872 39b27d38a54c
child 73480 0e880b793db1
permissions -rwxr-xr-x
more options;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13804
d643300e4fc0 New tool for displaying version information.
berghofe
parents:
diff changeset
     1
#!/usr/bin/env bash
d643300e4fc0 New tool for displaying version information.
berghofe
parents:
diff changeset
     2
#
d643300e4fc0 New tool for displaying version information.
berghofe
parents:
diff changeset
     3
# Author: Stefan Berghofer, TU Muenchen
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
     4
# Author: Makarius
13804
d643300e4fc0 New tool for displaying version information.
berghofe
parents:
diff changeset
     5
#
d643300e4fc0 New tool for displaying version information.
berghofe
parents:
diff changeset
     6
# DESCRIPTION: display Isabelle version
d643300e4fc0 New tool for displaying version information.
berghofe
parents:
diff changeset
     7
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
     8
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
     9
PRG="$(basename "$0")"
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    10
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    11
function usage()
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    12
{
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    13
  echo
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    14
  echo "Usage: isabelle $PRG [OPTIONS]"
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    15
  echo
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    16
  echo "  Options are:"
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    17
  echo "    -i           short identification (derived from Mercurial id)"
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    18
  echo
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    19
  echo "  Display Isabelle version information."
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    20
  echo
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    21
  exit 1
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    22
}
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    23
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    24
function fail()
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    25
{
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    26
  echo "$1" >&2
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    27
  exit 2
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    28
}
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    29
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    30
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    31
## process command line
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    32
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    33
# options
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    34
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    35
SHORT_ID=""
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    36
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    37
while getopts "i" OPT
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    38
do
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    39
  case "$OPT" in
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    40
    i)
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    41
      SHORT_ID=true
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    42
      ;;
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    43
    \?)
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    44
      usage
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    45
      ;;
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    46
  esac
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    47
done
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    48
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    49
shift $(($OPTIND - 1))
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    50
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    51
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    52
# args
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    53
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    54
[ "$#" -ne 0 ] && usage
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    55
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    56
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    57
## main
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    58
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    59
if [ -n "$SHORT_ID" ]; then
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    60
  if [ -n "$ISABELLE_ID" ]; then
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    61
    echo "$ISABELLE_ID"
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    62
  else
67872
39b27d38a54c more accurate isabelle_id: parent directory is not necessarily at tip;
wenzelm
parents: 67866
diff changeset
    63
    "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || echo undefined
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    64
  fi
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    65
else
67866
11e4060bcdca clarified message;
wenzelm
parents: 67865
diff changeset
    66
  echo 'repository version'    # filled in automatically!
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    67
fi