src/Pure/build
author wenzelm
Sun Nov 11 20:31:46 2012 +0100 (2012-11-11)
changeset 50081 9b92ee8dec98
parent 48662 b171bcd5dd86
child 52054 eaf17514aabd
permissions -rwxr-xr-x
tuned;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Makarius
     4 #
     5 # build - build Isabelle/ML
     6 #
     7 # Requires proper Isabelle settings environment.
     8 
     9 
    10 ## diagnostics
    11 
    12 function usage()
    13 {
    14   echo
    15   echo "Usage: $PRG TARGET [OUTPUT]"
    16   echo
    17   exit 1
    18 }
    19 
    20 function fail()
    21 {
    22   echo "$1" >&2
    23   exit 2
    24 }
    25 
    26 [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"
    27 
    28 
    29 ## process command line
    30 
    31 # args
    32 
    33 if [ "$#" -eq 1 ]; then
    34   TARGET="$1"; shift
    35   OUTPUT=""; shift
    36 elif [ "$#" -eq 2 ]; then
    37   TARGET="$1"; shift
    38   OUTPUT="$1"; shift
    39 else
    40   usage
    41 fi
    42 
    43 
    44 ## main
    45 
    46 # get compatibility file
    47 
    48 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
    49 [ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
    50 
    51 COMPAT=""
    52 [ -f "ML-Systems/${ML_SYSTEM_BASE}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM_BASE}.ML"
    53 [ -f "ML-Systems/${ML_SYSTEM}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM}.ML"
    54 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
    55 
    56 
    57 # run isabelle
    58 
    59 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
    60 
    61 if [ "$TARGET" = RAW ]; then
    62   if [ -z "$OUTPUT" ]; then
    63     "$ISABELLE_PROCESS" \
    64       -e "use\"$COMPAT\" handle _ => Posix.Process.exit 0w1;" \
    65       -q RAW_ML_SYSTEM
    66   else
    67     "$ISABELLE_PROCESS" \
    68       -e "use\"$COMPAT\" handle _ => Posix.Process.exit 0w1;" \
    69       -e "structure Isar = struct fun main () = () end;" \
    70       -e "ml_prompts \"ML> \" \"ML# \";" \
    71       -q -w RAW_ML_SYSTEM "$OUTPUT"
    72   fi
    73 else
    74   if [ -z "$OUTPUT" ]; then
    75     "$ISABELLE_PROCESS" \
    76       -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \
    77       -q RAW_ML_SYSTEM
    78   else
    79     "$ISABELLE_PROCESS" \
    80       -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \
    81       -e "ml_prompts \"ML> \" \"ML# \";" \
    82       -f -q -w RAW_ML_SYSTEM "$OUTPUT"
    83   fi
    84 fi
    85 
    86 RC="$?"
    87 
    88 . "$ISABELLE_HOME/lib/scripts/timestop.bash"
    89 
    90 if [ "$RC" -eq 0 ]; then
    91   echo "Finished $TARGET ($TIMES_REPORT)" >&2
    92 fi
    93 
    94 exit "$RC"