build
author mueller
Thu, 24 Apr 1997 18:07:35 +0200
changeset 3041 bdd21deed6ea
parent 3007 e5efa177ee0c
child 3184 4e0bbfb113d5
permissions -rwxr-xr-x
expandshort
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3007
e5efa177ee0c removed -norc;
wenzelm
parents: 2936
diff changeset
     1
#!/bin/bash
2755
9a7128d9722e build - compile parts of the Isabelle system;
wenzelm
parents:
diff changeset
     2
#
9a7128d9722e build - compile parts of the Isabelle system;
wenzelm
parents:
diff changeset
     3
# $Id$
9a7128d9722e build - compile parts of the Isabelle system;
wenzelm
parents:
diff changeset
     4
#
2902
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
     5
# build - compile the Isabelle system and object-logics
2755
9a7128d9722e build - compile parts of the Isabelle system;
wenzelm
parents:
diff changeset
     6
9a7128d9722e build - compile parts of the Isabelle system;
wenzelm
parents:
diff changeset
     7
2789
69cf3aea45ee major tuning;
wenzelm
parents: 2781
diff changeset
     8
## settings
69cf3aea45ee major tuning;
wenzelm
parents: 2781
diff changeset
     9
69cf3aea45ee major tuning;
wenzelm
parents: 2781
diff changeset
    10
PRG=$(basename $0)
2755
9a7128d9722e build - compile parts of the Isabelle system;
wenzelm
parents:
diff changeset
    11
2789
69cf3aea45ee major tuning;
wenzelm
parents: 2781
diff changeset
    12
ISABELLE_HOME=$(dirname $0)
69cf3aea45ee major tuning;
wenzelm
parents: 2781
diff changeset
    13
. $ISABELLE_HOME/lib/scripts/getsettings || \
2936
bd33e7aae062 fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents: 2918
diff changeset
    14
  { echo "$PRG probably not called from its original place!"; exit 2; }
2755
9a7128d9722e build - compile parts of the Isabelle system;
wenzelm
parents:
diff changeset
    15
2789
69cf3aea45ee major tuning;
wenzelm
parents: 2781
diff changeset
    16
2879
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    17
## diagnostics
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    18
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    19
function usage()
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    20
{
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    21
  echo
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    22
  echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    23
  echo
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    24
  echo "  Options are:"
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    25
  echo "    -a           all logics"
2902
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    26
  echo "    -b           batch mode"
2918
0305b0acba78 added -t (run tests) option;
wenzelm
parents: 2914
diff changeset
    27
  echo "    -t           run tests"
2879
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    28
  echo
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    29
  echo "  Compile the named LOGICS (default $DEFAULT_LOGIC), or all object logics"
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    30
  echo "  in the distribution."
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    31
  echo
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    32
  exit 1
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    33
}
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    34
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    35
function fail()
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    36
{
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    37
  echo "$1" >&2
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    38
  exit 2
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    39
}
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    40
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    41
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    42
## process command line
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    43
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    44
# options
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    45
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    46
ALL=""
2902
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    47
BATCH=""
2918
0305b0acba78 added -t (run tests) option;
wenzelm
parents: 2914
diff changeset
    48
TEST=""
2755
9a7128d9722e build - compile parts of the Isabelle system;
wenzelm
parents:
diff changeset
    49
2918
0305b0acba78 added -t (run tests) option;
wenzelm
parents: 2914
diff changeset
    50
while getopts "abt" OPT
2879
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    51
do
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    52
  case "$OPT" in
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    53
    a)
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    54
      ALL=true
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    55
      ;;
2902
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    56
    b)
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    57
      BATCH=true
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    58
      ;;
2918
0305b0acba78 added -t (run tests) option;
wenzelm
parents: 2914
diff changeset
    59
    t)
0305b0acba78 added -t (run tests) option;
wenzelm
parents: 2914
diff changeset
    60
      TEST=test
0305b0acba78 added -t (run tests) option;
wenzelm
parents: 2914
diff changeset
    61
      ;;
