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