lib/Tools/version
author wenzelm
Sat, 27 Mar 2021 18:03:50 +0100
changeset 73482 9830d7981ad0
parent 73481 92db3e31fae3
child 73483 804e75127f29
permissions -rwxr-xr-x
tuned;
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)"
73481
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    18
  echo "    -t           symbolic tags (derived from Mercurial id)"
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    19
  echo
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    20
  echo "  Display Isabelle version information."
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    21
  echo
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    22
  exit 1
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    23
}
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    24
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    25
function fail()
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    26
{
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    27
  echo "$1" >&2
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    28
  exit 2
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
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    32
## process command line
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    33
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    34
# options
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    35
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    36
SHORT_ID=""
73481
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    37
TAGS=""
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    38
73481
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    39
while getopts "it" OPT
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    40
do
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    41
  case "$OPT" in
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    42
    i)
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    43
      SHORT_ID=true
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    44
      ;;
73481
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    45
    t)
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    46
      TAGS=true
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    47
      ;;
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    48
    \?)
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    49
      usage
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    50
      ;;
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    51
  esac
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    52
done
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    53
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    54
shift $(($OPTIND - 1))
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
# args
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    58
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    59
[ "$#" -ne 0 ] && usage
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    60
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    61
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    62
## main
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    63
73481
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    64
if [ -z "$SHORT_ID" -a -z "$TAGS" ]; then
67866
11e4060bcdca clarified message;
wenzelm
parents: 67865
diff changeset
    65
  echo 'repository version'    # filled in automatically!
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    66
fi
73481
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    67
73482
wenzelm
parents: 73481
diff changeset
    68
HG_ARCHIVAL="$ISABELLE_HOME/.hg_archival.txt"
wenzelm
parents: 73481
diff changeset
    69
73481
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    70
if [ -n "$SHORT_ID" ]; then
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    71
  if [ -d "$ISABELLE_HOME/.hg" ]; then
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    72
    "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || exit "$?"
73482
wenzelm
parents: 73481
diff changeset
    73
  elif [ -f "$HG_ARCHIVAL" ]; then
wenzelm
parents: 73481
diff changeset
    74
    RESULT="$(fgrep node: < "$HG_ARCHIVAL" | cut -d " " -f2 | head -c12)"
73481
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    75
    [ -n "$RESULT" ] && echo "$RESULT"
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    76
  elif [ -n "$ISABELLE_ID" ]; then
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    77
    echo "$ISABELLE_ID"
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    78
  fi
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    79
fi
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    80
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    81
if [ -n "$TAGS" ]; then
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    82
  RESULT=""
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    83
  if [ -d "$ISABELLE_HOME/.hg" ]; then
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    84
    RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" id -t 2>/dev/null)
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    85
    RC="$?"
73482
wenzelm
parents: 73481
diff changeset
    86
  elif [ -f "$HG_ARCHIVAL" ]; then
wenzelm
parents: 73481
diff changeset
    87
    RESULT="$(fgrep tag: < "$HG_ARCHIVAL" | cut -d " " -f2)"
73481
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    88
    RC="$?"
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    89
  fi
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    90
  if [ "$RC" -ne 0 ]; then
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    91
    exit "$RC"
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    92
  elif [ -n "$RESULT" -a "$RESULT" != "tip" ]; then
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    93
    echo "$RESULT"
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    94
  fi
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    95
fi