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