src/Pure/mk
author blanchet
Mon, 06 Dec 2010 13:29:23 +0100
changeset 40996 63112be4a469
parent 34282 549969a7f582
child 43948 8f5add916a99
permissions -rwxr-xr-x
added "Neq" operator to monotonicity inference module
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11391
e8638d07fdee #!/usr/bin/env bash;
wenzelm
parents: 10900
diff changeset
     1
#!/usr/bin/env bash
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     2
#
9789
wenzelm
parents: 8361
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     4
#
34282
549969a7f582 simplified build/bootstrap of Isabelle/Scala components -- avoid make;
wenzelm
parents: 31317
diff changeset
     5
# mk - build Isabelle/Pure.
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     6
#
34282
549969a7f582 simplified build/bootstrap of Isabelle/Scala components -- avoid make;
wenzelm
parents: 31317
diff changeset
     7
# Requires proper Isabelle settings environment.
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     8
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     9
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    10
## diagnostics
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    11
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    12
function usage()
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    13
{
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    14
  echo
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    15
  echo "Usage: $PRG [OPTIONS]"
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    16
  echo
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    17
  echo "  Make Pure Isabelle."
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    18
  echo
21996
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    19
  echo "    -R DIR/FILE  run RAW session"
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    20
  echo "    -r           build RAW image"
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    21
  echo
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    22
  exit 1
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    23
}
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    24
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    25
function fail()
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    26
{
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    27
  echo "$1" >&2
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    28
  exit 2
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    29
}
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    30
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    31
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    32
## process command line
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    33
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    34
# options
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    35
21996
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    36
RAW_SESSION=""
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    37
RAW=""
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    38
21996
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    39
while getopts "R:r" OPT
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    40
do
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    41
  case "$OPT" in
21996
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    42
    R)
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    43
      RAW_SESSION="$OPTARG"
10102
3c21a2e616e7 support copy option;
wenzelm
parents: 9789
diff changeset
    44
      ;;
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    45
    r)
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    46
      RAW=true
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    47
      ;;
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    48
    \?)
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    49
      usage
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    50
      ;;
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    51
  esac
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    52
done
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    53
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    54
shift $(($OPTIND - 1))
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    55
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    56
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    57
# args
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    58
9789
wenzelm
parents: 8361
diff changeset
    59
[ "$#" -ne 0 ] && usage
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    60
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    61
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    62
## main
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    63
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    64
# get compatibility file
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    65
9789
wenzelm
parents: 8361
diff changeset
    66
ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
16131
e1b85512d87d tuned msg;
wenzelm
parents: 15790
diff changeset
    67
[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    68
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    69
COMPAT=""
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    70
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    71
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    72
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    73
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    74
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    75
# prepare log dir
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    76
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    77
LOGDIR="$ISABELLE_OUTPUT/log"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    78
mkdir -p "$LOGDIR"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    79
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    80
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    81
# run isabelle
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    82
18321
3414557c2dda replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
wenzelm
parents: 16376
diff changeset
    83
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    84
21996
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    85
if [ -n "$RAW" ]; then
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    86
  ITEM="RAW"
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    87
  echo "Building $ITEM ..."
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    88
  LOG="$LOGDIR/$ITEM"
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    89
28502
6b0e3e4e1891 replaced ISABELLE by ISABELLE_PROCESS;
wenzelm
parents: 22011
diff changeset
    90
  "$ISABELLE_PROCESS" \
21996
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    91
    -e "val ml_system = \"$ML_SYSTEM\";" \
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    92
    -e "val ml_platform = \"$ML_PLATFORM\";" \
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    93
    -e "use\"$COMPAT\" handle _ => exit 1;" \
30592
a66fe59e0a26 RAW: provide dummy Isar.main to make tty work gracefully (with ML toplevel);
wenzelm
parents: 30204
diff changeset
    94
    -e "structure Isar = struct fun main () = () end;" \
30611
591fefcf184e uniform ml_prompts for RAW and Pure;
wenzelm
parents: 30592
diff changeset
    95
    -e "ml_prompts \"ML> \" \"ML# \";" \
21996
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    96
    -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    97
  RC="$?"
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    98
elif [ -n "$RAW_SESSION" ]; then
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
    99
  ITEM="RAW-$(basename $(dirname "$RAW_SESSION"))"
22011
3d4ea1819cb7 tuned msg;
wenzelm
parents: 21996
diff changeset
   100
  echo "Running $ITEM ..."
21996
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
   101
  LOG="$LOGDIR/$ITEM"
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
   102
28502
6b0e3e4e1891 replaced ISABELLE by ISABELLE_PROCESS;
wenzelm
parents: 22011
diff changeset
   103
  "$ISABELLE_PROCESS" \
21996
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
   104
    -e "use\"$RAW_SESSION\" handle _ => exit 1;" \
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
   105
    -q RAW > "$LOG" 2>&1
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
   106
  RC="$?"
18937ee21db7 removed obsolete option -C;
wenzelm
parents: 20814
diff changeset
   107
else
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   108
  ITEM="Pure"
7277
bb9502f9154a improved messages;
wenzelm
parents: 7263
diff changeset
   109
  echo "Building $ITEM ..."
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   110
  LOG="$LOGDIR/$ITEM"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   111
28502
6b0e3e4e1891 replaced ISABELLE by ISABELLE_PROCESS;
wenzelm
parents: 22011
diff changeset
   112
  "$ISABELLE_PROCESS" \
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
   113
    -e "val ml_system = \"$ML_SYSTEM\";" \
16376
65e2df6d8e10 pass ml_platform;
wenzelm
parents: 16131
diff changeset
   114
    -e "val ml_platform = \"$ML_PLATFORM\";" \
4495
8648ba842d14 improved error handling;
wenzelm
parents: 4492
diff changeset
   115
    -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
30611
591fefcf184e uniform ml_prompts for RAW and Pure;
wenzelm
parents: 30592
diff changeset
   116
    -e "ml_prompts \"ML> \" \"ML# \";" \
31317
1f5740424c69 removed "compress" option from isabelle-process and isabelle usedir -- this is always enabled;
wenzelm
parents: 30611
diff changeset
   117
    -f -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
9789
wenzelm
parents: 8361
diff changeset
   118
  RC="$?"
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
   119
fi
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   120
18321
3414557c2dda replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
wenzelm
parents: 16376
diff changeset
   121
. "$ISABELLE_HOME/lib/scripts/timestop.bash"
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   122
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   123
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   124
# exit status
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   125
9789
wenzelm
parents: 8361
diff changeset
   126
if [ "$RC" -eq 0 ]; then
18321
3414557c2dda replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
wenzelm
parents: 16376
diff changeset
   127
  echo "Finished $ITEM ($TIMES_REPORT)"
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   128
  gzip --force "$LOG"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   129
else
7263
2d09363ada6c tuned messages;
wenzelm
parents: 6239
diff changeset
   130
  echo "$ITEM FAILED"
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   131
  echo "(see also $LOG)"
9789
wenzelm
parents: 8361
diff changeset
   132
  echo; tail "$LOG"; echo
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   133
fi
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   134
9789
wenzelm
parents: 8361
diff changeset
   135
exit "$RC"