author | lcp |
Tue, 21 Jun 1994 17:20:34 +0200 | |
changeset 435 | ca5356bd315a |
parent 363 | 1180a3c5479e |
child 467 | 92868dab2939 |
permissions | -rw-r--r-- |
0 | 1 |
######################################################################### |
2 |
# # |
|
3 |
# Makefile for Isabelle (ZF) # |
|
4 |
# # |
|
5 |
######################################################################### |
|
6 |
||
7 |
#To make the system, cd to this directory and type |
|
8 |
# make -f Makefile |
|
9 |
#To make the system and test it on standard examples, type |
|
10 |
# make -f Makefile test |
|
11 |
||
12 |
#Environment variable ISABELLECOMP specifies the compiler. |
|
13 |
#Environment variable ISABELLEBIN specifies the destination directory. |
|
14 |
#For Poly/ML, ISABELLEBIN must begin with a / |
|
15 |
||
16 |
#Makes FOL if this file is ABSENT -- but not |
|
17 |
#if it is out of date, since this Makefile does not know its dependencies! |
|
18 |
||
19 |
BIN = $(ISABELLEBIN) |
|
20 |
COMP = $(ISABELLECOMP) |
|
339 | 21 |
FILES = ROOT.ML ZF.thy ZF.ML upair.ML subset.ML pair.ML domrange.ML \ |
22 |
func.ML simpdata.ML Bool.thy Bool.ML \ |
|
342 | 23 |
Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \ |
92 | 24 |
ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.ML \ |
435 | 25 |
equalities.ML Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \ |
26 |
WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \ |
|
27 |
OrderType.thy OrderType.ML OrderArith.thy OrderArith.ML \ |
|
28 |
Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \ |
|
29 |
Nat.thy Nat.ML \ |
|
339 | 30 |
Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \ |
342 | 31 |
QUniv.thy QUniv.ML constructor.ML Datatype.ML \ |
363 | 32 |
Fin.ML List.ML ListFn.thy ListFn.ML |
0 | 33 |
|
342 | 34 |
EX_FILES = ex/ROOT.ML ex/Acc.ML ex/Bin.ML ex/BinFn.ML ex/BinFn.thy\ |
35 |
ex/BT.ML ex/BT_Fn.ML ex/BT_Fn.thy ex/Comb.ML\ |
|
363 | 36 |
ex/Contract0.ML ex/Contract0.thy ex/CoUnit.ML ex/Data.ML\ |
342 | 37 |
ex/Enum.ML ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\ |
363 | 38 |
ex/ListN.ML ex/LList.ML ex/LList_Eq.ML ex/LListFn.ML ex/LListFn.thy\ |
342 | 39 |
ex/misc.ML ex/ParContract.ML ex/Primrec0.ML ex/Primrec0.thy\ |
40 |
ex/Prop.ML ex/PropLog.ML ex/PropLog.thy ex/Ramsey.ML ex/Ramsey.thy\ |
|
41 |
ex/Rmap.ML ex/Term.ML ex/TermFn.ML ex/TermFn.thy ex/TF.ML\ |
|
339 | 42 |
ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML |
102 | 43 |
|
0 | 44 |
#Uses cp rather than make_database because Poly/ML allows only 3 levels |
45 |
$(BIN)/ZF: $(BIN)/FOL $(FILES) |
|
46 |
case "$(COMP)" in \ |
|
47 |
poly*) cp $(BIN)/FOL $(BIN)/ZF;\ |
|
82
b9ac34abc054
no longer specifies "-h 15000". Instead $ISABELLECOMP should
lcp
parents:
75
diff
changeset
|
48 |
echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\ |
0 | 49 |
sml*) echo 'use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\ |
435 | 50 |
*) echo Bad value for ISABELLECOMP: \ |
51 |
$(COMP) is not poly or sml;;\ |
|
0 | 52 |
esac |
53 |
||
54 |
$(BIN)/FOL: |
|
55 |
cd ../FOL; $(MAKE) |
|
56 |
||
102 | 57 |
test: ex/ROOT.ML $(BIN)/ZF $(EX_FILES) |
0 | 58 |
case "$(COMP)" in \ |
82
b9ac34abc054
no longer specifies "-h 15000". Instead $ISABELLECOMP should
lcp
parents:
75
diff
changeset
|
59 |
poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/ZF ;;\ |
0 | 60 |
sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/ZF;;\ |
435 | 61 |
*) echo Bad value for ISABELLECOMP: \ |
62 |
$(COMP) is not poly or sml;;\ |
|
0 | 63 |
esac |
64 |
||
65 |
.PRECIOUS: $(BIN)/FOL $(BIN)/ZF |