author | lcp |
Thu, 10 Nov 1994 11:36:40 +0100 | |
changeset 700 | 31f50c1778ef |
parent 589 | 31847a7504ec |
child 798 | 31ec33d96231 |
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) |
|
530 | 21 |
FILES = ROOT.ML ZF.thy ZF.ML upair.thy upair.ML subset.thy subset.ML \ |
22 |
pair.thy pair.ML domrange.thy domrange.ML \ |
|
23 |
func.thy func.ML AC.thy AC.ML simpdata.thy simpdata.ML\ |
|
24 |
equalities.thy equalities.ML Bool.thy Bool.ML \ |
|
342 | 25 |
Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \ |
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
531
diff
changeset
|
26 |
../Pure/section_utils.ML ind_syntax.thy ind_syntax.ML \ |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
531
diff
changeset
|
27 |
add_ind_def.thy add_ind_def.ML \ |
531
e24f47f8938e
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
lcp
parents:
530
diff
changeset
|
28 |
intr_elim.thy intr_elim.ML indrule.thy indrule.ML \ |
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
531
diff
changeset
|
29 |
Inductive.thy Inductive.ML \ |
531
e24f47f8938e
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
lcp
parents:
530
diff
changeset
|
30 |
Perm.thy Perm.ML Rel.thy Rel.ML EquivClass.ML EquivClass.thy \ |
e24f47f8938e
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
lcp
parents:
530
diff
changeset
|
31 |
Trancl.thy Trancl.ML \ |
435 | 32 |
WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \ |
488 | 33 |
Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \ |
34 |
QUniv.thy QUniv.ML constructor.ML Datatype.thy Datatype.ML \ |
|
467 | 35 |
OrderArith.thy OrderArith.ML OrderType.thy OrderType.ML \ |
435 | 36 |
Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \ |
488 | 37 |
Cardinal_AC.thy Cardinal_AC.ML InfDatatype.thy InfDatatype.ML \ |
516 | 38 |
Zorn.thy Zorn.ML Nat.thy Nat.ML Finite.thy Finite.ML \ |
39 |
List.thy List.ML |
|
0 | 40 |
|
516 | 41 |
IMP_FILES = IMP/ROOT.ML IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\ |
42 |
IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy |
|
483 | 43 |
|
516 | 44 |
EX_FILES = ex/ROOT.ML ex/misc.ML ex/Ramsey.ML ex/Ramsey.thy\ |
531
e24f47f8938e
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
lcp
parents:
530
diff
changeset
|
45 |
ex/Integ.ML ex/Integ.thy\ |
589 | 46 |
ex/twos_compl.thy ex/twos_compl.ML ex/Bin.thy ex/Bin.ML\ |
516 | 47 |
ex/BT.thy ex/BT.ML ex/Term.thy ex/Term.ML \ |
48 |
ex/TF.thy ex/TF.ML ex/Ntree.thy ex/Ntree.ML \ |
|
49 |
ex/Brouwer.thy ex/Brouwer.ML \ |
|
50 |
ex/Data.thy ex/Data.ML ex/Enum.thy ex/Enum.ML \ |
|
51 |
ex/Rmap.thy ex/Rmap.ML ex/PropLog.ML ex/PropLog.thy \ |
|
52 |
ex/ListN.thy ex/ListN.ML ex/Acc.thy ex/Acc.ML\ |
|
53 |
ex/Comb.thy ex/Comb.ML ex/Primrec.thy ex/Primrec.ML\ |
|
54 |
ex/LList.thy ex/LList.ML ex/CoUnit.thy ex/CoUnit.ML |
|
102 | 55 |
|
0 | 56 |
#Uses cp rather than make_database because Poly/ML allows only 3 levels |
57 |
$(BIN)/ZF: $(BIN)/FOL $(FILES) |
|
58 |
case "$(COMP)" in \ |
|
59 |
poly*) cp $(BIN)/FOL $(BIN)/ZF;\ |
|
82
b9ac34abc054
no longer specifies "-h 15000". Instead $ISABELLECOMP should
lcp
parents:
75
diff
changeset
|
60 |
echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\ |
0 | 61 |
sml*) echo 'use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\ |
435 | 62 |
*) echo Bad value for ISABELLECOMP: \ |
63 |
$(COMP) is not poly or sml;;\ |
|
0 | 64 |
esac |
65 |
||
66 |
$(BIN)/FOL: |
|
67 |
cd ../FOL; $(MAKE) |
|
68 |
||
488 | 69 |
#Directory IMP also tests the system |
70 |
#Load ex/ROOT.ML last since it creates the file "test" |
|
71 |
test: $(BIN)/ZF $(IMP_FILES) $(EX_FILES) |
|
0 | 72 |
case "$(COMP)" in \ |
700
31f50c1778ef
HOL,ZF/Makefile: enclosed multiple "use" calls in parentheses. This
lcp
parents:
589
diff
changeset
|
73 |
poly*) echo '(use"IMP/ROOT.ML"; use"ex/ROOT.ML"); quit();' | \ |
483 | 74 |
$(COMP) $(BIN)/ZF ;;\ |
700
31f50c1778ef
HOL,ZF/Makefile: enclosed multiple "use" calls in parentheses. This
lcp
parents:
589
diff
changeset
|
75 |
sml*) echo '(use"IMP/ROOT.ML"; use"ex/ROOT.ML");' | $(BIN)/ZF;;\ |
435 | 76 |
*) echo Bad value for ISABELLECOMP: \ |
77 |
$(COMP) is not poly or sml;;\ |
|
0 | 78 |
esac |
79 |
||
80 |
.PRECIOUS: $(BIN)/FOL $(BIN)/ZF |