author | paulson <lp15@cam.ac.uk> |
Sun, 12 Feb 2023 20:49:31 +0000 | |
changeset 77234 | 61fba09a3456 |
parent 73523 | 2cd23d587db9 |
permissions | -rwxr-xr-x |
13804 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
3 |
# Author: Stefan Berghofer, TU Muenchen |
|
41511 | 4 |
# Author: Makarius |
13804 | 5 |
# |
6 |
# DESCRIPTION: display Isabelle version |
|
7 |
||
41511 | 8 |
|
9 |
PRG="$(basename "$0")" |
|
10 |
||
11 |
function usage() |
|
12 |
{ |
|
13 |
echo |
|
14 |
echo "Usage: isabelle $PRG [OPTIONS]" |
|
15 |
echo |
|
16 |
echo " Options are:" |
|
17 |
echo " -i short identification (derived from Mercurial id)" |
|
73481 | 18 |
echo " -t symbolic tags (derived from Mercurial id)" |
41511 | 19 |
echo |
20 |
echo " Display Isabelle version information." |
|
21 |
echo |
|
22 |
exit 1 |
|
23 |
} |
|
24 |
||
25 |
function fail() |
|
26 |
{ |
|
27 |
echo "$1" >&2 |
|
28 |
exit 2 |
|
29 |
} |
|
30 |
||
31 |
||
32 |
## process command line |
|
33 |
||
34 |
# options |
|
35 |
||
36 |
SHORT_ID="" |
|
73481 | 37 |
TAGS="" |
41511 | 38 |
|
73481 | 39 |
while getopts "it" OPT |
41511 | 40 |
do |
41 |
case "$OPT" in |
|
42 |
i) |
|
43 |
SHORT_ID=true |
|
44 |
;; |
|
73481 | 45 |
t) |
46 |
TAGS=true |
|
47 |
;; |
|
41511 | 48 |
\?) |
49 |
usage |
|
50 |
;; |
|
51 |
esac |
|
52 |
done |
|
53 |
||
54 |
shift $(($OPTIND - 1)) |
|
55 |
||
56 |
||
57 |
# args |
|
58 |
||
59 |
[ "$#" -ne 0 ] && usage |
|
60 |
||
61 |
||
62 |
## main |
|
63 |
||
73481 | 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 | 66 |
fi |
73481 | 67 |
|
73482 | 68 |
HG_ARCHIVAL="$ISABELLE_HOME/.hg_archival.txt" |
69 |
||
73483 | 70 |
export LANG=C |
71 |
export HGPLAIN= |
|
72 |
||
73481 | 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 | 75 |
RESULT="$(cat "$ISABELLE_HOME/etc/ISABELLE_ID")" |
76 |
RC="$?" |
|
77 |
elif [ -d "$ISABELLE_HOME/.hg" ]; then |
|
78 |
RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null) |
|
79 |
RC="$?" |
|
73482 | 80 |
elif [ -f "$HG_ARCHIVAL" ]; then |
73509 | 81 |
RESULT="$(grep "^node:" < "$HG_ARCHIVAL" | cut -d " " -f2 | head -c12)" |
73521 | 82 |
RC="$?" |
83 |
else |
|
84 |
RESULT="" |
|
85 |
RC="0" |
|
86 |
fi |
|
87 |
if [ "$RC" -ne 0 ]; then |
|
88 |
exit "$RC" |
|
89 |
elif [ -n "$RESULT" ]; then |
|
90 |
echo "$RESULT" |
|
73481 | 91 |
fi |
92 |
fi |
|
93 |
||
94 |
if [ -n "$TAGS" ]; then |
|
73521 | 95 |
if [ -f "$ISABELLE_HOME/etc/ISABELLE_TAGS" ]; then |
96 |
RESULT="$(cat "$ISABELLE_HOME/etc/ISABELLE_TAGS")" |
|
97 |
RC="$?" |
|
98 |
elif [ -d "$ISABELLE_HOME/.hg" ]; then |
|
73481 | 99 |
RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" id -t 2>/dev/null) |
100 |
RC="$?" |
|
73482 | 101 |
elif [ -f "$HG_ARCHIVAL" ]; then |
73509 | 102 |
RESULT="$(grep "^tag:" < "$HG_ARCHIVAL" | cut -d " " -f2)" |
73481 | 103 |
RC="$?" |
73521 | 104 |
else |
105 |
RESULT="" |
|
106 |
RC="0" |
|
73481 | 107 |
fi |
108 |
if [ "$RC" -ne 0 ]; then |
|
109 |
exit "$RC" |
|
110 |
elif [ -n "$RESULT" -a "$RESULT" != "tip" ]; then |
|
111 |
echo "$RESULT" |
|
112 |
fi |
|
113 |
fi |