lib/scripts/getsettings
author wenzelm
Tue Jun 25 11:41:16 2013 +0200 (2013-06-25)
changeset 52443 725916b7dee5
parent 49347 d4768cb77a69
child 53576 793a429c63e7
permissions -rwxr-xr-x
more formal isabelle_admin_build;
tuned;
     1 # -*- shell-script -*- :mode=shellscript:
     2 #
     3 # Author: Markus Wenzel, TU Muenchen
     4 #
     5 # getsettings - bash source script to augment current env.
     6 
     7 if [ -z "$ISABELLE_SETTINGS_PRESENT" ]
     8 then
     9 
    10 set -o allexport
    11 
    12 ISABELLE_SETTINGS_PRESENT=true
    13 
    14 #Cygwin vs. POSIX
    15 if [ "$OSTYPE" = cygwin ]
    16 then
    17   if [ -z "$USER_HOME" ]; then
    18     USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")"
    19   fi
    20 
    21   ISABELLE_HOME_WINDOWS="$(cygpath -w "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")"
    22   ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")"
    23 
    24   CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
    25   function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
    26   CYGWIN_ROOT="$(jvmpath "/")"
    27 else
    28   if [ -z "$USER_HOME" ]; then
    29     USER_HOME="$HOME"
    30   fi
    31 
    32   function jvmpath() { echo "$@"; }
    33   CLASSPATH="$CLASSPATH"
    34 fi
    35 
    36 export ISABELLE_HOME
    37 
    38 #key executables
    39 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
    40 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
    41 
    42 function isabelle ()
    43 {
    44   "$ISABELLE_TOOL" "$@"
    45 }
    46 
    47 #platform
    48 source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
    49 if [ -z "$ISABELLE_PLATFORM" ]; then
    50   echo 1>&2 "Failed to determine hardware and operating system type!"
    51   exit 2
    52 fi
    53 
    54 #Isabelle distribution identifier -- filled in automatically!
    55 ISABELLE_ID=""
    56 [ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
    57 
    58 #sometimes users put strange things in here ...
    59 unset ENV
    60 unset BASH_ENV
    61 
    62 #shared library convenience
    63 function librarypath ()
    64 {
    65   for X in "$@"
    66   do
    67     case "$ISABELLE_PLATFORM" in
    68       *-darwin)
    69         if [ -z "$DYLD_LIBRARY_PATH" ]; then
    70           DYLD_LIBRARY_PATH="$X"
    71         else
    72           DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
    73         fi
    74         export DYLD_LIBRARY_PATH
    75         ;;
    76       *)
    77         if [ -z "$LD_LIBRARY_PATH" ]; then
    78           LD_LIBRARY_PATH="$X"
    79         else
    80           LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
    81         fi
    82         export LD_LIBRARY_PATH
    83         ;;
    84     esac
    85   done
    86 }
    87 
    88 #robust invocation via ISABELLE_JDK_HOME
    89 function isabelle_jdk ()
    90 {
    91   if [ -z "$ISABELLE_JDK_HOME" ]; then
    92     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
    93     return 127
    94   else
    95     local PRG="$1"; shift
    96     "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
    97   fi
    98 }
    99 
   100 #robust invocation via SCALA_HOME
   101 function isabelle_scala ()
   102 {
   103   if [ -z "$ISABELLE_JDK_HOME" ]; then
   104     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
   105     return 127
   106   elif [ -z "$SCALA_HOME" ]; then
   107     echo "Unknown SCALA_HOME -- Scala unavailable" >&2
   108     return 127
   109   else
   110     local PRG="$1"; shift
   111     "$SCALA_HOME/bin/$PRG" "$@"
   112   fi
   113 }
   114 
   115 #administrative build
   116 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
   117   function isabelle_admin_build ()
   118   {
   119     "$ISABELLE_HOME/Admin/build" "$@"
   120   }
   121 else
   122   function isabelle_admin_build () { return 0; }
   123 fi
   124 
   125 #CLASSPATH convenience
   126 function classpath ()
   127 {
   128   for X in "$@"
   129   do
   130     if [ -z "$CLASSPATH" ]; then
   131       CLASSPATH="$X"
   132     else
   133       CLASSPATH="$X:$CLASSPATH"
   134     fi
   135   done
   136   export CLASSPATH
   137 }
   138 
   139 #arrays
   140 function splitarray ()
   141 {
   142   SPLITARRAY=()
   143   local IFS="$1"; shift
   144   for X in $*
   145   do
   146     SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
   147   done
   148 }
   149 
   150 
   151 # components
   152 
   153 ISABELLE_COMPONENTS=""
   154 ISABELLE_COMPONENTS_MISSING=""
   155 
   156 #init component tree
   157 function init_component ()
   158 {
   159   local COMPONENT="$1"
   160   case "$COMPONENT" in
   161     /*) ;;
   162     *)
   163       echo >&2 "Absolute component path required: \"$COMPONENT\""
   164       exit 2
   165       ;;
   166   esac
   167 
   168   if [ -d "$COMPONENT" ]; then
   169     if [ -z "$ISABELLE_COMPONENTS" ]; then
   170       ISABELLE_COMPONENTS="$COMPONENT"
   171     else
   172       ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
   173     fi
   174   else
   175     echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
   176     if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
   177       ISABELLE_COMPONENTS_MISSING="$COMPONENT"
   178     else
   179       ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
   180     fi
   181   fi
   182 
   183   if [ -f "$COMPONENT/etc/settings" ]; then
   184     source "$COMPONENT/etc/settings"
   185     local RC="$?"
   186     if [ "$RC" -ne 0 ]; then
   187       echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
   188       exit 2
   189     fi
   190   fi
   191   if [ -f "$COMPONENT/etc/components" ]; then
   192     init_components "$COMPONENT" "$COMPONENT/etc/components"
   193   fi
   194 }
   195 
   196 #init component forest
   197 function init_components ()
   198 {
   199   local BASE="$1"
   200   local CATALOG="$2"
   201 
   202   if [ ! -f "$CATALOG" ]; then
   203     echo >&2 "Bad component catalog file: \"$CATALOG\""
   204     exit 2
   205   fi
   206   {
   207     while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   208     do
   209       case "$REPLY" in
   210         \#* | "") ;;
   211         /*) init_component "$REPLY" ;;
   212         *) init_component "$BASE/$REPLY" ;;
   213       esac
   214     done
   215   } < "$CATALOG"
   216 }
   217 
   218 #main components
   219 init_component "$ISABELLE_HOME"
   220 [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
   221 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
   222 
   223 
   224 #ML system identifier
   225 if [ -z "$ML_PLATFORM" ]; then
   226   ML_IDENTIFIER="$ML_SYSTEM"
   227 else
   228   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
   229 fi
   230 
   231 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   232 
   233 #enforce JAVA_HOME
   234 export JAVA_HOME="$ISABELLE_JDK_HOME"
   235 
   236 #build condition etc.
   237 case "$ML_SYSTEM" in
   238   polyml*)
   239     ISABELLE_POLYML="true"
   240     ;;
   241   *)
   242     ISABELLE_POLYML=""
   243     ;;
   244 esac
   245 
   246 set +o allexport
   247 
   248 fi