wneuper/isa: src/Pure/build@37999ee01156

     1 #!/usr/bin/env bash

2 #

     3 # Author: Makarius

4 #

     5 # build - build Isabelle/ML

6 #

     7 # Requires proper Isabelle settings environment.

    10 ## diagnostics

    12 function usage()

    13 {

    14   echo

    15   echo "Usage: $PRG TARGET [OUTPUT]"

    16   echo

    17   exit 1

    18 }

    20 function fail()

    21 {

    22   echo "$1" >&2

    23   exit 2

    24 }

    26 [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"

    29 ## process command line

    31 # args

    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

    44 ## main

    46 # get compatibility file

    48 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)

    49 [ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"

    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\"!"

    57 # run isabelle

    59 . "$ISABELLE_HOME/lib/scripts/timestart.bash"

    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       -f -q -w RAW_ML_SYSTEM "$OUTPUT"

    83   fi

    84 fi

    86 RC="$?"

    88 . "$ISABELLE_HOME/lib/scripts/timestop.bash"

    90 if [ "$RC" -eq 0 ]; then

    91   echo "Finished $TARGET ($TIMES_REPORT)" >&2

    92 fi

    94 exit "$RC"

author	wenzelm
	Thu, 26 Jul 2012 12:59:09 +0200
changeset 49526	37999ee01156
parent 49462	ef600ce4559c
child 49677	b171bcd5dd86
permissions	-rwxr-xr-x