equal
deleted
inserted
replaced
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # |
4 # |
5 # mk - build Pure Isabelle. |
5 # mk - build Pure Isabelle. |
6 # |
6 # |
7 # Notes: |
7 # Assumes to be called via Isabelle make utility (cf. IsaMakefile). |
8 # (1) make sure the Isabelle bin dir is in PATH (try 'which isabelle') |
|
9 # (2) make sure etc/settings are appropriate |
|
10 # (3) then cd here and run ./mk |
|
11 |
8 |
12 |
9 |
13 ## diagnostics |
10 ## diagnostics |
14 |
11 |
15 function fail() |
12 function fail() |
19 } |
16 } |
20 |
17 |
21 |
18 |
22 ## main |
19 ## main |
23 |
20 |
24 ML_SYSTEM=$(isatool getenv ML_SYSTEM) |
|
25 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-) |
21 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-) |
26 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to build Isabelle." |
22 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Probably not run via 'isatool make'?." |
27 |
23 |
28 COMPAT="" |
24 COMPAT="" |
29 [ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML" |
25 [ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML" |
30 [ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML" |
26 [ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML" |
31 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!" |
27 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!" |
32 |
28 |
33 exec isabelle \ |
29 $ISABELLE_HOME/bin/isabelle \ |
34 -e "val ml_system = \"$ML_SYSTEM\";" \ |
30 -e "val ml_system = \"$ML_SYSTEM\";" \ |
35 -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \ |
31 -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \ |
36 -cq SYSTEM Pure |
32 -cq SYSTEM Pure |
|
33 |
|
34 chmod -w $ISABELLE_OUTPUT_DIR/Pure |