src/Pure/build
author wenzelm
Mon, 23 Jul 2012 15:59:14 +0200
changeset 48447 ef600ce4559c
parent 48417 bb1d4ec90f30
child 48511 37999ee01156
permissions -rwxr-xr-x
added system build mode: produce output in ISABELLE_HOME; determine output location more explicitly;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48360
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
     2
#
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
     4
#
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
     5
# build - build Isabelle/ML
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
     6
#
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
     7
# Requires proper Isabelle settings environment.
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
     8
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
     9
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    10
## diagnostics
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    11
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    12
function usage()
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    13
{
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    14
  echo
48447
ef600ce4559c added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents: 48417
diff changeset
    15
  echo "Usage: $PRG TARGET OUTPUT"
48360
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    16
  echo
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    17
  exit 1
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    18
}
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    19
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    20
function fail()
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    21
{
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    22
  echo "$1" >&2
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    23
  exit 2
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    24
}
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    25
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    26
[ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    27
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    28
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    29
## process command line
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    30
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    31
# args
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    32
48447
ef600ce4559c added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents: 48417
diff changeset
    33
if [ "$#" -eq 2 ]; then
ef600ce4559c added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents: 48417
diff changeset
    34
  TARGET="$1"; shift
ef600ce4559c added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents: 48417
diff changeset
    35
  OUTPUT="$1"; shift
ef600ce4559c added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents: 48417
diff changeset
    36
else
ef600ce4559c added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents: 48417
diff changeset
    37
  usage
ef600ce4559c added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents: 48417
diff changeset
    38
fi
48360
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    39
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    40
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    41
## main
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    42
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    43
# get compatibility file
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    44
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    45
ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    46
[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    47
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    48
COMPAT=""
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    49
[ -f "ML-Systems/${ML_SYSTEM_BASE}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM_BASE}.ML"
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    50
[ -f "ML-Systems/${ML_SYSTEM}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM}.ML"
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    51
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    52
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    53
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    54
# run isabelle
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    55
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    56
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    57
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    58
if [ "$TARGET" = RAW ]; then
48447
ef600ce4559c added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents: 48417
diff changeset
    59
  if [ -z "$OUTPUT" ]; then
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    60
    "$ISABELLE_PROCESS" \
48417
bb1d4ec90f30 tuned -- no dependency on exit function;
wenzelm
parents: 48373
diff changeset
    61
      -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    62
      -q RAW_ML_SYSTEM
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    63
  else
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    64
    "$ISABELLE_PROCESS" \
48417
bb1d4ec90f30 tuned -- no dependency on exit function;
wenzelm
parents: 48373
diff changeset
    65
      -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    66
      -e "structure Isar = struct fun main () = () end;" \
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    67
      -e "ml_prompts \"ML> \" \"ML# \";" \
48447
ef600ce4559c added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents: 48417
diff changeset
    68
      -q -w RAW_ML_SYSTEM "$OUTPUT"
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    69
  fi
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    70
else
48447
ef600ce4559c added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents: 48417
diff changeset
    71
  if [ -z "$OUTPUT" ]; then
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    72
    "$ISABELLE_PROCESS" \
48417
bb1d4ec90f30 tuned -- no dependency on exit function;
wenzelm
parents: 48373
diff changeset
    73
      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    74
      -q RAW_ML_SYSTEM
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    75
  else
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    76
    "$ISABELLE_PROCESS" \
48417
bb1d4ec90f30 tuned -- no dependency on exit function;
wenzelm
parents: 48373
diff changeset
    77
      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    78
      -e "ml_prompts \"ML> \" \"ML# \";" \
48447
ef600ce4559c added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents: 48417
diff changeset
    79
      -f -q -w RAW_ML_SYSTEM "$OUTPUT"
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    80
  fi
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    81
fi
48360
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    82
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48360
diff changeset
    83
RC="$?"
48360
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    84
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    85
. "$ISABELLE_HOME/lib/scripts/timestop.bash"
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    86
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    87
if [ "$RC" -eq 0 ]; then
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    88
  echo "Finished $TARGET ($TIMES_REPORT)" >&2
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    89
fi
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    90
631d286e97b0 simplified script to build Isabelle/ML;
wenzelm
parents:
diff changeset
    91
exit "$RC"