1 #!/usr/bin/env bash |
|
2 # |
|
3 # Author: Timothy Bourke, NICTA |
|
4 # Based on scripts by Makarius Wenzel, TU Muenchen |
|
5 # |
|
6 # DESCRIPTION: run find theorems web server |
|
7 |
|
8 PRG=$(basename "$0") |
|
9 |
|
10 function usage() |
|
11 { |
|
12 echo |
|
13 echo "Usage: $ISABELLE_TOOL $PRG [Command] [Options] [HEAP]" |
|
14 echo |
|
15 echo " Command must be one of:" |
|
16 echo " start start lighttpd and isabelle" |
|
17 echo " stop stop lighttpd and isabelle" |
|
18 echo " status show www and scgi port statuses" |
|
19 echo |
|
20 echo " Options are:" |
|
21 echo " -l make log file" |
|
22 echo " -c specify lighttpd config file" |
|
23 echo " (default: $WWWCONFIG)" |
|
24 echo |
|
25 echo " Provide a web interface to find_theorems against the given HEAP" |
|
26 echo |
|
27 exit 1 |
|
28 } |
|
29 |
|
30 function fail() |
|
31 { |
|
32 echo "$1" >&2 |
|
33 exit 2 |
|
34 } |
|
35 |
|
36 function checkplatform() |
|
37 { |
|
38 case "$ISABELLE_PLATFORM" in |
|
39 *-linux) |
|
40 ;; |
|
41 *) |
|
42 fail "Platform $ISABELLE_PLATFORM currently not supported by $PRG component" |
|
43 ;; |
|
44 esac |
|
45 } |
|
46 |
|
47 function kill_by_port () { |
|
48 IPADDR='[0-9]*\.[0-9]*\.[0-9]*\.[0-9]*' |
|
49 PID=$(netstat -nltp 2>/dev/null \ |
|
50 | sed -ne "s#^.*${IPADDR}:$1 *${IPADDR}:.*LISTEN *\([0-9]*\)/.*#\1#p") |
|
51 if [ "$PID" != "" ]; then |
|
52 kill -9 $PID |
|
53 fi |
|
54 } |
|
55 |
|
56 function show_socket_status () { |
|
57 netstat -latp 2>/dev/null | grep ":$1 " |
|
58 } |
|
59 |
|
60 ## platform support check |
|
61 |
|
62 checkplatform |
|
63 |
|
64 ## process command line |
|
65 |
|
66 case "$1" in |
|
67 start|stop|status) |
|
68 COMMAND="$1" |
|
69 ;; |
|
70 *) |
|
71 usage |
|
72 ;; |
|
73 esac |
|
74 |
|
75 shift |
|
76 |
|
77 # options |
|
78 |
|
79 NO_OPTS=true |
|
80 LOGFILE=false |
|
81 |
|
82 while getopts "lc:" OPT |
|
83 do |
|
84 NO_OPTS="" |
|
85 case "$OPT" in |
|
86 l) |
|
87 LOGFILE=true |
|
88 ;; |
|
89 c) |
|
90 USER_CONFIG="$OPTARG" |
|
91 ;; |
|
92 \?) |
|
93 usage |
|
94 ;; |
|
95 esac |
|
96 done |
|
97 |
|
98 shift $(($OPTIND - 1)) |
|
99 |
|
100 # args |
|
101 |
|
102 INPUT="" |
|
103 |
|
104 if [ "$#" -ge 1 ]; then |
|
105 INPUT="$1" |
|
106 shift |
|
107 fi |
|
108 |
|
109 [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC" |
|
110 |
|
111 [ -x "$LIGHTTPD" ] || fail "lighttpd not found at $LIGHTTPD" |
|
112 |
|
113 if [ -n "$USER_CONFIG" ]; then |
|
114 WWWCONFIG="$USER_CONFIG" |
|
115 else |
|
116 TMP=$(mktemp "/tmp/lighttpd.conf.$$.XXX") |
|
117 echo "server.document-root = \"$WWWFINDDIR/www\"" > "$TMP" |
|
118 cat "$WWWCONFIG" >> "$TMP" |
|
119 WWWCONFIG="$TMP" |
|
120 fi |
|
121 |
|
122 |
|
123 ## main |
|
124 |
|
125 WWWPORT=`sed -e 's/[ ]*//g' -ne 's/server.port=\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"` |
|
126 SCGIPORT=`sed -e 's/[ ]*//g' -ne 's/"port"=>\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"` |
|
127 |
|
128 # inform theory which SCGI port to use via environment variable |
|
129 export SCGIPORT |
|
130 MLSTARTSERVER="use_thy \"Start_WWW_Find\";" |
|
131 |
|
132 case "$COMMAND" in |
|
133 start) |
|
134 "$LIGHTTPD" -f "$WWWCONFIG" |
|
135 if [ "$LOGFILE" = true ]; then |
|
136 (cd "$WWWFINDDIR"; \ |
|
137 nohup "$ISABELLE_PROCESS" -r -o show_question_marks=false -e "$MLSTARTSERVER" "$INPUT") & |
|
138 else |
|
139 (cd "$WWWFINDDIR"; \ |
|
140 nohup "$ISABELLE_PROCESS" -r -o show_question_marks=false -e "$MLSTARTSERVER" \ |
|
141 "$INPUT" > /dev/null 2> /dev/null) & |
|
142 fi |
|
143 ;; |
|
144 stop) |
|
145 kill_by_port $SCGIPORT |
|
146 kill_by_port $WWWPORT |
|
147 ;; |
|
148 status) |
|
149 show_socket_status $WWWPORT |
|
150 show_socket_status $SCGIPORT |
|
151 ;; |
|
152 esac |
|
153 |
|