lib/Tools/version
author paulson <lp15@cam.ac.uk>
Sun, 12 Feb 2023 20:49:31 +0000
changeset 77234 61fba09a3456
parent 73523 2cd23d587db9
permissions -rwxr-xr-x
Simplification of proofs
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
73523
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73521
diff changeset
    65
  echo "$ISABELLE_NAME"
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
73483
804e75127f29 more robust invocation of hg;
wenzelm
parents: 73482
diff changeset
    70
export LANG=C
804e75127f29 more robust invocation of hg;
wenzelm
parents: 73482
diff changeset
    71
export HGPLAIN=
804e75127f29 more robust invocation of hg;
wenzelm
parents: 73482
diff changeset
    72
73481
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    73
if [ -n "$SHORT_ID" ]; then
73520
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73509
diff changeset
    74
  if [ -f "$ISABELLE_HOME/etc/ISABELLE_ID" ]; then
73521
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    75
    RESULT="$(cat "$ISABELLE_HOME/etc/ISABELLE_ID")"
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    76
    RC="$?"
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    77
  elif [ -d "$ISABELLE_HOME/.hg" ]; then
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    78
    RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null)
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    79
    RC="$?"
73482
wenzelm
parents: 73481
diff changeset
    80
  elif [ -f "$HG_ARCHIVAL" ]; then
73509
5d750df8e894 more robust;
wenzelm
parents: 73483
diff changeset
    81
    RESULT="$(grep "^node:" < "$HG_ARCHIVAL" | cut -d " " -f2 | head -c12)"
73521
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    82
    RC="$?"
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    83
  else
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    84
    RESULT=""
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    85
    RC="0"
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    86
  fi
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    87
  if [ "$RC" -ne 0 ]; then
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    88
    exit "$RC"
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    89
  elif [ -n "$RESULT" ]; then
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    90
    echo "$RESULT"
73481
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    91
  fi
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    92
fi
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    93
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    94
if [ -n "$TAGS" ]; then
73521
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    95
  if [ -f "$ISABELLE_HOME/etc/ISABELLE_TAGS" ]; then
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    96
    RESULT="$(cat "$ISABELLE_HOME/etc/ISABELLE_TAGS")"
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    97
    RC="$?"
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
    98
  elif [ -d "$ISABELLE_HOME/.hg" ]; then
73481
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
    99
    RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" id -t 2>/dev/null)
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
   100
    RC="$?"
73482
wenzelm
parents: 73481
diff changeset
   101
  elif [ -f "$HG_ARCHIVAL" ]; then
73509
5d750df8e894 more robust;
wenzelm
parents: 73483
diff changeset
   102
    RESULT="$(grep "^tag:" < "$HG_ARCHIVAL" | cut -d " " -f2)"
73481
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
   103
    RC="$?"
73521
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
   104
  else
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
   105
    RESULT=""
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73520
diff changeset
   106
    RC="0"
73481
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
   107
  fi
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
   108
  if [ "$RC" -ne 0 ]; then
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
   109
    exit "$RC"
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
   110
  elif [ -n "$RESULT" -a "$RESULT" != "tip" ]; then
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
   111
    echo "$RESULT"
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
   112
  fi
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
   113
fi