author | wenzelm |
Tue, 06 May 1997 15:27:35 +0200 | |
changeset 3118 | 24dae6222579 |
parent 3081 | 71c54eb8ed1d |
child 3190 | 5aa3756a4bf2 |
permissions | -rw-r--r-- |
wenzelm@2494 | 1 |
# |
wenzelm@2494 | 2 |
# $Id$ |
wenzelm@2494 | 3 |
# |
wenzelm@2494 | 4 |
# IsaMakefile for HOLCF |
wenzelm@2494 | 5 |
# |
wenzelm@2494 | 6 |
|
wenzelm@2494 | 7 |
#### Base system |
wenzelm@2494 | 8 |
|
wenzelm@3118 | 9 |
OUT = $(ISABELLE_OUTPUT) |
wenzelm@2494 | 10 |
|
slotosch@2640 | 11 |
THYS = Porder.thy Porder0.thy Pcpo.thy \ |
wenzelm@2494 | 12 |
Fun1.thy Fun2.thy Fun3.thy \ |
wenzelm@2494 | 13 |
Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \ |
wenzelm@2494 | 14 |
Cprod1.thy Cprod2.thy Cprod3.thy \ |
wenzelm@2494 | 15 |
Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \ |
wenzelm@2494 | 16 |
Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \ |
slotosch@2640 | 17 |
Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy \ |
slotosch@2640 | 18 |
One.thy Tr.thy\ |
nipkow@2841 | 19 |
Discrete0.thy Discrete1.thy Discrete.thy\ |
oheimb@3028 | 20 |
Lift1.thy Lift2.thy Lift3.thy HOLCF.thy |
wenzelm@2494 | 21 |
|
slotosch@2640 | 22 |
ONLYTHYS = Lift.thy |
slotosch@2640 | 23 |
|
oheimb@3028 | 24 |
FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) \ |
wenzelm@3043 | 25 |
ax_ops/holcflogic.ML ax_ops/thy_axioms.ML \ |
oheimb@3028 | 26 |
ax_ops/thy_ops.ML ax_ops/thy_syntax.ML \ |
oheimb@3028 | 27 |
domain/library.ML domain/syntax.ML domain/axioms.ML \ |
oheimb@3028 | 28 |
domain/theorems.ML domain/extender.ML domain/interface.ML |
wenzelm@2494 | 29 |
|
wenzelm@2494 | 30 |
$(OUT)/HOLCF: $(OUT)/HOL $(FILES) |
wenzelm@3057 | 31 |
@$(ISATOOL) usedir -b $(OUT)/HOL HOLCF |
wenzelm@2494 | 32 |
@chmod -w $@ |
wenzelm@2494 | 33 |
|
wenzelm@2494 | 34 |
$(OUT)/HOL: |
wenzelm@2494 | 35 |
@cd ../HOL; $(ISATOOL) make |
wenzelm@2494 | 36 |
|
wenzelm@2494 | 37 |
|
wenzelm@2494 | 38 |
|
wenzelm@2494 | 39 |
#### Tests and examples |
wenzelm@2494 | 40 |
|
mueller@3081 | 41 |
## IOA meta theory and examples |
mueller@3081 | 42 |
|
mueller@3081 | 43 |
|
mueller@3081 | 44 |
IOA_FILES = IOA/ROOT.ML IOA/meta_theory/Traces.thy \ |
mueller@3081 | 45 |
IOA/meta_theory/Asig.ML IOA/meta_theory/Asig.thy \ |
mueller@3081 | 46 |
IOA/meta_theory/CompoScheds.thy IOA/meta_theory/CompoExecs.ML \ |
mueller@3081 | 47 |
IOA/meta_theory/CompoTraces.thy IOA/meta_theory/CompoScheds.ML \ |
mueller@3081 | 48 |
IOA/meta_theory/CompoTraces.ML IOA/meta_theory/Sequence.ML \ |
mueller@3081 | 49 |
IOA/meta_theory/Seq.thy IOA/meta_theory/RefCorrectness.thy \ |
mueller@3081 | 50 |
IOA/meta_theory/Automata.thy IOA/meta_theory/Traces.ML \ |
mueller@3081 | 51 |
IOA/meta_theory/Seq.ML IOA/meta_theory/RefMappings.ML \ |
mueller@3081 | 52 |
IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/ShortExecutions.ML \ |
mueller@3081 | 53 |
IOA/meta_theory/IOA.thy IOA/meta_theory/IOA.ML \ |
mueller@3081 | 54 |
IOA/meta_theory/Sequence.thy IOA/meta_theory/Automata.ML \ |
mueller@3081 | 55 |
IOA/meta_theory/CompoExecs.thy IOA/meta_theory/RefMappings.thy \ |
mueller@3081 | 56 |
IOA/meta_theory/RefCorrectness.ML IOA/meta_theory/Compositionality.ML \ |
mueller@3081 | 57 |
IOA/meta_theory/Compositionality.thy |
mueller@3081 | 58 |
|
mueller@3081 | 59 |
|
mueller@3081 | 60 |
IOA_ABP_FILES = IOA/ABP/Abschannel.thy \ |
mueller@3081 | 61 |
IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.ML \ |
mueller@3081 | 62 |
IOA/ABP/Action.thy IOA/ABP/Check.ML \ |
mueller@3081 | 63 |
IOA/ABP/Correctness.ML IOA/ABP/Correctness.thy \ |
mueller@3081 | 64 |
IOA/ABP/Env.thy IOA/ABP/Impl.thy \ |
mueller@3081 | 65 |
IOA/ABP/Impl_finite.thy IOA/ABP/Lemmas.ML \ |
mueller@3081 | 66 |
IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \ |
mueller@3081 | 67 |
IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy \ |
mueller@3081 | 68 |
IOA/ABP/Sender.thy IOA/ABP/Spec.thy |
mueller@3081 | 69 |
|
mueller@3081 | 70 |
|
mueller@3081 | 71 |
IOA_NTP_FILES = IOA/NTP/Abschannel.ML \ |
mueller@3081 | 72 |
IOA/NTP/Abschannel.thy IOA/NTP/Action.ML \ |
mueller@3081 | 73 |
IOA/NTP/Action.thy IOA/NTP/Correctness.ML \ |
mueller@3081 | 74 |
IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \ |
mueller@3081 | 75 |
IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML \ |
mueller@3081 | 76 |
IOA/NTP/Lemmas.thy IOA/NTP/Multiset.ML \ |
mueller@3081 | 77 |
IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \ |
mueller@3081 | 78 |
IOA/NTP/Packet.thy IOA/NTP/ROOT.ML \ |
mueller@3081 | 79 |
IOA/NTP/Receiver.ML IOA/NTP/Receiver.thy \ |
mueller@3081 | 80 |
IOA/NTP/Sender.ML IOA/NTP/Sender.thy \ |
mueller@3081 | 81 |
IOA/NTP/Spec.thy |
mueller@3081 | 82 |
|
mueller@3081 | 83 |
|
mueller@3081 | 84 |
IOA: $(OUT)/HOLCF $(IOA_FILES) |
mueller@3081 | 85 |
@cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA |
mueller@3081 | 86 |
|
mueller@3081 | 87 |
IOA_ABP: $(OUT)/IOA $(IOA_ABP_FILES) |
mueller@3081 | 88 |
@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP |
mueller@3081 | 89 |
|
mueller@3081 | 90 |
IOA_NTP: $(OUT)/IOA $(IOA_NTP_FILES) |
mueller@3081 | 91 |
@cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP |
mueller@3081 | 92 |
|
nipkow@2797 | 93 |
## IMP |
nipkow@2797 | 94 |
|
nipkow@2797 | 95 |
IMP_THYS = IMP/Denotational.thy |
nipkow@2797 | 96 |
IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML) |
nipkow@2797 | 97 |
|
nipkow@2797 | 98 |
IMP: $(OUT)/HOLCF $(IMP_FILES) |
wenzelm@2828 | 99 |
@$(ISATOOL) usedir $(OUT)/HOLCF IMP |
nipkow@2797 | 100 |
|
wenzelm@2494 | 101 |
## Miscellaneous examples |
wenzelm@2494 | 102 |
|
oheimb@2571 | 103 |
EX_THYS = ex/Classlib.thy ex/Witness.thy\ |
oheimb@2571 | 104 |
ex/Dnat.thy ex/Dlist.thy ex/Stream.thy\ |
oheimb@2571 | 105 |
ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy\ |
oheimb@2571 | 106 |
ex/Hoare.thy ex/Loop.thy |
wenzelm@2494 | 107 |
|
wenzelm@2494 | 108 |
EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
wenzelm@2494 | 109 |
|
nipkow@2797 | 110 |
EX: ex/ROOT.ML $(EX_FILES) |
wenzelm@2828 | 111 |
@$(ISATOOL) usedir $(OUT)/HOLCF ex |
wenzelm@2494 | 112 |
|
nipkow@2797 | 113 |
## Full test |
nipkow@2797 | 114 |
|
mueller@3081 | 115 |
test: $(OUT)/HOLCF IOA IOA_ABP IOA_NTP IMP EX |
nipkow@2797 | 116 |
echo 'Test examples ran successfully' > test |
nipkow@2797 | 117 |
|
wenzelm@2494 | 118 |
.PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF |