author | lcp |
Fri, 12 Aug 1994 12:51:34 +0200 | |
changeset 516 | 1957113f0d7d |
parent 488 | 52f7447d4f1b |
child 530 | 2eb142800801 |
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 \ |
484 | 22 |
func.ML AC.thy AC.ML simpdata.ML Bool.thy Bool.ML \ |
342 | 23 |
Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \ |
516 | 24 |
ind_syntax.ML add_ind_def.thy add_ind_def.ML \ |
25 |
\ intr_elim.ML indrule.ML inductive.ML \ |
|
435 | 26 |
equalities.ML Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \ |
27 |
WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \ |
|
488 | 28 |
Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \ |
29 |
QUniv.thy QUniv.ML constructor.ML Datatype.thy Datatype.ML \ |
|
467 | 30 |
OrderArith.thy OrderArith.ML OrderType.thy OrderType.ML \ |
435 | 31 |
Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \ |
488 | 32 |
Cardinal_AC.thy Cardinal_AC.ML InfDatatype.thy InfDatatype.ML \ |
516 | 33 |
Zorn.thy Zorn.ML Nat.thy Nat.ML Finite.thy Finite.ML \ |
34 |
List.thy List.ML |
|
0 | 35 |
|
516 | 36 |
IMP_FILES = IMP/ROOT.ML IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\ |
37 |
IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy |
|
483 | 38 |
|
516 | 39 |
EX_FILES = ex/ROOT.ML ex/misc.ML ex/Ramsey.ML ex/Ramsey.thy\ |
40 |
ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\ |
|
41 |
ex/twos_compl.ML ex/Bin.thy ex/Bin.ML\ |
|
42 |
ex/BT.thy ex/BT.ML ex/Term.thy ex/Term.ML \ |
|
43 |
ex/TF.thy ex/TF.ML ex/Ntree.thy ex/Ntree.ML \ |
|
44 |
ex/Brouwer.thy ex/Brouwer.ML \ |
|
45 |
ex/Data.thy ex/Data.ML ex/Enum.thy ex/Enum.ML \ |
|
46 |
ex/Rmap.thy ex/Rmap.ML ex/PropLog.ML ex/PropLog.thy \ |
|
47 |
ex/ListN.thy ex/ListN.ML ex/Acc.thy ex/Acc.ML\ |
|
48 |
ex/Comb.thy ex/Comb.ML ex/Primrec.thy ex/Primrec.ML\ |
|
49 |
ex/LList.thy ex/LList.ML ex/CoUnit.thy ex/CoUnit.ML |
|
102 | 50 |
|
0 | 51 |
#Uses cp rather than make_database because Poly/ML allows only 3 levels |
52 |
$(BIN)/ZF: $(BIN)/FOL $(FILES) |
|
53 |
case "$(COMP)" in \ |
|
54 |
poly*) cp $(BIN)/FOL $(BIN)/ZF;\ |
|
82
b9ac34abc054
no longer specifies "-h 15000". Instead $ISABELLECOMP should
lcp
parents:
75
diff
changeset
|
55 |
echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\ |
0 | 56 |
sml*) echo 'use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\ |
435 | 57 |
*) echo Bad value for ISABELLECOMP: \ |
58 |
$(COMP) is not poly or sml;;\ |
|
0 | 59 |
esac |
60 |
||
61 |
$(BIN)/FOL: |
|
62 |
cd ../FOL; $(MAKE) |
|
63 |
||
488 | 64 |
#Directory IMP also tests the system |
65 |
#Load ex/ROOT.ML last since it creates the file "test" |
|
66 |
test: $(BIN)/ZF $(IMP_FILES) $(EX_FILES) |
|
0 | 67 |
case "$(COMP)" in \ |
483 | 68 |
poly*) echo 'use"IMP/ROOT.ML"; use"ex/ROOT.ML"; quit();' | \ |
69 |
$(COMP) $(BIN)/ZF ;;\ |
|
70 |
sml*) echo 'use"IMP/ROOT.ML"; use"ex/ROOT.ML";' | $(BIN)/ZF;;\ |
|
435 | 71 |
*) echo Bad value for ISABELLECOMP: \ |
72 |
$(COMP) is not poly or sml;;\ |
|
0 | 73 |
esac |
74 |
||
75 |
.PRECIOUS: $(BIN)/FOL $(BIN)/ZF |