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