2879
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    62
    \?)
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    63
      usage
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    64
      ;;
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    65
  esac
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    66
done
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    67
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    68
shift $(($OPTIND - 1))
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    69
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    70
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    71
# args
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    72
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    73
LOGICS="$@"
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    74
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    75
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    76
## main
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    77
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    78
# tell the user about current values
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    79
2902
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    80
if [ -z "$BATCH" ]; then
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    81
  echo
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    82
  echo "                *****************************"
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    83
  echo "                * Welcome to Isabelle build *"
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    84
  echo "                *****************************"
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    85
  echo
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    86
  echo "Please check $ISABELLE_HOME/etc/settings"
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    87
  [ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    88
  echo "to make sure that Isabelle's ML system settings are appropriate."
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    89
  echo
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    90
  echo "Your current values are:"
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    91
  echo
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    92
  echo "  ML_SYSTEM=$ML_SYSTEM"
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    93
  echo "  ML_HOME=$ML_HOME"
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    94
  echo "  ML_OPTIONS=$ML_OPTIONS"
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
    95
fi
2789
69cf3aea45ee major tuning;
wenzelm
parents: 2781
diff changeset
    96
69cf3aea45ee major tuning;
wenzelm
parents: 2781
diff changeset
    97
2879
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
    98
# check logics
2755
9a7128d9722e build - compile parts of the Isabelle system;
wenzelm
parents:
diff changeset
    99
2902
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   100
if [ -z "$BATCH" ]; then
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   101
  echo
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   102
  echo
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   103
  echo "Press RETURN to start compilation (including parents) of:"
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   104
  echo
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   105
fi
2879
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   106
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   107
[ -z "$LOGICS" ] && LOGICS=$DEFAULT_LOGIC
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   108
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   109
if [ -n "$ALL" ]; then
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   110
  LOGICS=""
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   111
  for DIR in $ISABELLE_HOME/src/*
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   112
  do
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   113
    if [ -f $DIR/IsaMakefile ]; then
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   114
      L=$(basename $DIR)
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   115
      LOGICS="$LOGICS $L"
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   116
    fi
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   117
  done
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   118
else
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   119
  for L in $LOGICS
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   120
  do
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   121
    DIR=$ISABELLE_HOME/src/$L
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   122
    [ ! -f $DIR/IsaMakefile ] && fail "No such logic: $L"
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   123
  done
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   124
fi
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   125
2902
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   126
if [ -z "$BATCH" ]; then
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   127
  echo " " $LOGICS
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   128
  echo
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   129
  read
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   130
else
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   131
  echo
2914
01d24f98528f improved messages;
wenzelm
parents: 2902
diff changeset
   132
  echo "Isabelle build:" $LOGICS
01d24f98528f improved messages;
wenzelm
parents: 2902
diff changeset
   133
  echo
2902
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   134
  echo "ML_SYSTEM=$ML_SYSTEM"
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   135
  echo "ML_HOME=$ML_HOME"
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   136
  echo "ML_OPTIONS=$ML_OPTIONS"
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   137
  echo
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   138
fi
2755
9a7128d9722e build - compile parts of the Isabelle system;
wenzelm
parents:
diff changeset
   139
9a7128d9722e build - compile parts of the Isabelle system;
wenzelm
parents:
diff changeset
   140
2879
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   141
# build it
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   142
2914
01d24f98528f improved messages;
wenzelm
parents: 2902
diff changeset
   143
echo
01d24f98528f improved messages;
wenzelm
parents: 2902
diff changeset
   144
echo -n "Started at "; date
01d24f98528f improved messages;
wenzelm
parents: 2902
diff changeset
   145
echo
01d24f98528f improved messages;
wenzelm
parents: 2902
diff changeset
   146
2781
0d6fcae3ae45 added THIS_IS_ISABELLE_BUILD;
wenzelm
parents: 2775
diff changeset
   147
export THIS_IS_ISABELLE_BUILD=true
2755
9a7128d9722e build - compile parts of the Isabelle system;
wenzelm
parents:
diff changeset
   148
2879
477bfcb022d8 misc improvements;
wenzelm
parents: 2789
diff changeset
   149
for L in $LOGICS
2755
9a7128d9722e build - compile parts of the Isabelle system;
wenzelm
parents:
diff changeset
   150
do
2918
0305b0acba78 added -t (run tests) option;
wenzelm
parents: 2914
diff changeset
   151
  ( cd $ISABELLE_HOME/src/$L; $ISATOOL make $TEST )
2755
9a7128d9722e build - compile parts of the Isabelle system;
wenzelm
parents:
diff changeset
   152
done
2902
bacef535265c added -b option (batch mode);
wenzelm
parents: 2879
diff changeset
   153
2914
01d24f98528f improved messages;
wenzelm
parents: 2902
diff changeset
   154
echo
01d24f98528f improved messages;
wenzelm
parents: 2902
diff changeset
   155
echo -n "Finished at "; date
01d24f98528f improved messages;
wenzelm
parents: 2902
diff changeset
   156
echo