lib/scripts/getsettings
author wenzelm
Wed Sep 30 21:05:14 2015 +0200 (2015-09-30)
changeset 61293 876e7eae22be
parent 61159 da900891ee06
child 61294 2d3d26e9b191
permissions -rwxr-xr-x
clarified ISABELLE_ROOT (platform path) vs. ISABELLE_HOME (standard path);
     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 #GNU tar (notably on Mac OS X)
    15 if [ -x /usr/bin/gnutar ]; then
    16   function tar() { /usr/bin/gnutar "$@"; }
    17 fi
    18 
    19 #sane environment defaults (notably on Mac OS X)
    20 if [ "$ISABELLE_APP" = true -a -x /usr/libexec/path_helper ]; then
    21   eval $(/usr/libexec/path_helper -s)
    22 fi
    23 
    24 #Cygwin vs. POSIX
    25 if [ "$OSTYPE" = cygwin ]
    26 then
    27   unset INI_DIR
    28 
    29   if [ -n "$TEMP_WINDOWS" ]; then
    30     TMPDIR="$(cygpath -u "$TEMP_WINDOWS")"
    31     TMP="$TMPDIR"
    32     TEMP="$TMPDIR"
    33   fi
    34 
    35   if [ -z "$USER_HOME" ]; then
    36     USER_HOME="$(cygpath -u "$USERPROFILE")"
    37   fi
    38 
    39   function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
    40   CYGWIN_ROOT="$(jvmpath "/")"
    41   ISABELLE_ROOT="$(jvmpath "$ISABELLE_HOME")"
    42 
    43   ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
    44   unset CLASSPATH
    45 else
    46   if [ -z "$USER_HOME" ]; then
    47     USER_HOME="$HOME"
    48   fi
    49 
    50   ISABELLE_ROOT="$ISABELLE_HOME"
    51 
    52   function jvmpath() { echo "$@"; }
    53 
    54   ISABELLE_CLASSPATH="$CLASSPATH"
    55   unset CLASSPATH
    56 fi
    57 
    58 export ISABELLE_HOME
    59 
    60 #key executables
    61 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
    62 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle_process"
    63 ISABELLE_SCALA_SCRIPT="$ISABELLE_HOME/bin/isabelle_scala_script"
    64 
    65 function isabelle ()
    66 {
    67   "$ISABELLE_TOOL" "$@"
    68 }
    69 
    70 function isabelle_process ()
    71 {
    72   "$ISABELLE_PROCESS" "$@"
    73 }
    74 
    75 function isabelle_scala_script ()
    76 {
    77   "$ISABELLE_SCALA_SCRIPT" "$@"
    78 }
    79 
    80 #platform
    81 source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
    82 if [ -z "$ISABELLE_PLATFORM" ]; then
    83   echo 1>&2 "Failed to determine hardware and operating system type!"
    84   exit 2
    85 fi
    86 
    87 #Isabelle distribution identifier -- filled in automatically!
    88 ISABELLE_ID=""
    89 [ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
    90 
    91 #sometimes users put strange things in here ...
    92 unset ENV
    93 unset BASH_ENV
    94 
    95 #shared library convenience
    96 function librarypath ()
    97 {
    98   for X in "$@"
    99   do
   100     case "$ISABELLE_PLATFORM" in
   101       *-darwin)
   102         if [ -z "$DYLD_LIBRARY_PATH" ]; then
   103           DYLD_LIBRARY_PATH="$X"
   104         else
   105           DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
   106         fi
   107         export DYLD_LIBRARY_PATH
   108         ;;
   109       *)
   110         if [ -z "$LD_LIBRARY_PATH" ]; then
   111           LD_LIBRARY_PATH="$X"
   112         else
   113           LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
   114         fi
   115         export LD_LIBRARY_PATH
   116         ;;
   117     esac
   118   done
   119 }
   120 
   121 #robust invocation via ISABELLE_JDK_HOME
   122 function isabelle_jdk ()
   123 {
   124   if [ -z "$ISABELLE_JDK_HOME" ]; then
   125     echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2
   126     return 127
   127   else
   128     local PRG="$1"; shift
   129     "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
   130   fi
   131 }
   132 
   133 #robust invocation via JAVA_HOME
   134 function isabelle_java ()
   135 {
   136   if [ -z "$JAVA_HOME" ]; then
   137     echo "Unknown JAVA_HOME -- Java unavailable" >&2
   138     return 127
   139   else
   140     local PRG="$1"; shift
   141     "$JAVA_HOME/bin/$PRG" "$@"
   142   fi
   143 }
   144 
   145 #robust invocation via SCALA_HOME
   146 function isabelle_scala ()
   147 {
   148   if [ -z "$JAVA_HOME" ]; then
   149     echo "Unknown JAVA_HOME -- Java unavailable" >&2
   150     return 127
   151   elif [ -z "$SCALA_HOME" ]; then
   152     echo "Unknown SCALA_HOME -- Scala unavailable" >&2
   153     return 127
   154   else
   155     local PRG="$1"; shift
   156     "$SCALA_HOME/bin/$PRG" "$@"
   157   fi
   158 }
   159 
   160 #administrative build
   161 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
   162   function isabelle_admin_build ()
   163   {
   164     "$ISABELLE_HOME/Admin/build" "$@"
   165   }
   166 else
   167   function isabelle_admin_build () { return 0; }
   168 fi
   169 
   170 #classpath
   171 function classpath ()
   172 {
   173   for X in "$@"
   174   do
   175     if [ -z "$ISABELLE_CLASSPATH" ]; then
   176       ISABELLE_CLASSPATH="$X"
   177     else
   178       ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
   179     fi
   180   done
   181   export ISABELLE_CLASSPATH
   182 }
   183 
   184 #arrays
   185 function splitarray ()
   186 {
   187   SPLITARRAY=()
   188   local IFS="$1"; shift
   189   for X in $*
   190   do
   191     SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
   192   done
   193 }
   194 
   195 
   196 # components
   197 
   198 ISABELLE_COMPONENTS=""
   199 ISABELLE_COMPONENTS_MISSING=""
   200 
   201 #init component tree
   202 function init_component ()
   203 {
   204   local COMPONENT="$1"
   205   case "$COMPONENT" in
   206     /*) ;;
   207     *)
   208       echo >&2 "Absolute component path required: \"$COMPONENT\""
   209       exit 2
   210       ;;
   211   esac
   212 
   213   if [ -d "$COMPONENT" ]; then
   214     if [ -z "$ISABELLE_COMPONENTS" ]; then
   215       ISABELLE_COMPONENTS="$COMPONENT"
   216     else
   217       ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
   218     fi
   219   else
   220     echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
   221     if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
   222       ISABELLE_COMPONENTS_MISSING="$COMPONENT"
   223     else
   224       ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
   225     fi
   226   fi
   227 
   228   if [ -f "$COMPONENT/etc/settings" ]; then
   229     source "$COMPONENT/etc/settings"
   230     local RC="$?"
   231     if [ "$RC" -ne 0 ]; then
   232       echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
   233       exit 2
   234     fi
   235   fi
   236   if [ -f "$COMPONENT/etc/components" ]; then
   237     init_components "$COMPONENT" "$COMPONENT/etc/components"
   238   fi
   239 }
   240 
   241 #init component forest
   242 function init_components ()
   243 {
   244   local BASE="$1"
   245   local CATALOG="$2"
   246   local COMPONENT=""
   247   local -a COMPONENTS=()
   248 
   249   if [ ! -f "$CATALOG" ]; then
   250     echo >&2 "Bad component catalog file: \"$CATALOG\""
   251     exit 2
   252   fi
   253 
   254   {
   255     while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   256     do
   257       case "$REPLY" in
   258         \#* | "") ;;
   259         /*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;;
   260         *) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;;
   261       esac
   262     done
   263   } < "$CATALOG"
   264 
   265   for COMPONENT in "${COMPONENTS[@]}"
   266   do
   267     init_component "$COMPONENT"
   268   done
   269 }
   270 
   271 #main components
   272 init_component "$ISABELLE_HOME"
   273 [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
   274 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
   275 
   276 
   277 #ML system identifier
   278 if [ -z "$ML_PLATFORM" ]; then
   279   ML_IDENTIFIER="$ML_SYSTEM"
   280 else
   281   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
   282 fi
   283 
   284 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   285 
   286 #enforce JAVA_HOME
   287 export JAVA_HOME="$ISABELLE_JDK_HOME/jre"
   288 
   289 #build condition etc.
   290 case "$ML_SYSTEM" in
   291   polyml*)
   292     ML_SYSTEM_POLYML="true"
   293     ;;
   294   *)
   295     ML_SYSTEM_POLYML=""
   296     ;;
   297 esac
   298 
   299 set +o allexport
   300 
   301 fi