author | clasohm |
Fri, 17 Nov 1995 13:22:50 +0100 | |
changeset 1341 | 69fec018854c |
parent 1296 | ae31bb7774a7 |
child 1350 | 5bf4a54ba25f |
permissions | -rw-r--r-- |
1296 | 1 |
# $Id$ |
0 | 2 |
######################################################################### |
3 |
# # |
|
4 |
# Makefile for Isabelle (ZF) # |
|
5 |
# # |
|
6 |
######################################################################### |
|
7 |
||
8 |
#To make the system, cd to this directory and type |
|
1296 | 9 |
# make |
0 | 10 |
#To make the system and test it on standard examples, type |
1296 | 11 |
# make test |
12 |
#To generate HTML files for every theory, set the environment variable |
|
13 |
#MAKE_HTML or add the parameter "MAKE_HTML=". |
|
0 | 14 |
|
15 |
#Environment variable ISABELLECOMP specifies the compiler. |
|
16 |
#Environment variable ISABELLEBIN specifies the destination directory. |
|
17 |
#For Poly/ML, ISABELLEBIN must begin with a / |
|
18 |
||
19 |
#Makes FOL if this file is ABSENT -- but not |
|
20 |
#if it is out of date, since this Makefile does not know its dependencies! |
|
21 |
||
22 |
BIN = $(ISABELLEBIN) |
|
23 |
COMP = $(ISABELLECOMP) |
|
993
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
24 |
NAMES = ZF upair subset pair domrange \ |
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
25 |
func AC simpdata equalities Bool \ |
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
26 |
Sum QPair mono Fixedpt ind_syntax add_ind_def \ |
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
27 |
constructor intr_elim indrule Inductive Perm Rel EquivClass Trancl \ |
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
28 |
WF Order Ordinal Epsilon Arith Univ \ |
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
29 |
QUniv Datatype OrderArith OrderType \ |
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
30 |
Cardinal CardinalArith Cardinal_AC InfDatatype \ |
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
31 |
Zorn Nat Finite List |
0 | 32 |
|
993
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
33 |
FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML \ |
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
34 |
$(NAMES:%=%.thy) $(NAMES:%=%.ML) |
102 | 35 |
|
0 | 36 |
#Uses cp rather than make_database because Poly/ML allows only 3 levels |
37 |
$(BIN)/ZF: $(BIN)/FOL $(FILES) |
|
38 |
case "$(COMP)" in \ |
|
39 |
poly*) cp $(BIN)/FOL $(BIN)/ZF;\ |
|
1296 | 40 |
if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
41 |
then echo 'open PolyML; init_html (); exit_use"ROOT";' \ |
|
42 |
| $(COMP) $(BIN)/ZF;\ |
|
43 |
else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/ZF;\ |
|
44 |
fi;;\ |
|
45 |
sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
|
46 |
then echo 'init_html (); exit_use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;\ |
|
47 |
else echo 'exit_use"ROOT.ML"; xML"$(BIN)/ZF" banner;' \ |
|
48 |
| $(BIN)/FOL;\ |
|
49 |
fi;;\ |
|
435 | 50 |
*) echo Bad value for ISABELLECOMP: \ |
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
51 |
$(COMP) is not poly or sml; exit 1;;\ |
0 | 52 |
esac |
53 |
||
54 |
$(BIN)/FOL: |
|
55 |
cd ../FOL; $(MAKE) |
|
56 |
||
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
57 |
#### Testing of ZF |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
58 |
|
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
59 |
#A macro referring to the object-logic (depends on ML compiler) |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
60 |
LOGIC:sh=case $ISABELLECOMP in \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
61 |
poly*) echo "$ISABELLECOMP $ISABELLEBIN/ZF" ;;\ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
62 |
sml*) echo "$ISABELLEBIN/ZF" ;;\ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
63 |
*) echo "echo Bad value for ISABELLECOMP: \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
64 |
$ISABELLEBIN is not poly or sml; exit 1" ;;\ |
0 | 65 |
esac |
66 |
||
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
67 |
##IMP-semantics example |
993
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
68 |
IMP_NAMES = Com Denotation Equiv |
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
69 |
IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML) |
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
70 |
|
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
71 |
IMP: $(BIN)/ZF $(IMP_FILES) |
956
cc929b9ddc80
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
917
diff
changeset
|
72 |
echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC) |
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
73 |
|
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
74 |
##Coinduction example |
993
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
75 |
COIND_NAMES = ECR Language MT Map Static Types Values |
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
76 |
|
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
77 |
COIND_FILES = Coind/ROOT.ML Coind/BCR.thy Coind/Dynamic.thy \ |
993
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
78 |
$(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML) |
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
79 |
|
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
80 |
Coind: $(BIN)/ZF $(COIND_FILES) |
956
cc929b9ddc80
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
917
diff
changeset
|
81 |
echo 'exit_use"Coind/ROOT.ML";quit();' | $(LOGIC) |
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
82 |
|
993
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
83 |
##AC examples |
1199 | 84 |
AC_NAMES = AC_Equiv OrdQuant Transrec2 Cardinal_aux \ |
85 |
AC15_WO6 AC16_WO4 AC16_lemmas AC17_AC1 AC18_AC19 AC1_WO2 \ |
|
86 |
DC DC_lemmas HH Hartog WO1_AC \ |
|
87 |
WO2_AC16 WO6_WO1 WO_AC first recfunAC16 rel_is_fun |
|
993
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
88 |
|
1199 | 89 |
AC_FILES = AC/ROOT.ML AC/AC0_AC1.ML AC/AC10_AC15.ML AC/AC1_AC17.ML \ |
90 |
AC/AC2_AC6.ML AC/AC7_AC9.ML \ |
|
91 |
AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML \ |
|
92 |
$(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML) |
|
993
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
93 |
|
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
94 |
AC: $(BIN)/ZF $(AC_FILES) |
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
95 |
echo 'exit_use"AC/ROOT.ML";quit();' | $(LOGIC) |
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
96 |
|
1059 | 97 |
##Residuals example |
98 |
||
99 |
RESID_NAMES = Confluence Redex SubUnion Conversion Reduction Substitution \ |
|
100 |
Cube Residuals Terms |
|
101 |
||
102 |
RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) \ |
|
103 |
$(RESID_NAMES:%=Resid/%.ML) |
|
104 |
||
105 |
Resid: $(BIN)/ZF $(RESID_FILES) |
|
106 |
echo 'exit_use"Resid/ROOT.ML";quit();' | $(LOGIC) |
|
107 |
||
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
108 |
##Miscellaneous examples |
1282 | 109 |
EX_NAMES = Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \ |
110 |
Data Enum Rmap PropLog ListN Acc Comb Primrec LList CoUnit |
|
993
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
111 |
|
eab3015d97f0
Simplified using pattern replacements. Added the AC example.
lcp
parents:
956
diff
changeset
|
112 |
EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
113 |
|
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
114 |
#Test ZF by loading the examples in directory ex |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
115 |
ex: $(BIN)/ZF $(EX_FILES) |
956
cc929b9ddc80
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
917
diff
changeset
|
116 |
echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC) |
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
117 |
|
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
118 |
#Full test. |
1059 | 119 |
test: $(BIN)/ZF IMP Coind AC Resid ex |
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
120 |
echo 'Test examples ran successfully' > test |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
121 |
|
0 | 122 |
.PRECIOUS: $(BIN)/FOL $(BIN)/ZF |