author | lcp |
Thu, 06 Apr 1995 11:18:02 +0200 | |
changeset 238 | efd07203ceec |
parent 232 | e22d5a7f5f9f |
child 250 | 093e273405f0 |
permissions | -rw-r--r-- |
238 | 1 |
# $Id$ |
0 | 2 |
######################################################################### |
3 |
# # |
|
4 |
# Makefile for Isabelle (HOL) # |
|
5 |
# # |
|
6 |
######################################################################### |
|
7 |
||
8 |
#To make the system, cd to this directory and type |
|
9 |
# make -f Makefile |
|
10 |
#To make the system and test it on standard examples, type |
|
11 |
# make -f Makefile test |
|
12 |
||
13 |
#Environment variable ISABELLECOMP specifies the compiler. |
|
14 |
#Environment variable ISABELLEBIN specifies the destination directory. |
|
15 |
#For Poly/ML, ISABELLEBIN must begin with a / |
|
16 |
||
17 |
#Makes pure Isabelle (Pure) if this file is ABSENT -- but not |
|
18 |
#if it is out of date, since this Makefile does not know its dependencies! |
|
19 |
||
20 |
BIN = $(ISABELLEBIN) |
|
21 |
COMP = $(ISABELLECOMP) |
|
238 | 22 |
NAMES = HOL Ord Set Fun subset equalities Prod Trancl Sum WF \ |
23 |
mono Lfp Gfp Nat Inductive Finite Arith Sexp Univ List |
|
133
4a2bb4fbc168
Added IMP, which necessiated changes in intr_elim.tex (mk_cases).
nipkow
parents:
129
diff
changeset
|
24 |
|
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
25 |
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
|
26 |
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
|
27 |
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
|
28 |
../Provers/hypsubst.ML ../Provers/classical.ML\ |
e2245da1b601
Added dependencies on ../Provers/hypsubst.ML and removed those on
nipkow
parents:
221
diff
changeset
|
29 |
../Provers/simplifier.ML ../Provers/splitter.ML\ |
238 | 30 |
$(NAMES:%=%.thy) $(NAMES:%=%.ML) |
16 | 31 |
|
0 | 32 |
$(BIN)/HOL: $(BIN)/Pure $(FILES) |
78 | 33 |
if [ -d $${ISABELLEBIN:?}/Pure ];\ |
34 |
then echo Bad value for ISABELLEBIN: \ |
|
35 |
$(BIN) is the Isabelle source directory; \ |
|
36 |
exit 1; \ |
|
37 |
fi;\ |
|
0 | 38 |
case "$(COMP)" in \ |
39 |
poly*) echo 'make_database"$(BIN)/HOL"; quit();' \ |
|
40 |
| $(COMP) $(BIN)/Pure;\ |
|
232
e22d5a7f5f9f
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
228
diff
changeset
|
41 |
echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/HOL ;;\ |
e22d5a7f5f9f
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
228
diff
changeset
|
42 |
sml*) echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure ;;\ |
78 | 43 |
*) echo Bad value for ISABELLECOMP: \ |
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
44 |
$(COMP) is not poly or sml; exit 1;;\ |
0 | 45 |
esac |
46 |
||
47 |
$(BIN)/Pure: |
|
48 |
cd ../Pure; $(MAKE) |
|
49 |
||
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
50 |
#### Testing of HOL |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
51 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
52 |
#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
|
53 |
LOGIC:sh=case $ISABELLECOMP in \ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
54 |
poly*) echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
55 |
sml*) echo "$ISABELLEBIN/HOL" ;;\ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
56 |
*) echo "echo Bad value for ISABELLECOMP: \ |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
57 |
$ISABELLEBIN is not poly or sml; exit 1" ;;\ |
0 | 58 |
esac |
59 |
||
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
60 |
##IMP-semantics example |
238 | 61 |
IMP_NAMES = Com Denotation Equiv Properties |
62 |
IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML) |
|
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
63 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
64 |
IMP: $(BIN)/HOL $(IMP_FILES) |
232
e22d5a7f5f9f
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
228
diff
changeset
|
65 |
echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC) |
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
66 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
67 |
##The integers in HOL |
238 | 68 |
INTEG_NAMES = Relation Equiv Integ |
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
69 |
|
238 | 70 |
INTEG_FILES = Integ/ROOT.ML \ |
71 |
$(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML) |
|
221
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) |
232
e22d5a7f5f9f
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
228
diff
changeset
|
74 |
echo 'exit_use"Integ/ROOT.ML";quit();' | $(LOGIC) |
221
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 |
238 | 77 |
IOA_EX_NAMES = Action Channels Correctness Impl Lemmas Multiset Receiver Sender |
78 |
IOA_MT_NAMES = Asig IOA Option Solve |
|
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
79 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
80 |
IOA_FILES = IOA/ROOT.ML IOA/example/Packet.thy IOA/example/Spec.thy\ |
238 | 81 |
$(IOA_EX_NAMES:%=IOA/example/%.thy) $(IOA_EX_NAMES:%=IOA/example/%.ML)\ |
82 |
$(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML) |
|
221
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: $(BIN)/HOL $(IOA_FILES) |
232
e22d5a7f5f9f
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
228
diff
changeset
|
85 |
echo 'exit_use"IOA/ROOT.ML";quit();' | $(LOGIC) |
221
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 |
##Properties of substitutions |
238 | 88 |
SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas |
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
89 |
|
238 | 90 |
SUBST_FILES = Subst/ROOT.ML \ |
91 |
$(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML) |
|
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
92 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
93 |
Subst: $(BIN)/HOL $(SUBST_FILES) |
232
e22d5a7f5f9f
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
228
diff
changeset
|
94 |
echo 'exit_use"Subst/ROOT.ML";quit();' | $(LOGIC) |
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
95 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
96 |
##Miscellaneous examples |
238 | 97 |
EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String |
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
98 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
99 |
EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ |
238 | 100 |
ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
221
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
101 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
102 |
ex: $(BIN)/HOL $(EX_FILES) |
232
e22d5a7f5f9f
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
228
diff
changeset
|
103 |
echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC) |
221
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 |
#Full test. |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
106 |
test: $(BIN)/HOL IMP Integ IOA Subst ex |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
107 |
echo 'Test examples ran successfully' > test |
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
108 |
|
14050d4d9b00
Re-organised to perform the tests independently. Now test
lcp
parents:
209
diff
changeset
|
109 |
.PRECIOUS: $(BIN)/Pure $(BIN)/HOL |