From: Claudio Sacerdoti Coen Date: Thu, 31 Oct 2002 10:20:33 +0000 (+0000) Subject: New version of the library added. X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~6 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d63f384d57565bce1efbcf50b1c0b50f76397c85;p=helm.git New version of the library added. --- diff --git a/helm/scripts/init.d/etc_default_helm_mowgli b/helm/scripts/init.d/etc_default_helm_mowgli new file mode 100644 index 000000000..af0ac44a5 --- /dev/null +++ b/helm/scripts/init.d/etc_default_helm_mowgli @@ -0,0 +1,29 @@ +# Configuration for helm daemons + + # DAEMONS started/stopped/ecc. by /etc/init.d/helm, name listed here + # must correspond to scripts located in /etc/init.d +DAEMONS=" + helm-http-getter_mowgli + helm-proof-checker_mowgli + helm-uri-set-queue_mowgli + helm-draw-graph_mowgli +" + + # script used to define a good(TM) environment for daemons +ENVSCRIPT="/projects/helm/shared/scripts/phd_mowgli.rc" + + # script used to load/unload uwobo predefined scripts +UWOBO_INIT_SCRIPT="/projects/helm/shared/scripts/init.d/loadPredefinedStylesheets.pl" + + # http getter cache dirs that need to be created at boot time +HTTP_GETTER_CACHE_DIRS=" + /projects/helm/shared/cache/library + /projects/helm/shared/cache/library/http_getter_mowgli + /projects/helm/shared/cache/rdf_library + /projects/helm/shared/cache/rdf_library/http_getter_mowgli +" + + # user which will own the daemons and the cache directories +OWNER="sacerdot:helm" + +# vim: set ft=sh: diff --git a/helm/scripts/init.d/helm-bootmisc_mowgli.sh b/helm/scripts/init.d/helm-bootmisc_mowgli.sh new file mode 100755 index 000000000..41a2af838 --- /dev/null +++ b/helm/scripts/init.d/helm-bootmisc_mowgli.sh @@ -0,0 +1,19 @@ +#!/bin/sh + +HTTP_GETTER_CACHE_DIRS="" +if [ -f /etc/default/helm_mowgli ]; then + . /etc/default/helm_mowgli +fi + +# clean pid file for helm related daemons +( cd /projects/helm/run/ && rm -f *.pid ) + +# create http_getter cache dirs +for d in $HTTP_GETTER_CACHE_DIRS; do + if ! [ -d $d ]; then + mkdir -m 2775 $d + OWNER=`echo -n $OWNER | sed -e 's/:/./'` + chown $OWNER $d + fi +done + diff --git a/helm/scripts/init.d/helm-draw-graph_mowgli b/helm/scripts/init.d/helm-draw-graph_mowgli new file mode 100755 index 000000000..d1a08f9f6 --- /dev/null +++ b/helm/scripts/init.d/helm-draw-graph_mowgli @@ -0,0 +1,59 @@ +#!/bin/sh +# +# init.d script for HELM draw_graph.cgi +# +# by --Zack +# Created: Wed, 9 Oct 2002 11:12:01 +0200 +# Last-Modified: Wed, 9 Oct 2002 11:12:01 +0200 + +DAEMON=/projects/helm/graphs/tools/draw_graph.cgi +USAGE="Usage: /etc/init.d/helm-draw-graph_mowgli { start | stop | restart }" + +ENVSCRIPT="" +if [ -f /etc/default/helm_mowgli ]; then + . /etc/default/helm_mowgli +fi +if ! [ -f "$ENVSCRIPT" ]; then + echo "Can't find environment script '$ENVSCRIPT'" + exit 1 +fi +. $ENVSCRIPT &> /dev/null + +NAME=`basename $DAEMON` +PIDFILE=/projects/helm/run/$NAME.pid + +do_start () { + echo "Starting $DAEMON ..." + start-stop-daemon \ + --start --background --pidfile $PIDFILE --make-pidfile \ + --chuid $OWNER --exec $DAEMON +} + +do_stop () { + echo "Stopping $DAEMON ..." + start-stop-daemon --stop --pidfile $PIDFILE && \ + (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) +} + +case "$1" in + + start) + do_start + ;; + + stop) + do_stop + ;; + + restart) + do_stop + do_start + ;; + + *) + echo "$USAGE" >&2 + exit 1 + ;; + +esac + diff --git a/helm/scripts/init.d/helm-http-getter_mowgli b/helm/scripts/init.d/helm-http-getter_mowgli new file mode 100755 index 000000000..7eff55e32 --- /dev/null +++ b/helm/scripts/init.d/helm-http-getter_mowgli @@ -0,0 +1,59 @@ +#!/bin/sh +# +# init.d script for http_getter.pl +# +# by --Zack +# Created: Tue, 8 Oct 2002 17:18:17 +0200 +# Last-Modified: Wed, 9 Oct 2002 11:12:01 +0200 + +DAEMON=/projects/helm/http_getter/http_getter.pl +USAGE="Usage: /etc/init.d/helm-http-getter_mowgli { start | stop | restart }" + +ENVSCRIPT="" +if [ -f /etc/default/helm_mowgli ]; then + . /etc/default/helm_mowgli +fi +if ! [ -f "$ENVSCRIPT" ]; then + echo "Can't find environment script '$ENVSCRIPT'" + exit 1 +fi +. $ENVSCRIPT &> /dev/null + +NAME=`basename $DAEMON` +PIDFILE=/projects/helm/run/"$NAME"_mowgli.pid + +do_start () { + echo "Starting $DAEMON ..." + start-stop-daemon \ + --start --background --pidfile $PIDFILE --make-pidfile \ + --chuid $OWNER --exec $DAEMON +} + +do_stop () { + echo "Stopping $DAEMON ..." + start-stop-daemon --stop --pidfile $PIDFILE && \ + (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) +} + +case "$1" in + + start) + do_start + ;; + + stop) + do_stop + ;; + + restart) + do_stop + do_start + ;; + + *) + echo "$USAGE" >&2 + exit 1 + ;; + +esac + diff --git a/helm/scripts/init.d/helm-tomcat_mowgli b/helm/scripts/init.d/helm-tomcat_mowgli new file mode 100755 index 000000000..45f3c141e --- /dev/null +++ b/helm/scripts/init.d/helm-tomcat_mowgli @@ -0,0 +1,50 @@ +#!/bin/sh +# +# init.d script for HELM daemons +# +# by --Zack +# Created: Wed, 9 Oct 2002 14:26:27 +0200 +# Last-Modified: Wed, 9 Oct 2002 14:26:27 +0200 + +UWOBO_INIT_SCRIPT="" +ENVSCRIPT="" +if [ -f /etc/default/helm_mowgli ]; then + . /etc/default/helm_mowgli +fi +test -x "$UWOBO_INIT_SCRIPT" || exit 0 +if ! [ -f "$ENVSCRIPT" ]; then + echo "Can't find environment script '$ENVSCRIPT'" + exit 1 +fi +. $ENVSCRIPT &> /dev/null + +case "$1" in + + start) + echo -n "Loading UWOBO stylesheets (mowgli) ... " + $UWOBO_INIT_SCRIPT > /dev/null + echo "done!" + ;; + + stop) + $UWOBO_INIT_SCRIPT --unload > /dev/null + ;; + + reload) + $UWOBO_INIT_SCRIPT --reload > /dev/null + ;; + + restart) + $UWOBO_INIT_SCRIPT --unload > /dev/null + $UWOBO_INIT_SCRIPT > /dev/null + ;; + + *) + echo + echo "Usage: /etc/init.d/helm-tomcat_mowgli { start | stop | restart | reload }" >&2 + echo + exit 1 + ;; + +esac + diff --git a/helm/scripts/init.d/helm-uri-set-queue_mowgli b/helm/scripts/init.d/helm-uri-set-queue_mowgli new file mode 100755 index 000000000..36c195e1d --- /dev/null +++ b/helm/scripts/init.d/helm-uri-set-queue_mowgli @@ -0,0 +1,59 @@ +#!/bin/sh +# +# init.d script for HELM uri_set_queue.cgi +# +# by --Zack +# Created: Tue, 8 Oct 2002 17:18:17 +0200 +# Last-Modified: Wed, 9 Oct 2002 11:12:01 +0200 + +DAEMON=/projects/helm/graphs/tools/uri_set_queue.cgi +USAGE="Usage: /etc/init.d/helm-uri-set-queue_mowgli { start | stop | restart }" + +ENVSCRIPT="" +if [ -f /etc/default/helm_mowgli ]; then + . /etc/default/helm_mowgli +fi +if ! [ -f "$ENVSCRIPT" ]; then + echo "Can't find environment script '$ENVSCRIPT'" + exit 1 +fi +. $ENVSCRIPT &> /dev/null + +NAME=`basename $DAEMON` +PIDFILE=/projects/helm/run/$NAME.pid + +do_start () { + echo "Starting $DAEMON ..." + start-stop-daemon \ + --start --background --pidfile $PIDFILE --make-pidfile \ + --chuid $OWNER --exec $DAEMON +} + +do_stop () { + echo "Stopping $DAEMON ..." + start-stop-daemon --stop --pidfile $PIDFILE && \ + (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) +} + +case "$1" in + + start) + do_start + ;; + + stop) + do_stop + ;; + + restart) + do_stop + do_start + ;; + + *) + echo "$USAGE" >&2 + exit 1 + ;; + +esac + diff --git a/helm/scripts/init.d/helm_mowgli b/helm/scripts/init.d/helm_mowgli new file mode 100755 index 000000000..fe73ec0d7 --- /dev/null +++ b/helm/scripts/init.d/helm_mowgli @@ -0,0 +1,37 @@ +#!/bin/sh +# +# init.d script for HELM daemons +# +# by --Zack +# Created: Tue, 8 Oct 2002 17:18:17 +0200 +# Last-Modified: Tue, 8 Oct 2002 17:18:17 +0200 + +DAEMONS="" +if [ -f /etc/default/helm_mowgli ]; then + . /etc/default/helm_mowgli +fi + +case "$1" in + + start|stop|restart|force-reload|reload) + for d in $DAEMONS; do + /etc/init.d/$d $1 + done + ;; + + *) + echo + echo "Usage: /etc/init.d/helm { start | stop | restart | force-reload | reload }" >&2 + echo + if [ -z "$DAEMONS" ]; then + echo "Actually, no daemons are considered!" + else + echo "Actually, considered daemons are: $DAEMONS" + fi + echo "to change this setting see /etc/default/helm" + echo + exit 1 + ;; + +esac + diff --git a/helm/scripts/template.cshrc b/helm/scripts/template.cshrc index 3fa77db4d..257d95d78 100644 --- a/helm/scripts/template.cshrc +++ b/helm/scripts/template.cshrc @@ -52,16 +52,18 @@ setenv HTTP_GETTER_XSLT_INDEXNAME xslt_index.txt setenv HELM_ANNOTATIONS_DIR pippo setenv HELM_ANNOTATIONS_URL pippo setenv UWOBO_PORT 8081 -setenv URI_SET_QUEUE_PORT 48082 -setenv DRAW_GRAPH_PORT 48083 setenv UWOBO_PANEL_CONF /projects/helm/public_html/uwobo/panel/control.html if ($COQV == V7) then + setenv URI_SET_QUEUE_PORT 48082 + setenv DRAW_GRAPH_PORT 48083 setenv PROOF_CHECKER_PORT 48084 setenv HTTP_GETTER_PORT 48081 setenv HELM_UWOBO_URL http://mowgli.cs.unibo.it:$UWOBO_PORT/helm/servlet/uwobo/ setenv HTTP_GETTER_DTD_BASE_URL http://www.cs.unibo.it/helm/dtd else # V7_mowgli + setenv URI_SET_QUEUE_PORT 58082 + setenv DRAW_GRAPH_PORT 58083 setenv PROOF_CHECKER_PORT 58084 setenv HTTP_GETTER_PORT 58081 setenv HELM_UWOBO_URL http://mowgli.cs.unibo.it:$UWOBO_PORT/mowgli/servlet/uwobo/ diff --git a/helm/scripts/template.rc b/helm/scripts/template.rc index caae152b4..ed6c78c95 100644 --- a/helm/scripts/template.rc +++ b/helm/scripts/template.rc @@ -44,16 +44,18 @@ export HTTP_GETTER_XSLT_INDEXNAME=xslt_index.txt export HELM_ANNOTATIONS_DIR=pippo export HELM_ANNOTATIONS_URL=pippo export UWOBO_PORT=8081 -export URI_SET_QUEUE_PORT=48082 -export DRAW_GRAPH_PORT=48083 export UWOBO_PANEL_CONF=/projects/helm/public_html/uwobo/panel/control.html if test $COQV = V7; then + export URI_SET_QUEUE_PORT=48082 + export DRAW_GRAPH_PORT=48083 export PROOF_CHECKER_PORT=48084 export HTTP_GETTER_PORT=48081 export HELM_UWOBO_URL=http://mowgli.cs.unibo.it:$UWOBO_PORT/helm/servlet/uwobo/ export HTTP_GETTER_DTD_BASE_URL=http://www.cs.unibo.it/helm/dtd else # V7_mowgli + export URI_SET_QUEUE_PORT=58082 + export DRAW_GRAPH_PORT=58083 export PROOF_CHECKER_PORT=58084 export HTTP_GETTER_PORT=58081 export HELM_UWOBO_URL=http://mowgli.cs.unibo.it:$UWOBO_PORT/mowgli/servlet/uwobo/