src/Pure/mk
author wenzelm
Mon, 09 Dec 1996 16:09:02 +0100
changeset 2340 74a01a9f325d
parent 2339 2d5551c8dec0
child 2401 0293bc1cecfc
permissions -rwxr-xr-x
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     1
#!/bin/bash -norc
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     2
#
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     3
# $Id$
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     4
#
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     5
# mk - build Pure Isabelle.
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     6
#
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     7
# Notes:
2340
74a01a9f325d *** empty log message ***
wenzelm
parents: 2339
diff changeset
     8
#   (1) make sure the Isabelle bin dir is in PATH (try 'which isabelle')
74a01a9f325d *** empty log message ***
wenzelm
parents: 2339
diff changeset
     9
#   (2) make sure etc/settings are appropriate
74a01a9f325d *** empty log message ***
wenzelm
parents: 2339
diff changeset
    10
#   (3) then cd here and run ./mk
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    11
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    12
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    13
## diagnostics
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    14
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    15
function fail()
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    16
{
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    17
  echo "$1" >&2
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    18
  exit 2
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    19
}
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    20
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    21
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    22
## main
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    23
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    24
ML_SYSTEM=$(isatool getenv ML_SYSTEM)
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    25
ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    26
[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to build Isabelle."
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    27
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    28
COMPAT=""
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    29
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    30
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    31
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    32
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    33
exec isabelle -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" -cq SYSTEM Pure