4 # IsaMakefile for HOLCF
9 OUT = $(ISABELLE_OUTPUT_DIR)
11 THYS = Porder.thy Porder0.thy Pcpo.thy \
12 Fun1.thy Fun2.thy Fun3.thy \
13 Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
14 Cprod1.thy Cprod2.thy Cprod3.thy \
15 Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
16 Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
17 Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy \
19 Discrete0.thy Discrete1.thy Discrete.thy\
20 Lift1.thy Lift2.thy Lift3.thy HOLCF.thy
24 FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) \
25 ax_ops/holcflogic.ML ax_ops/thy_axioms.ML \
26 ax_ops/thy_ops.ML ax_ops/thy_syntax.ML \
27 domain/library.ML domain/syntax.ML domain/axioms.ML \
28 domain/theorems.ML domain/extender.ML domain/interface.ML
30 $(OUT)/HOLCF: $(OUT)/HOL $(FILES)
31 @$(ISATOOL) usedir -b $(OUT)/HOL HOLCF
35 @cd ../HOL; $(ISATOOL) make
39 #### Tests and examples
41 ## IOA meta theory and examples
44 IOA_FILES = IOA/ROOT.ML IOA/meta_theory/Traces.thy \
45 IOA/meta_theory/Asig.ML IOA/meta_theory/Asig.thy \
46 IOA/meta_theory/CompoScheds.thy IOA/meta_theory/CompoExecs.ML \
47 IOA/meta_theory/CompoTraces.thy IOA/meta_theory/CompoScheds.ML \
48 IOA/meta_theory/CompoTraces.ML IOA/meta_theory/Sequence.ML \
49 IOA/meta_theory/Seq.thy IOA/meta_theory/RefCorrectness.thy \
50 IOA/meta_theory/Automata.thy IOA/meta_theory/Traces.ML \
51 IOA/meta_theory/Seq.ML IOA/meta_theory/RefMappings.ML \
52 IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/ShortExecutions.ML \
53 IOA/meta_theory/IOA.thy IOA/meta_theory/IOA.ML \
54 IOA/meta_theory/Sequence.thy IOA/meta_theory/Automata.ML \
55 IOA/meta_theory/CompoExecs.thy IOA/meta_theory/RefMappings.thy \
56 IOA/meta_theory/RefCorrectness.ML IOA/meta_theory/Compositionality.ML \
57 IOA/meta_theory/Compositionality.thy
60 IOA_ABP_FILES = IOA/ABP/Abschannel.thy \
61 IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.ML \
62 IOA/ABP/Action.thy IOA/ABP/Check.ML \
63 IOA/ABP/Correctness.ML IOA/ABP/Correctness.thy \
64 IOA/ABP/Env.thy IOA/ABP/Impl.thy \
65 IOA/ABP/Impl_finite.thy IOA/ABP/Lemmas.ML \
66 IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \
67 IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy \
68 IOA/ABP/Sender.thy IOA/ABP/Spec.thy
71 IOA_NTP_FILES = IOA/NTP/Abschannel.ML \
72 IOA/NTP/Abschannel.thy IOA/NTP/Action.ML \
73 IOA/NTP/Action.thy IOA/NTP/Correctness.ML \
74 IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \
75 IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML \
76 IOA/NTP/Lemmas.thy IOA/NTP/Multiset.ML \
77 IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \
78 IOA/NTP/Packet.thy IOA/NTP/ROOT.ML \
79 IOA/NTP/Receiver.ML IOA/NTP/Receiver.thy \
80 IOA/NTP/Sender.ML IOA/NTP/Sender.thy \
84 IOA: $(OUT)/HOLCF $(IOA_FILES)
85 @cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA
87 IOA_ABP: $(OUT)/IOA $(IOA_ABP_FILES)
88 @cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP
90 IOA_NTP: $(OUT)/IOA $(IOA_NTP_FILES)
91 @cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP
95 IMP_THYS = IMP/Denotational.thy
96 IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
98 IMP: $(OUT)/HOLCF $(IMP_FILES)
99 @$(ISATOOL) usedir $(OUT)/HOLCF IMP
101 ## Miscellaneous examples
103 EX_THYS = ex/Classlib.thy ex/Witness.thy\
104 ex/Dnat.thy ex/Dlist.thy ex/Stream.thy\
105 ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy\
106 ex/Hoare.thy ex/Loop.thy
108 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
110 EX: ex/ROOT.ML $(EX_FILES)
111 @$(ISATOOL) usedir $(OUT)/HOLCF ex
115 test: $(OUT)/HOLCF IOA IOA_ABP IOA_NTP IMP EX
116 echo 'Test examples ran successfully' > test
118 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF