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