src/HOLCF/IsaMakefile
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 6011 c48050d6928d
child 6213 f5bdd6497e08
permissions -rw-r--r--
tidying
     1 #
     2 # $Id$
     3 #
     4 # IsaMakefile for HOLCF
     5 #
     6 
     7 ## targets
     8 
     9 default: HOLCF
    10 images: HOLCF IOA
    11 test: HOLCF-IMP HOLCF-ex IOA-ABP IOA-NTP IOA-Storage
    12 all: images test
    13 
    14 
    15 ## global settings
    16 
    17 SRC = $(ISABELLE_HOME)/src
    18 OUT = $(ISABELLE_OUTPUT)
    19 LOG = $(OUT)/log
    20 
    21 
    22 ## HOLCF
    23 
    24 HOLCF: HOL $(OUT)/HOLCF
    25 
    26 HOL:
    27 	@cd $(SRC)/HOL; $(ISATOOL) make HOL
    28 
    29 $(OUT)/HOLCF: $(OUT)/HOL Cfun1.ML Cfun1.thy Cfun2.ML Cfun2.thy \
    30   Cfun3.ML Cfun3.thy Cont.ML Cont.thy Cprod1.ML Cprod1.thy Cprod2.ML \
    31   Cprod2.thy Cprod3.ML Cprod3.thy Discrete.ML Discrete.thy Discrete0.ML \
    32   Discrete0.thy Discrete1.ML Discrete1.thy Fix.ML Fix.thy Fun1.ML \
    33   Fun1.thy Fun2.ML Fun2.thy Fun3.ML Fun3.thy HOLCF.ML HOLCF.thy Lift.ML \
    34   Lift.thy Lift1.ML Lift1.thy Lift2.ML Lift2.thy Lift3.ML Lift3.thy \
    35   One.ML One.thy Pcpo.ML Pcpo.thy Porder.ML Porder.thy Porder0.ML \
    36   Porder0.thy ROOT.ML Sprod0.ML Sprod0.thy Sprod1.ML Sprod1.thy \
    37   Sprod2.ML Sprod2.thy Sprod3.ML Sprod3.thy Ssum0.ML Ssum0.thy Ssum1.ML \
    38   Ssum1.thy Ssum2.ML Ssum2.thy Ssum3.ML Ssum3.thy Tr.ML Tr.thy Up1.ML \
    39   Up1.thy Up2.ML Up2.thy Up3.ML Up3.thy adm.ML cont_consts.ML \
    40   domain/axioms.ML domain/extender.ML domain/interface.ML \
    41   domain/library.ML domain/syntax.ML domain/theorems.ML holcf_logic.ML
    42 	@$(ISATOOL) usedir -b $(OUT)/HOL HOLCF
    43 
    44 
    45 ## HOLCF-IMP
    46 
    47 HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz
    48 
    49 $(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/Denotational.ML \
    50   IMP/Denotational.thy IMP/ROOT.ML
    51 	@$(ISATOOL) usedir $(OUT)/HOLCF IMP
    52 
    53 
    54 ## HOLCF-ex
    55 
    56 HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
    57 
    58 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Dagstuhl.ML ex/Dagstuhl.thy \
    59   ex/Dnat.ML ex/Dnat.thy ex/Fix2.ML ex/Fix2.thy ex/Focus_ex.ML \
    60   ex/Focus_ex.thy ex/Hoare.ML ex/Hoare.thy ex/Loop.ML ex/Loop.thy \
    61   ex/ROOT.ML ex/Stream.ML ex/Stream.thy ex/loeckx.ML
    62 	@$(ISATOOL) usedir $(OUT)/HOLCF ex
    63 
    64 
    65 ## IOA
    66 
    67 IOA: HOLCF $(OUT)/IOA
    68 
    69 $(OUT)/IOA: $(OUT)/HOLCF IOA/ROOT.ML IOA/meta_theory/Traces.thy \
    70   IOA/meta_theory/Asig.ML IOA/meta_theory/Asig.thy \
    71   IOA/meta_theory/CompoScheds.thy IOA/meta_theory/CompoExecs.ML \
    72   IOA/meta_theory/CompoTraces.thy IOA/meta_theory/CompoScheds.ML \
    73   IOA/meta_theory/CompoTraces.ML IOA/meta_theory/Sequence.ML \
    74   IOA/meta_theory/Seq.thy IOA/meta_theory/RefCorrectness.thy \
    75   IOA/meta_theory/Automata.thy IOA/meta_theory/Traces.ML \
    76   IOA/meta_theory/Seq.ML IOA/meta_theory/RefMappings.ML \
    77   IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/ShortExecutions.ML \
    78   IOA/meta_theory/IOA.thy IOA/meta_theory/IOA.ML \
    79   IOA/meta_theory/Sequence.thy IOA/meta_theory/Automata.ML \
    80   IOA/meta_theory/CompoExecs.thy IOA/meta_theory/RefMappings.thy \
    81   IOA/meta_theory/RefCorrectness.ML IOA/meta_theory/Compositionality.ML \
    82   IOA/meta_theory/Compositionality.thy \
    83   IOA/meta_theory/TL.thy IOA/meta_theory/TL.ML IOA/meta_theory/TLS.thy \
    84   IOA/meta_theory/TLS.ML IOA/meta_theory/LiveIOA.thy IOA/meta_theory/LiveIOA.ML \
    85   IOA/meta_theory/Pred.thy IOA/meta_theory/Abstraction.thy \
    86   IOA/meta_theory/Abstraction.ML IOA/meta_theory/TrivEx.thy IOA/meta_theory/TrivEx.ML \
    87   IOA/meta_theory/TrivEx2.thy IOA/meta_theory/TrivEx2.ML \
    88   IOA/meta_theory/Simulations.thy IOA/meta_theory/Simulations.ML \
    89   IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/SimCorrectness.ML 
    90 	@cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA
    91 
    92 
    93 ## IOA-ABP
    94 
    95 IOA-ABP: IOA $(LOG)/IOA-ABP.gz
    96 
    97 $(LOG)/IOA-ABP.gz: $(OUT)/IOA IOA/ABP/Abschannel.thy \
    98   IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.ML IOA/ABP/Action.thy \
    99   IOA/ABP/Check.ML IOA/ABP/Correctness.ML IOA/ABP/Correctness.thy \
   100   IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \
   101   IOA/ABP/Lemmas.ML IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \
   102   IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \
   103   IOA/ABP/Spec.thy
   104 	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP
   105 
   106 
   107 ## IOA-NTP
   108 
   109 IOA-NTP: IOA $(LOG)/IOA-NTP.gz
   110 
   111 $(LOG)/IOA-NTP.gz: $(OUT)/IOA IOA/NTP/Abschannel.ML \
   112   IOA/NTP/Abschannel.thy IOA/NTP/Action.ML IOA/NTP/Action.thy \
   113   IOA/NTP/Correctness.ML IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \
   114   IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML IOA/NTP/Lemmas.thy \
   115   IOA/NTP/Multiset.ML IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \
   116   IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.ML \
   117   IOA/NTP/Receiver.thy IOA/NTP/Sender.ML IOA/NTP/Sender.thy \
   118   IOA/NTP/Spec.thy
   119 	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP
   120 
   121 
   122 ## IOA-Storage
   123 
   124 IOA-Storage: IOA $(LOG)/IOA-Storage.gz
   125 
   126 $(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.ML \
   127   IOA/Storage/Action.thy IOA/Storage/Correctness.ML \
   128   IOA/Storage/Correctness.thy IOA/Storage/Impl.ML IOA/Storage/Impl.thy \
   129   IOA/Storage/ROOT.ML IOA/Storage/Spec.thy
   130 	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA Storage
   131 
   132 
   133 ## clean
   134 
   135 clean:
   136 	@rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \
   137 	  $(LOG)/HOLCF-ex.gz $(OUT)/IOA $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz \
   138 	  $(LOG)/IOA-NTP.gz $(LOG)/IOA-Storage.gz