author | nipkow |
Wed, 08 Mar 1995 17:22:28 +0100 | |
changeset 228 | e2245da1b601 |
parent 221 | 14050d4d9b00 |
child 232 | e22d5a7f5f9f |
permissions | -rw-r--r-- |
0 | 1 |
######################################################################### |
2 |
# # |
|
3 |
# Makefile for Isabelle (HOL) # |
|
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 pure Isabelle (Pure) 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) |
|
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
21 |
THYS = HOL.thy Ord.thy Set.thy Fun.thy subset.thy \ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
22 |
equalities.thy Prod.thy Trancl.thy Sum.thy WF.thy \ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
23 |
mono.thy Lfp.thy Gfp.thy Nat.thy Inductive.thy \ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
24 |
Finite.thy Arith.thy Sexp.thy Univ.thy List.thy |
133
4a2bb4fbc168
Added IMP, which necessiated changes in intr_elim.tex (mk_cases).
nipkow
parents:
129
diff
changeset
|
25 |
|
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
26 |
FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML\ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
27 |
ind_syntax.ML indrule.ML intr_elim.ML simpdata.ML\ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
28 |
subtype.ML thy_syntax.ML ../Pure/section_utils.ML\ |
228
e2245da1b601
Added dependencies on ../Provers/hypsubst.ML and removed those on
nipkow
parents:
221
diff
changeset
|
29 |
../Provers/hypsubst.ML ../Provers/classical.ML\ |
e2245da1b601
Added dependencies on ../Provers/hypsubst.ML and removed those on
nipkow
parents:
221
diff
changeset
|
30 |
../Provers/simplifier.ML ../Provers/splitter.ML\ |
e2245da1b601
Added dependencies on ../Provers/hypsubst.ML and removed those on
nipkow
parents:
221
diff
changeset
|
31 |
$(THYS) $(THYS:.thy=.ML) |
16 | 32 |
|
0 | 33 |
$(BIN)/HOL: $(BIN)/Pure $(FILES) |
78 | 34 |
if [ -d $${ISABELLEBIN:?}/Pure ];\ |
35 |
then echo Bad value for ISABELLEBIN: \ |
|
36 |
$(BIN) is the Isabelle source directory; \ |
|
37 |
exit 1; \ |
|
38 |
fi;\ |
|
0 | 39 |
case "$(COMP)" in \ |
40 |
poly*) echo 'make_database"$(BIN)/HOL"; quit();' \ |
|
41 |
| $(COMP) $(BIN)/Pure;\ |
|
42 |
echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/HOL ;;\ |
|
43 |
sml*) echo 'use"ROOT.ML"; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure ;;\ |
|
78 | 44 |
*) echo Bad value for ISABELLECOMP: \ |
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
45 |
$(COMP) is not poly or sml; exit 1;;\ |
0 | 46 |
esac |
47 |
||
48 |
$(BIN)/Pure: |
|
49 |
cd ../Pure; $(MAKE) |
|
50 |
||
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
51 |
#### Testing of HOL |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
52 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
53 |
#A macro referring to the object-logic (depends on ML compiler) |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
54 |
LOGIC:sh=case $ISABELLECOMP in \ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
55 |
poly*) echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
56 |
sml*) echo "$ISABELLEBIN/HOL" ;;\ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
57 |
*) echo "echo Bad value for ISABELLECOMP: \ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
58 |
$ISABELLEBIN is not poly or sml; exit 1" ;;\ |
0 | 59 |
esac |
60 |
||
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
61 |
##IMP-semantics example |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
62 |
IMP_THYS = IMP/Com.thy IMP/Denotation.thy IMP/Equiv.thy IMP/Properties.thy |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
63 |
IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML) |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
64 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
65 |
IMP: $(BIN)/HOL $(IMP_FILES) |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
66 |
echo 'use"IMP/ROOT.ML";quit();' | $(LOGIC) |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
67 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
68 |
##The integers in HOL |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
69 |
INTEG_THYS = Integ/Relation.thy Integ/Equiv.thy Integ/Integ.thy |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
70 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
71 |
INTEG_FILES = Integ/ROOT.ML $(INTEG_THYS) $(INTEG_THYS:.thy=.ML) |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
72 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
73 |
Integ: $(BIN)/HOL $(INTEG_FILES) |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
74 |
echo 'use"Integ/ROOT.ML";quit();' | $(LOGIC) |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
75 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
76 |
##I/O Automata |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
77 |
IOA_THYS = IOA/example/Action.thy IOA/example/Channels.thy\ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
78 |
IOA/example/Correctness.thy IOA/example/Impl.thy \ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
79 |
IOA/example/Lemmas.thy IOA/example/Multiset.thy \ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
80 |
IOA/example/Receiver.thy IOA/example/Sender.thy \ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
81 |
IOA/meta_theory/Asig.thy IOA/meta_theory/IOA.thy \ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
82 |
IOA/meta_theory/Option.thy IOA/meta_theory/Solve.thy |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
83 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
84 |
IOA_FILES = IOA/ROOT.ML IOA/example/Packet.thy IOA/example/Spec.thy\ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
85 |
$(IOA_THYS) $(IOA_THYS:.thy=.ML) |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
86 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
87 |
IOA: $(BIN)/HOL $(IOA_FILES) |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
88 |
echo 'use"IOA/ROOT.ML";quit();' | $(LOGIC) |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
89 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
90 |
##Properties of substitutions |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
91 |
SUBST_THYS = Subst/AList.thy Subst/Setplus.thy\ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
92 |
Subst/Subst.thy Subst/Unifier.thy\ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
93 |
Subst/UTerm.thy Subst/UTLemmas.thy |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
94 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
95 |
SUBST_FILES = Subst/ROOT.ML $(SUBST_THYS) $(SUBST_THYS:.thy=.ML) |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
96 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
97 |
Subst: $(BIN)/HOL $(SUBST_FILES) |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
98 |
echo 'use"Subst/ROOT.ML";quit();' | $(LOGIC) |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
99 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
100 |
##Miscellaneous examples |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
101 |
EX_THYS = ex/LexProd.thy ex/MT.thy ex/Acc.thy \ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
102 |
ex/PropLog.thy ex/Puzzle.thy ex/Qsort.thy ex/LList.thy \ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
103 |
ex/Rec.thy ex/Simult.thy ex/Term.thy ex/String.thy |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
104 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
105 |
EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
106 |
ex/set.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
107 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
108 |
ex: $(BIN)/HOL $(EX_FILES) |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
109 |
echo 'use"ex/ROOT.ML";quit();' | $(LOGIC) |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
110 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
111 |
#Full test. |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
112 |
test: $(BIN)/HOL IMP Integ IOA Subst ex |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
113 |
echo 'Test examples ran successfully' > test |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
114 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
115 |
.PRECIOUS: $(BIN)/Pure $(BIN)/HOL |