src/Pure/build
author wenzelm
Mon Aug 17 23:45:12 2015 +0200 (2015-08-17)
changeset 60962 faa452d8e265
parent 52083 f852d08376f9
child 61925 ab52f183f020
permissions -rwxr-xr-x
basic setup for native Windows (RAW session without image);
     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 _ => OS.Process.exit OS.Process.failure;" \
    65       -q RAW_ML_SYSTEM
    66   else
    67     "$ISABELLE_PROCESS" \
    68       -e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
    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 _ => OS.Process.exit OS.Process.failure;" \
    77       -q RAW_ML_SYSTEM
    78   else
    79     "$ISABELLE_PROCESS" \
    80       -e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
    81       -e "ml_prompts \"ML> \" \"ML# \";" \
    82       -e "Command_Line.tool0 Session.finish;" \
    83       -e "Options.reset_default ();" \
    84       -q -w RAW_ML_SYSTEM "$OUTPUT"
    85   fi
    86 fi
    87 
    88 RC="$?"
    89 
    90 . "$ISABELLE_HOME/lib/scripts/timestop.bash"
    91 
    92 if [ "$RC" -eq 0 ]; then
    93   echo "Finished $TARGET ($TIMES_REPORT)" >&2
    94 fi
    95 
    96 exit "$RC"