author | nipkow |
Thu, 21 Jul 1994 16:51:26 +0200 | |
changeset 483 | 4d1614d8f119 |
parent 467 | 92868dab2939 |
child 484 | 70b789956bd3 |
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 \ |
|
467 | 27 |
OrderArith.thy OrderArith.ML OrderType.thy OrderType.ML \ |
435 | 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 |
|
483 | 34 |
IMP_FILES = IMP/ROOT.ML IMP/Aexp.ML IMP/Aexp.thy IMP/Assign.ML IMP/Assign.thy\ |
35 |
IMP/Bexp.ML IMP/Bexp.thy IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\ |
|
36 |
IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy IMP/Evala0.thy\ |
|
37 |
IMP/Evala.ML IMP/Evala.thy IMP/Evalb0.thy IMP/Evalb.ML\ |
|
38 |
IMP/Evalb.thy IMP/Evalc0.thy IMP/Evalc.ML IMP/Evalc.thy |
|
39 |
||
342 | 40 |
EX_FILES = ex/ROOT.ML ex/Acc.ML ex/Bin.ML ex/BinFn.ML ex/BinFn.thy\ |
41 |
ex/BT.ML ex/BT_Fn.ML ex/BT_Fn.thy ex/Comb.ML\ |
|
363 | 42 |
ex/Contract0.ML ex/Contract0.thy ex/CoUnit.ML ex/Data.ML\ |
342 | 43 |
ex/Enum.ML ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\ |
363 | 44 |
ex/ListN.ML ex/LList.ML ex/LList_Eq.ML ex/LListFn.ML ex/LListFn.thy\ |
342 | 45 |
ex/misc.ML ex/ParContract.ML ex/Primrec0.ML ex/Primrec0.thy\ |
46 |
ex/Prop.ML ex/PropLog.ML ex/PropLog.thy ex/Ramsey.ML ex/Ramsey.thy\ |
|
47 |
ex/Rmap.ML ex/Term.ML ex/TermFn.ML ex/TermFn.thy ex/TF.ML\ |
|
339 | 48 |
ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML |
102 | 49 |
|
0 | 50 |
#Uses cp rather than make_database because Poly/ML allows only 3 levels |
51 |
$(BIN)/ZF: $(BIN)/FOL $(FILES) |
|
52 |
case "$(COMP)" in \ |
|
53 |
poly*) cp $(BIN)/FOL $(BIN)/ZF;\ |
|
82
b9ac34abc054
no longer specifies "-h 15000". Instead $ISABELLECOMP should
lcp
parents:
75
diff
changeset
|
54 |
echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\ |
0 | 55 |
sml*) echo 'use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\ |
435 | 56 |
*) echo Bad value for ISABELLECOMP: \ |
57 |
$(COMP) is not poly or sml;;\ |
|
0 | 58 |
esac |
59 |
||
60 |
$(BIN)/FOL: |
|
61 |
cd ../FOL; $(MAKE) |
|
62 |
||
483 | 63 |
test: ex/ROOT.ML $(BIN)/ZF $(IMP_FILES) $(EX_FILES) |
0 | 64 |
case "$(COMP)" in \ |
483 | 65 |
poly*) echo 'use"IMP/ROOT.ML"; use"ex/ROOT.ML"; quit();' | \ |
66 |
$(COMP) $(BIN)/ZF ;;\ |
|
67 |
sml*) echo 'use"IMP/ROOT.ML"; use"ex/ROOT.ML";' | $(BIN)/ZF;;\ |
|
435 | 68 |
*) echo Bad value for ISABELLECOMP: \ |
69 |
$(COMP) is not poly or sml;;\ |
|
0 | 70 |
esac |
71 |
||
72 |
.PRECIOUS: $(BIN)/FOL $(BIN)/ZF |