src/Pure/mk
author wenzelm
Tue, 07 Jan 1997 09:01:52 +0100
changeset 2474 9990f088d7ac
parent 2432 527b5f1b7520
child 2768 bc6d915b8019
permissions -rwxr-xr-x
minor tuning;
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
#
2432
527b5f1b7520 minor modifications to accomodate IsaMakefile;
wenzelm
parents: 2401
diff changeset
     7
# Assumes to be called via Isabelle make utility (cf. IsaMakefile).
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
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    12
function fail()
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    13
{
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    14
  echo "$1" >&2
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    15
  exit 2
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    16
}
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    17
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    18
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    19
## main
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    20
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    21
ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
2432
527b5f1b7520 minor modifications to accomodate IsaMakefile;
wenzelm
parents: 2401
diff changeset
    22
[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Probably not run via 'isatool make'?."
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    23
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    24
COMPAT=""
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    25
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    26
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    27
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    28
2474
9990f088d7ac minor tuning;
wenzelm
parents: 2432
diff changeset
    29
$ISABELLE \
2401
0293bc1cecfc now passes ML_SYSTEM as ml_system;
wenzelm
parents: 2340
diff changeset
    30
  -e "val ml_system = \"$ML_SYSTEM\";" \
0293bc1cecfc now passes ML_SYSTEM as ml_system;
wenzelm
parents: 2340
diff changeset
    31
  -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
0293bc1cecfc now passes ML_SYSTEM as ml_system;
wenzelm
parents: 2340
diff changeset
    32
  -cq SYSTEM Pure
2432
527b5f1b7520 minor modifications to accomodate IsaMakefile;
wenzelm
parents: 2401
diff changeset
    33
527b5f1b7520 minor modifications to accomodate IsaMakefile;
wenzelm
parents: 2401
diff changeset
    34
chmod -w $ISABELLE_OUTPUT_DIR/Pure