author | lcp |
Wed, 15 Mar 1995 10:59:20 +0100 | |
changeset 956 | cc929b9ddc80 |
parent 917 | bd26f536e1fe |
child 993 | eab3015d97f0 |
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) |
|
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
21 |
THYS = ZF.thy upair.thy subset.thy pair.thy domrange.thy \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
22 |
func.thy AC.thy simpdata.thy equalities.thy Bool.thy \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
23 |
Sum.thy QPair.thy mono.thy Fixedpt.thy ind_syntax.thy add_ind_def.thy \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
24 |
constructor.thy intr_elim.thy indrule.thy Inductive.thy \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
25 |
Perm.thy Rel.thy EquivClass.thy Trancl.thy \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
26 |
WF.thy Order.thy Ordinal.thy Epsilon.thy Arith.thy Univ.thy \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
27 |
QUniv.thy Datatype.thy OrderArith.thy OrderType.thy \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
28 |
Cardinal.thy CardinalArith.thy Cardinal_AC.thy InfDatatype.thy \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
29 |
Zorn.thy Nat.thy Finite.thy List.thy |
0 | 30 |
|
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
31 |
FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML $(THYS) $(THYS:.thy=.ML) |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
32 |
|
102 | 33 |
|
0 | 34 |
#Uses cp rather than make_database because Poly/ML allows only 3 levels |
35 |
$(BIN)/ZF: $(BIN)/FOL $(FILES) |
|
36 |
case "$(COMP)" in \ |
|
37 |
poly*) cp $(BIN)/FOL $(BIN)/ZF;\ |
|
956
cc929b9ddc80
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
917
diff
changeset
|
38 |
echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/ZF ;;\ |
cc929b9ddc80
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
917
diff
changeset
|
39 |
sml*) echo 'exit_use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\ |
435 | 40 |
*) echo Bad value for ISABELLECOMP: \ |
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
41 |
$(COMP) is not poly or sml; exit 1;;\ |
0 | 42 |
esac |
43 |
||
44 |
$(BIN)/FOL: |
|
45 |
cd ../FOL; $(MAKE) |
|
46 |
||
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
47 |
#### Testing of ZF |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
48 |
|
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
49 |
#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
|
50 |
LOGIC:sh=case $ISABELLECOMP in \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
51 |
poly*) echo "$ISABELLECOMP $ISABELLEBIN/ZF" ;;\ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
52 |
sml*) echo "$ISABELLEBIN/ZF" ;;\ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
53 |
*) echo "echo Bad value for ISABELLECOMP: \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
54 |
$ISABELLEBIN is not poly or sml; exit 1" ;;\ |
0 | 55 |
esac |
56 |
||
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
57 |
##IMP-semantics example |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
58 |
IMP_THYS = IMP/Com.thy IMP/Denotation.thy IMP/Equiv.thy |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
59 |
IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML) |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
60 |
|
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
61 |
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
|
62 |
echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC) |
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
63 |
|
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
64 |
##Coinduction example |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
65 |
COIND_THYS = Coind/ECR.thy Coind/Language.thy\ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
66 |
Coind/MT.thy Coind/Map.thy Coind/Static.thy \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
67 |
Coind/Types.thy Coind/Values.thy |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
68 |
|
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
69 |
COIND_FILES = Coind/ROOT.ML Coind/BCR.thy Coind/Dynamic.thy \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
70 |
$(COIND_THYS) $(COIND_THYS:.thy=.ML) |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
71 |
|
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
72 |
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
|
73 |
echo 'exit_use"Coind/ROOT.ML";quit();' | $(LOGIC) |
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
74 |
|
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
75 |
##Miscellaneous examples |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
76 |
EX_THYS = ex/Ramsey.thy ex/Integ.thy ex/twos_compl.thy ex/Bin.thy \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
77 |
ex/BT.thy ex/Term.thy ex/TF.thy ex/Ntree.thy \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
78 |
ex/Brouwer.thy ex/Data.thy ex/Enum.thy \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
79 |
ex/Rmap.thy ex/PropLog.thy ex/ListN.thy ex/Acc.thy \ |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
80 |
ex/Comb.thy ex/Primrec.thy ex/LList.thy ex/CoUnit.thy |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
81 |
EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
82 |
|
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
83 |
#Test ZF by loading the examples in directory ex |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
84 |
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
|
85 |
echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC) |
917
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
86 |
|
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
87 |
#Full test. |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
88 |
test: $(BIN)/ZF IMP Coind ex |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
89 |
echo 'Test examples ran successfully' > test |
bd26f536e1fe
Re-organised to perform the tests independently. Now test
lcp
parents:
798
diff
changeset
|
90 |
|
0 | 91 |
.PRECIOUS: $(BIN)/FOL $(BIN)/ZF |