src/Pure/mk
author nipkow
Fri Mar 14 10:35:30 1997 +0100 (1997-03-14)
changeset 2792 6c17c5ec3d8b
parent 2768 bc6d915b8019
child 3056 200565f7592a
permissions -rwxr-xr-x
Avoid eta-contraction in the simplifier.
Instead the net needs to eta-contract the object.
Also added a special function loose_bvar1(i,t) in term.ML.
wenzelm@2339
     1
#!/bin/bash -norc
wenzelm@2339
     2
#
wenzelm@2339
     3
# $Id$
wenzelm@2339
     4
#
wenzelm@2339
     5
# mk - build Pure Isabelle.
wenzelm@2339
     6
#
wenzelm@2432
     7
# Assumes to be called via Isabelle make utility (cf. IsaMakefile).
wenzelm@2339
     8
wenzelm@2339
     9
wenzelm@2339
    10
## diagnostics
wenzelm@2339
    11
wenzelm@2339
    12
function fail()
wenzelm@2339
    13
{
wenzelm@2339
    14
  echo "$1" >&2
wenzelm@2339
    15
  exit 2
wenzelm@2339
    16
}
wenzelm@2339
    17
wenzelm@2339
    18
wenzelm@2339
    19
## main
wenzelm@2339
    20
wenzelm@2339
    21
ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
wenzelm@2432
    22
[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Probably not run via 'isatool make'?."
wenzelm@2339
    23
wenzelm@2339
    24
COMPAT=""
wenzelm@2339
    25
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
wenzelm@2339
    26
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
wenzelm@2339
    27
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
wenzelm@2339
    28
wenzelm@2474
    29
$ISABELLE \
wenzelm@2401
    30
  -e "val ml_system = \"$ML_SYSTEM\";" \
wenzelm@2401
    31
  -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
wenzelm@2768
    32
  -cq RAW_ML_SYSTEM Pure
wenzelm@2432
    33
wenzelm@2432
    34
chmod -w $ISABELLE_OUTPUT_DIR/Pure