src/HOLCF/IsaMakefile
author wenzelm
Fri Dec 19 10:18:58 1997 +0100 (1997-12-19)
changeset 4447 b7ee449eb345
parent 4129 2fd816aa6206
child 4518 74c01296e818
permissions -rw-r--r--
log files;
'clean' target;
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@4447
    10
LOG = $(OUT)/log
wenzelm@2494
    11
slotosch@2640
    12
THYS = Porder.thy Porder0.thy Pcpo.thy \
wenzelm@2494
    13
       Fun1.thy Fun2.thy Fun3.thy \
wenzelm@2494
    14
       Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
wenzelm@2494
    15
       Cprod1.thy Cprod2.thy Cprod3.thy \
wenzelm@2494
    16
       Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
wenzelm@2494
    17
       Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
slotosch@3350
    18
       Up1.thy Up2.thy Up3.thy Fix.thy \
slotosch@2640
    19
       One.thy Tr.thy\
nipkow@2841
    20
       Discrete0.thy Discrete1.thy Discrete.thy\
slotosch@3324
    21
       Lift1.thy Lift2.thy Lift3.thy Lift.thy HOLCF.thy
wenzelm@2494
    22
slotosch@3324
    23
ONLYTHYS = 
slotosch@2640
    24
wenzelm@4038
    25
FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) adm.ML \
wenzelm@4129
    26
	holcf_logic.ML cont_consts.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
wenzelm@2494
    33
$(OUT)/HOL:
wenzelm@2494
    34
	@cd ../HOL; $(ISATOOL) make
wenzelm@2494
    35
wenzelm@2494
    36
wenzelm@2494
    37
wenzelm@2494
    38
#### Tests and examples
wenzelm@2494
    39
mueller@3081
    40
## IOA meta theory and examples
mueller@3081
    41
mueller@3081
    42
mueller@3081
    43
IOA_FILES = IOA/ROOT.ML IOA/meta_theory/Traces.thy \
mueller@3081
    44
  IOA/meta_theory/Asig.ML IOA/meta_theory/Asig.thy \
mueller@3081
    45
  IOA/meta_theory/CompoScheds.thy IOA/meta_theory/CompoExecs.ML \
mueller@3081
    46
  IOA/meta_theory/CompoTraces.thy IOA/meta_theory/CompoScheds.ML \
mueller@3081
    47
  IOA/meta_theory/CompoTraces.ML IOA/meta_theory/Sequence.ML \
mueller@3081
    48
  IOA/meta_theory/Seq.thy IOA/meta_theory/RefCorrectness.thy \
mueller@3081
    49
  IOA/meta_theory/Automata.thy IOA/meta_theory/Traces.ML \
mueller@3081
    50
  IOA/meta_theory/Seq.ML IOA/meta_theory/RefMappings.ML \
mueller@3081
    51
  IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/ShortExecutions.ML \
mueller@3081
    52
  IOA/meta_theory/IOA.thy IOA/meta_theory/IOA.ML \
mueller@3081
    53
  IOA/meta_theory/Sequence.thy IOA/meta_theory/Automata.ML \
mueller@3081
    54
  IOA/meta_theory/CompoExecs.thy IOA/meta_theory/RefMappings.thy \
mueller@3081
    55
  IOA/meta_theory/RefCorrectness.ML IOA/meta_theory/Compositionality.ML \
mueller@3081
    56
  IOA/meta_theory/Compositionality.thy
mueller@3081
    57
mueller@3081
    58
mueller@3081
    59
IOA_ABP_FILES = IOA/ABP/Abschannel.thy \
mueller@3081
    60
  IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.ML \
mueller@3081
    61
  IOA/ABP/Action.thy IOA/ABP/Check.ML \
mueller@3081
    62
  IOA/ABP/Correctness.ML IOA/ABP/Correctness.thy \
mueller@3081
    63
  IOA/ABP/Env.thy IOA/ABP/Impl.thy \
mueller@3081
    64
  IOA/ABP/Impl_finite.thy IOA/ABP/Lemmas.ML \
mueller@3081
    65
  IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \
mueller@3081
    66
  IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy \
mueller@3081
    67
  IOA/ABP/Sender.thy IOA/ABP/Spec.thy 
mueller@3081
    68
mueller@3081
    69
mueller@3081
    70
IOA_NTP_FILES = IOA/NTP/Abschannel.ML \
mueller@3081
    71
  IOA/NTP/Abschannel.thy IOA/NTP/Action.ML  \
mueller@3081
    72
  IOA/NTP/Action.thy IOA/NTP/Correctness.ML \
mueller@3081
    73
  IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \
mueller@3081
    74
  IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML \
mueller@3081
    75
  IOA/NTP/Lemmas.thy IOA/NTP/Multiset.ML \
mueller@3081
    76
  IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \
mueller@3081
    77
  IOA/NTP/Packet.thy IOA/NTP/ROOT.ML \
mueller@3081
    78
  IOA/NTP/Receiver.ML IOA/NTP/Receiver.thy \
mueller@3081
    79
  IOA/NTP/Sender.ML IOA/NTP/Sender.thy \
mueller@3081
    80
  IOA/NTP/Spec.thy 
mueller@3081
    81
mueller@3081
    82
 
wenzelm@4447
    83
$(OUT)/IOA: $(OUT)/HOLCF $(IOA_FILES)
mueller@3081
    84
	@cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA
mueller@3081
    85
wenzelm@4447
    86
$(LOG)/IOA-ABP.gz: $(OUT)/IOA $(IOA_ABP_FILES)
mueller@3081
    87
	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP
mueller@3081
    88
wenzelm@4447
    89
$(LOG)/IOA-NTP.gz: $(OUT)/IOA $(IOA_NTP_FILES)
mueller@3081
    90
	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP
mueller@3081
    91
wenzelm@3951
    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
wenzelm@4447
    98
$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF $(IMP_FILES)
wenzelm@2828
    99
	@$(ISATOOL) usedir $(OUT)/HOLCF IMP
nipkow@2797
   100
wenzelm@3951
   101
wenzelm@2494
   102
## Miscellaneous examples
wenzelm@2494
   103
wenzelm@3951
   104
EX_THYS = ex/Dnat.thy ex/Stream.thy \
wenzelm@3921
   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
wenzelm@4447
   110
$(LOG)/HOLCF-ex.gz: ex/ROOT.ML $(EX_FILES)
wenzelm@2828
   111
	@$(ISATOOL) usedir $(OUT)/HOLCF ex
wenzelm@2494
   112
wenzelm@3951
   113
nipkow@2797
   114
## Full test
nipkow@2797
   115
wenzelm@4447
   116
ALL_TARGETS = $(OUT)/HOLCF $(OUT)/IOA $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \
wenzelm@4447
   117
  $(LOG)/HOLCF-IMP.gz $(LOG)/HOLCF-ex.gz
wenzelm@4447
   118
wenzelm@4447
   119
test: $(ALL_TARGETS)
wenzelm@4447
   120
wenzelm@4447
   121
clean:
wenzelm@4447
   122
	@rm -f $(ALL_TARGETS)
nipkow@2797
   123
wenzelm@3951
   124
wenzelm@2494
   125
.PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF