lib/scripts/getfunctions
author wenzelm
Thu Nov 08 15:52:10 2018 +0100 (8 months ago)
changeset 69267 517655a528fe
parent 69255 800b1ce96fce
child 69277 258bef08b31e
permissions -rw-r--r--
always insist in specified resolver/compiler version;
     1 # -*- shell-script -*- :mode=shellscript:
     2 #
     3 # Author: Makarius
     4 #
     5 # Isabelle shell functions, with on-demand re-initialization for
     6 # non-interactive bash processess. NB: bash shell functions are not portable
     7 # and may be dropped by aggressively POSIX-conformant versions of /bin/sh.
     8 
     9 if type splitarray >/dev/null 2>/dev/null
    10 then
    11   :
    12 else
    13 
    14 if [ "$OSTYPE" = cygwin ]; then
    15   function platform_path() { cygpath -i -C UTF8 -w -p "$@"; }
    16   function standard_path() { cygpath -i -u -p "$@" | tr -d '\r'; }
    17 else
    18   function platform_path() { echo "$@"; }
    19   function standard_path() { echo "$@"; }
    20 fi
    21 export -f platform_path standard_path
    22 
    23 #GNU tar (notably on Mac OS X)
    24 if type -p gnutar >/dev/null
    25 then
    26   function tar() { gnutar "$@"; }
    27   export -f tar
    28 fi
    29 
    30 #OCaml management via OPAM
    31 function isabelle_opam()
    32 {
    33   if [ -z "$ISABELLE_OPAM" ]; then
    34     echo "Unknown ISABELLE_OPAM -- OCaml management tools unavailable" >&2
    35     return 127
    36   else
    37     env OPAMROOT="$ISABELLE_OPAM_ROOT" "$ISABELLE_OPAM" "$@"
    38   fi
    39 }
    40 export -f isabelle_opam
    41 
    42 #GHC management via Stack
    43 function isabelle_stack()
    44 {
    45   if [ -z "$ISABELLE_STACK" ]; then
    46     echo "Unknown ISABELLE_STACK -- GHC management tools unavailable" >&2
    47     return 127
    48   else
    49     env STACK_ROOT="$(platform_path "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" --resolver "$ISABELLE_STACK_RESOLVER" --compiler "$ISABELLE_GHC_VERSION" "$@"
    50   fi
    51 }
    52 export -f isabelle_stack
    53 
    54 #robust invocation via ISABELLE_JDK_HOME
    55 function isabelle_jdk ()
    56 {
    57   if [ -z "$ISABELLE_JDK_HOME" ]; then
    58     echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2
    59     return 127
    60   else
    61     local PRG="$1"; shift
    62     "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
    63   fi
    64 }
    65 export -f isabelle_jdk
    66 
    67 #robust invocation via JAVA_HOME
    68 function isabelle_java ()
    69 {
    70   if [ -z "$JAVA_HOME" ]; then
    71     echo "Unknown JAVA_HOME -- Java unavailable" >&2
    72     return 127
    73   else
    74     local PRG="$1"; shift
    75     "$JAVA_HOME/bin/$PRG" "$@"
    76   fi
    77 }
    78 export -f isabelle_java
    79 
    80 #robust invocation via SCALA_HOME
    81 function isabelle_scala ()
    82 {
    83   if [ -z "$JAVA_HOME" ]; then
    84     echo "Unknown JAVA_HOME -- Java unavailable" >&2
    85     return 127
    86   elif [ -z "$SCALA_HOME" ]; then
    87     echo "Unknown SCALA_HOME -- Scala unavailable" >&2
    88     return 127
    89   else
    90     local PRG="$1"; shift
    91     "$SCALA_HOME/bin/$PRG" "$@"
    92   fi
    93 }
    94 export -f isabelle_scala
    95 
    96 #classpath
    97 function classpath ()
    98 {
    99   local X=""
   100   for X in "$@"
   101   do
   102     if [ -z "$ISABELLE_CLASSPATH" ]; then
   103       ISABELLE_CLASSPATH="$X"
   104     else
   105       ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
   106     fi
   107   done
   108   export ISABELLE_CLASSPATH
   109 }
   110 export -f classpath
   111 
   112 #file formats
   113 function isabelle_file_format ()
   114 {
   115   local X=""
   116   for X in "$@"
   117   do
   118     if [ -z "$ISABELLE_CLASSES_FILE_FORMAT" ]; then
   119       ISABELLE_CLASSES_FILE_FORMAT="$X"
   120     else
   121       ISABELLE_CLASSES_FILE_FORMAT="$ISABELLE_CLASSES_FILE_FORMAT:$X"
   122     fi
   123   done
   124   export ISABELLE_CLASSES_FILE_FORMAT
   125 }
   126 export -f isabelle_file_format
   127 
   128 #administrative build
   129 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
   130   function isabelle_admin_build ()
   131   {
   132     "$ISABELLE_HOME/Admin/build" "$@"
   133   }
   134 else
   135   function isabelle_admin_build () { return 0; }
   136 fi
   137 export -f isabelle_admin_build
   138 
   139 #arrays
   140 function splitarray ()
   141 {
   142   SPLITARRAY=()
   143   local IFS="$1"; shift
   144   local X=""
   145   for X in $*
   146   do
   147     SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
   148   done
   149 }
   150 export -f splitarray
   151 
   152 #init component tree
   153 function init_component ()
   154 {
   155   local COMPONENT="$1"
   156   case "$COMPONENT" in
   157     /*) ;;
   158     *)
   159       echo >&2 "Absolute component path required: \"$COMPONENT\""
   160       exit 2
   161       ;;
   162   esac
   163 
   164   if [ -d "$COMPONENT" ]; then
   165     if [ -z "$ISABELLE_COMPONENTS" ]; then
   166       ISABELLE_COMPONENTS="$COMPONENT"
   167     else
   168       ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
   169     fi
   170   else
   171     echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
   172     if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
   173       ISABELLE_COMPONENTS_MISSING="$COMPONENT"
   174     else
   175       ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
   176     fi
   177   fi
   178 
   179   if [ -f "$COMPONENT/etc/settings" ]; then
   180     source "$COMPONENT/etc/settings"
   181     local RC="$?"
   182     if [ "$RC" -ne 0 ]; then
   183       echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
   184       exit 2
   185     fi
   186   fi
   187   if [ -f "$COMPONENT/etc/components" ]; then
   188     init_components "$COMPONENT" "$COMPONENT/etc/components"
   189   fi
   190 }
   191 export -f init_component
   192 
   193 #init component forest
   194 function init_components ()
   195 {
   196   local REPLY=""
   197   local BASE="$1"
   198   local CATALOG="$2"
   199   local COMPONENT=""
   200   local -a COMPONENTS=()
   201 
   202   if [ ! -f "$CATALOG" ]; then
   203     echo >&2 "Bad component catalog file: \"$CATALOG\""
   204     exit 2
   205   fi
   206 
   207   {
   208     while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   209     do
   210       case "$REPLY" in
   211         \#* | "") ;;
   212         /*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;;
   213         *) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;;
   214       esac
   215     done
   216   } < "$CATALOG"
   217 
   218   for COMPONENT in "${COMPONENTS[@]}"
   219   do
   220     init_component "$COMPONENT"
   221   done
   222 }
   223 export -f init_components
   224 
   225 fi