build
author berghofe
Thu Apr 21 19:12:03 2005 +0200 (2005-04-21)
changeset 15797 a63605582573
parent 15779 aed221aff642
child 15844 6b1e5f703246
permissions -rwxr-xr-x
- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 #
     6 # build - compile the Isabelle system and object-logics
     7 
     8 
     9 ## global settings
    10 
    11 ALL_LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Pure Sequents ZF"
    12 
    13 
    14 ## settings
    15 
    16 PRG="$(basename "$0")"
    17 
    18 export THIS_IS_ISABELLE_BUILD=true
    19 ISABELLE_HOME="$(dirname "$0")"
    20 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
    21   { echo "$PRG probably not called from its original place!"; exit 2; }
    22 
    23 
    24 ## diagnostics
    25 
    26 function usage()
    27 {
    28   echo
    29   echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
    30   echo
    31   echo "  Options are:"
    32   echo "    -a           all logics"
    33   echo "    -b           batch mode"
    34   echo "    -i           make images"
    35   echo "    -m TARGET    make this target"
    36   echo "    -t           make test"
    37   echo
    38   echo "  Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics"
    39   echo "  in the distribution."
    40   echo
    41   exit 1
    42 }
    43 
    44 function fail()
    45 {
    46   echo "$1" >&2
    47   exit 2
    48 }
    49 
    50 
    51 ## process command line
    52 
    53 # options
    54 
    55 ALL=""
    56 BATCH=""
    57 TARGETS=""
    58 
    59 while getopts "abim:p:t" OPT
    60 do
    61   case "$OPT" in
    62     a)
    63       ALL=true
    64       ;;
    65     b)
    66       BATCH=true
    67       ;;
    68     i)
    69       TARGETS="$TARGETS images"
    70       ;;
    71     m)
    72       TARGETS="$TARGETS $OPTARG"
    73       ;;
    74     t)
    75       TARGETS="$TARGETS test"
    76       ;;
    77     \?)
    78       usage
    79       ;;
    80   esac
    81 done
    82 
    83 shift $(($OPTIND - 1))
    84 
    85 
    86 # args
    87 
    88 LOGICS="$@"
    89 
    90 [ -n "$ALL" ] && LOGICS="$LOGICS $ALL_LOGICS"
    91 [ -z "$LOGICS" ] && LOGICS="$ISABELLE_LOGIC"
    92 
    93 
    94 ## main
    95 
    96 # tell the user about current values
    97 
    98 if [ -z "$BATCH" ]; then
    99   echo
   100   echo "                *****************************"
   101   echo "                * Welcome to Isabelle build *"
   102   echo "                *****************************"
   103   echo
   104   echo "Please check $ISABELLE_HOME/etc/settings"
   105   [ -f "$ISABELLE_HOME_USER/etc/settings" ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
   106   echo "to make sure that Isabelle's ML system settings and compilation options"
   107   echo "are appropriate."
   108   echo
   109   echo "The current values are:"
   110   echo
   111   echo "  ML_SYSTEM=$ML_SYSTEM"
   112   echo "  ML_HOME=$ML_HOME"
   113   echo "  ML_OPTIONS=$ML_OPTIONS"
   114   echo "  ML_PLATFORM=$ML_PLATFORM"
   115   echo "  ISABELLE_INTERFACE=$ISABELLE_INTERFACE"
   116   echo "ISABELLE_OUTPUT=$ISABELLE_OUTPUT"
   117   echo
   118   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
   119 fi
   120 
   121 
   122 # check logics
   123 
   124 if [ -z "$BATCH" ]; then
   125   echo
   126   echo
   127   echo "Press RETURN to compilation of"
   128   echo
   129 fi
   130 
   131 
   132 MAKE_LOGICS=""
   133 
   134 for L in $LOGICS
   135 do
   136   DIR="$ISABELLE_HOME/src/$L"
   137   if [ -f "$DIR/IsaMakefile" ]; then
   138     MAKE_LOGICS="$MAKE_LOGICS $L"
   139   else
   140     echo "No such logic: $L"
   141   fi
   142 done
   143 
   144 
   145 if [ -z "$BATCH" ]; then
   146   echo " $MAKE_LOGICS"
   147   [ -n "$TARGETS" ] && echo "  (targets:$TARGETS)"
   148   echo
   149   read
   150 else
   151   echo
   152   echo "Isabelle build: $MAKE_LOGICS"
   153   [ -n "$TARGETS" ] && echo "(targets:$TARGETS)"
   154   echo
   155   echo "ML_SYSTEM=$ML_SYSTEM"
   156   echo "ML_HOME=$ML_HOME"
   157   echo "ML_OPTIONS=$ML_OPTIONS"
   158   echo "ML_PLATFORM=$ML_PLATFORM"
   159   echo "ISABELLE_OUTPUT=$ISABELLE_OUTPUT"
   160   echo
   161   echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
   162   echo
   163 fi
   164 
   165 
   166 # build it
   167 
   168 SECONDS=0
   169 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
   170 
   171 for L in $MAKE_LOGICS
   172 do
   173   ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make $TARGETS )
   174 done
   175 
   176 echo -n "Finished at "; date
   177 
   178 ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
   179 echo "$ELAPSED total elapsed time"