lib/Tools/version
author wenzelm
Wed, 31 Mar 2021 11:24:46 +0200
changeset 73772 d3f2038198ae
parent 73764 5d750df8e894
child 73776 4cba4e250c28
permissions -rwxr-xr-x
clarified (again): local tip could be actually more recent;
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)"
73736
92db3e31fae3 clarified output;
wenzelm
parents: 73735
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=""
73736
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    37
TAGS=""
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    38
73736
92db3e31fae3 clarified output;
wenzelm
parents: 73735
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
      ;;
73736
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    45
    t)
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    46
      TAGS=true
92db3e31fae3 clarified output;
wenzelm
parents: 73735
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
73736
92db3e31fae3 clarified output;
wenzelm
parents: 73735
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
73736
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    67
73737
wenzelm
parents: 73736
diff changeset
    68
HG_ARCHIVAL="$ISABELLE_HOME/.hg_archival.txt"
wenzelm
parents: 73736
diff changeset
    69
73738
804e75127f29 more robust invocation of hg;
wenzelm
parents: 73737
diff changeset
    70
export LANG=C
804e75127f29 more robust invocation of hg;
wenzelm
parents: 73737
diff changeset
    71
export HGPLAIN=
804e75127f29 more robust invocation of hg;
wenzelm
parents: 73737
diff changeset
    72
73736
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    73
if [ -n "$SHORT_ID" ]; then
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    74
  if [ -d "$ISABELLE_HOME/.hg" ]; then
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    75
    "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || exit "$?"
73737
wenzelm
parents: 73736
diff changeset
    76
  elif [ -f "$HG_ARCHIVAL" ]; then
73764
5d750df8e894 more robust;
wenzelm
parents: 73738
diff changeset
    77
    RESULT="$(grep "^node:" < "$HG_ARCHIVAL" | cut -d " " -f2 | head -c12)"
73736
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    78
    [ -n "$RESULT" ] && echo "$RESULT"
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    79
  elif [ -n "$ISABELLE_ID" ]; then
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    80
    echo "$ISABELLE_ID"
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    81
  fi
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    82
fi
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    83
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    84
if [ -n "$TAGS" ]; then
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    85
  RESULT=""
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    86
  if [ -d "$ISABELLE_HOME/.hg" ]; then
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    87
    RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" id -t 2>/dev/null)
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    88
    RC="$?"
73737
wenzelm
parents: 73736
diff changeset
    89
  elif [ -f "$HG_ARCHIVAL" ]; then
73764
5d750df8e894 more robust;
wenzelm
parents: 73738
diff changeset
    90
    RESULT="$(grep "^tag:" < "$HG_ARCHIVAL" | cut -d " " -f2)"
73736
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    91
    RC="$?"
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    92
  fi
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    93
  if [ "$RC" -ne 0 ]; then
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    94
    exit "$RC"
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    95
  elif [ -n "$RESULT" -a "$RESULT" != "tip" ]; then
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    96
    echo "$RESULT"
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    97
  fi
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
    98
fi