# HG changeset patch # User wenzelm # Date 1292854755 -3600 # Node ID 9e576ec5c0dcbd8f8bb2ea91deb9f38555e7fdb9 # Parent bb8468ae414eb737cee62e5bd90fcf32d6440acf tuned/clarified some component settings; explicit comments about common mistakes; diff -r bb8468ae414e -r 9e576ec5c0dc src/HOL/Library/Sum_Of_Squares/etc/settings --- a/src/HOL/Library/Sum_Of_Squares/etc/settings Mon Dec 20 14:44:00 2010 +0100 +++ b/src/HOL/Library/Sum_Of_Squares/etc/settings Mon Dec 20 15:19:15 2010 +0100 @@ -1,1 +1,3 @@ +# -*- shell-script -*- :mode=shellscript: + ISABELLE_SUM_OF_SQUARES="$COMPONENT" diff -r bb8468ae414e -r 9e576ec5c0dc src/HOL/Mirabelle/etc/settings --- a/src/HOL/Mirabelle/etc/settings Mon Dec 20 14:44:00 2010 +0100 +++ b/src/HOL/Mirabelle/etc/settings Mon Dec 20 15:19:15 2010 +0100 @@ -1,3 +1,5 @@ +# -*- shell-script -*- :mode=shellscript: + MIRABELLE_HOME="$COMPONENT" MIRABELLE_LOGIC=HOL @@ -5,4 +7,4 @@ MIRABELLE_OUTPUT_PATH=/tmp/mirabelle MIRABELLE_TIMEOUT=30 -ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools" +ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools" diff -r bb8468ae414e -r 9e576ec5c0dc src/HOL/Mutabelle/etc/settings --- a/src/HOL/Mutabelle/etc/settings Mon Dec 20 14:44:00 2010 +0100 +++ b/src/HOL/Mutabelle/etc/settings Mon Dec 20 15:19:15 2010 +0100 @@ -1,7 +1,9 @@ +# -*- shell-script -*- :mode=shellscript: + MUTABELLE_HOME="$COMPONENT" DEFAULT_MUTABELLE_LOGIC=HOL DEFAULT_MUTABELLE_IMPORT_THEORY=Complex_Main DEFAULT_MUTABELLE_OUTPUT_PATH=/tmp/mutabelle -ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools" +ISABELLE_TOOLS="$ISABELLE_TOOLS:$MUTABELLE_HOME/lib/Tools" diff -r bb8468ae414e -r 9e576ec5c0dc src/HOL/Tools/ATP/etc/settings --- a/src/HOL/Tools/ATP/etc/settings Mon Dec 20 14:44:00 2010 +0100 +++ b/src/HOL/Tools/ATP/etc/settings Mon Dec 20 15:19:15 2010 +0100 @@ -1,1 +1,3 @@ +# -*- shell-script -*- :mode=shellscript: + ISABELLE_ATP="$COMPONENT" diff -r bb8468ae414e -r 9e576ec5c0dc src/HOL/Tools/Predicate_Compile/etc/settings --- a/src/HOL/Tools/Predicate_Compile/etc/settings Mon Dec 20 14:44:00 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/etc/settings Mon Dec 20 15:19:15 2010 +0100 @@ -1,5 +1,8 @@ # -*- shell-script -*- :mode=shellscript: +# FIXME contrib_devel not official +# FIXME $(type -p swipl) etc. does not allow spaces in file name + EXEC_SWIPL="$(choosefrom \ "$ISABELLE_HOME/contrib/swipl/$ISABELLE_PLATFORM/bin/swipl" \ "$ISABELLE_HOME/contrib_devel/swipl/$ISABELLE_PLATFORM/bin/swipl" \ diff -r bb8468ae414e -r 9e576ec5c0dc src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version --- a/src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version Mon Dec 20 14:44:00 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version Mon Dec 20 15:19:15 2010 +0100 @@ -7,6 +7,9 @@ if [ "$EXEC_SWIPL" = "" ]; then echo "" else + # FIXME does not allow spaces in $EXEC_SWIPL + # FIXME "expr match" not portable + # FIXME prefer $(...) in bash VERSION=`$EXEC_SWIPL --version` echo `expr match "$VERSION" 'SWI-Prolog version \([0-9\.]*\)'` fi diff -r bb8468ae414e -r 9e576ec5c0dc src/HOL/Tools/SMT/etc/settings --- a/src/HOL/Tools/SMT/etc/settings Mon Dec 20 14:44:00 2010 +0100 +++ b/src/HOL/Tools/SMT/etc/settings Mon Dec 20 15:19:15 2010 +0100 @@ -1,3 +1,5 @@ +# -*- shell-script -*- :mode=shellscript: + ISABELLE_SMT="$COMPONENT" REMOTE_SMT="$ISABELLE_SMT/lib/scripts/remote_smt" diff -r bb8468ae414e -r 9e576ec5c0dc src/Tools/WWW_Find/etc/settings --- a/src/Tools/WWW_Find/etc/settings Mon Dec 20 14:44:00 2010 +0100 +++ b/src/Tools/WWW_Find/etc/settings Mon Dec 20 15:19:15 2010 +0100 @@ -1,7 +1,8 @@ -# the path to lighttpd +# -*- shell-script -*- :mode=shellscript: + LIGHTTPD="/usr/sbin/lighttpd" -ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools" - WWWFINDDIR="$COMPONENT" WWWCONFIG="$WWWFINDDIR/lighttpd.conf" + +ISABELLE_TOOLS="$ISABELLE_TOOLS:$WWWFINDDIR/lib/Tools"