| author | wenzelm |
| Tue, 06 May 1997 15:27:35 +0200 | |
| changeset 3118 | 24dae6222579 |
| parent 3056 | 200565f7592a |
| child 3505 | 1cb4ea47d967 |
| permissions | -rwxr-xr-x |
| wenzelm@3056 | 1 |
#!/bin/bash |
| 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@3056 | 22 |
[ -z "$ML_SYSTEM" ] && \ |
| wenzelm@3056 | 23 |
fail "Missing ML system settings! Probably not run via 'isatool make'?." |
| wenzelm@2339 | 24 |
|
| wenzelm@2339 | 25 |
COMPAT="" |
| wenzelm@2339 | 26 |
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML" |
| wenzelm@2339 | 27 |
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML" |
| wenzelm@2339 | 28 |
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!" |
| wenzelm@2339 | 29 |
|
| wenzelm@2474 | 30 |
$ISABELLE \ |
| wenzelm@2401 | 31 |
-e "val ml_system = \"$ML_SYSTEM\";" \ |
| wenzelm@2401 | 32 |
-e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \ |
| wenzelm@3056 | 33 |
-q RAW_ML_SYSTEM Pure |
| wenzelm@2432 | 34 |
|
| wenzelm@3118 | 35 |
chmod -w $ISABELLE_OUTPUT/Pure |