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.
     1 #!/bin/bash -norc
     2 #
     3 # $Id$
     4 #
     5 # mk - build Pure Isabelle.
     6 #
     7 # Assumes to be called via Isabelle make utility (cf. IsaMakefile).
     8 
     9 
    10 ## diagnostics
    11 
    12 function fail()
    13 {
    14   echo "$1" >&2
    15   exit 2
    16 }
    17 
    18 
    19 ## main
    20 
    21 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
    22 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Probably not run via 'isatool make'?."
    23 
    24 COMPAT=""
    25 [ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
    26 [ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
    27 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
    28 
    29 $ISABELLE \
    30   -e "val ml_system = \"$ML_SYSTEM\";" \
    31   -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
    32   -cq RAW_ML_SYSTEM Pure
    33 
    34 chmod -w $ISABELLE_OUTPUT_DIR/Pure