wneuper/isa: src/HOLCF/IsaMakefile@4b79e5d3d0aa

1 #

     2 # $Id$

3 #

     4 # IsaMakefile for HOLCF

5 #

     7 ## targets

     9 default: HOLCF

    10 images: HOLCF IOA

    11 test: HOLCF-IMP HOLCF-ex HOLCF-FOCUS \

    12       IOA-ABP IOA-NTP IOA-Modelcheck IOA-Storage IOA-ex

    13 all: images test

    16 ## global settings

    18 SRC = $(ISABELLE_HOME)/src

    19 OUT = $(ISABELLE_OUTPUT)

    20 LOG = $(OUT)/log

    23 ## HOLCF

    25 HOLCF: HOL $(OUT)/HOLCF

    27 HOL:

    28 	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL

    30 $(OUT)/HOLCF: $(OUT)/HOL \

    31   ROOT.ML \

    32   Adm.thy \

    33   Algebraic.thy \

    34   Bifinite.thy \

    35   Cfun.thy \

    36   CompactBasis.thy \

    37   Completion.thy \

    38   Cont.thy \

    39   ConvexPD.thy \

    40   Cprod.thy \

    41   Discrete.thy \

    42   Deflation.thy \

    43   Domain.thy \

    44   Eventual.thy \

    45   Ffun.thy \

    46   Fixrec.thy \

    47   Fix.thy \

    48   HOLCF.thy \

    49   Lift.thy \

    50   LowerPD.thy \

    51   NatIso.thy \

    52   One.thy \

    53   Pcpodef.thy \

    54   Pcpo.thy \

    55   Porder.thy \

    56   Sprod.thy \

    57   Ssum.thy \

    58   Tr.thy \

    59   Universal.thy \

    60   UpperPD.thy \

    61   Up.thy \

    62   Tools/adm_tac.ML \

    63   Tools/cont_consts.ML \

    64   Tools/cont_proc.ML \

    65   Tools/domain/domain_extender.ML \

    66   Tools/domain/domain_axioms.ML \

    67   Tools/domain/domain_library.ML \

    68   Tools/domain/domain_syntax.ML \

    69   Tools/domain/domain_theorems.ML \

    70   Tools/fixrec_package.ML \

    71   Tools/pcpodef_package.ML \

    72   holcf_logic.ML \

    73   document/root.tex

    74 	@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF

    77 ## HOLCF-IMP

    79 HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz

    81 $(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \

    82   IMP/Denotational.thy IMP/ROOT.ML IMP/document/root.tex

    83 	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP

    86 ## HOLCF-ex

    88 HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz

    90 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Stream.thy ex/Dagstuhl.thy \

    91   ex/Dnat.thy ex/Fix2.thy ex/Focus_ex.thy ex/Hoare.thy ex/Loop.thy \

    92   ex/ROOT.ML ex/Fixrec_ex.thy ../HOL/Library/Nat_Infinity.thy

    93 	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex

    96 ## HOLCF-FOCUS

    98 HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz

   100 $(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF FOCUS/Fstreams.thy \

   101   FOCUS/Fstream.thy FOCUS/FOCUS.thy \

   102   FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \

   103   FOCUS/Buffer.thy FOCUS/Buffer_adm.thy

   104 	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS

   106 ## IOA

   108 IOA: HOLCF $(OUT)/IOA

   110 $(OUT)/IOA: $(OUT)/HOLCF IOA/ROOT.ML IOA/meta_theory/Traces.thy        \

   111   IOA/meta_theory/Asig.thy IOA/meta_theory/CompoScheds.thy	       \

   112   IOA/meta_theory/CompoTraces.thy IOA/meta_theory/Seq.thy	       \

   113   IOA/meta_theory/RefCorrectness.thy IOA/meta_theory/Automata.thy      \

   114   IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/IOA.thy	       \

   115   IOA/meta_theory/Sequence.thy IOA/meta_theory/CompoExecs.thy	       \

   116   IOA/meta_theory/RefMappings.thy IOA/meta_theory/Compositionality.thy \

   117   IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy		       \

   118   IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy		       \

   119   IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy      \

   120   IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa_package.ML

   121 	@cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA

   124 ## IOA-ABP

   126 IOA-ABP: IOA $(LOG)/IOA-ABP.gz

   128 $(LOG)/IOA-ABP.gz: $(OUT)/IOA IOA/ABP/Abschannel.thy \

   129   IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.thy \

   130   IOA/ABP/Check.ML IOA/ABP/Correctness.thy \

   131   IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \

   132   IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \

   133   IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \

   134   IOA/ABP/Spec.thy

   135 	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP

   137 ## IOA-NTP

   139 IOA-NTP: IOA $(LOG)/IOA-NTP.gz

   141 $(LOG)/IOA-NTP.gz: $(OUT)/IOA \

   142   IOA/NTP/Abschannel.thy IOA/NTP/Action.thy IOA/NTP/Correctness.thy \

   143   IOA/NTP/Impl.thy IOA/NTP/Lemmas.thy IOA/NTP/Multiset.thy \

   144   IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.thy IOA/NTP/Sender.thy \

   145   IOA/NTP/Spec.thy

   146 	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP

   149 ## IOA-Modelcheck

   151 IOA-Modelcheck: IOA $(LOG)/IOA-Modelcheck.gz

   153 $(LOG)/IOA-Modelcheck.gz: $(OUT)/IOA IOA/Modelcheck/ROOT.ML \

   154   IOA/Modelcheck/Cockpit.thy IOA/Modelcheck/MuIOA.thy \

   155   IOA/Modelcheck/MuIOAOracle.thy IOA/Modelcheck/Ring3.thy

   156 	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Modelcheck

   159 ## IOA-Storage

   161 IOA-Storage: IOA $(LOG)/IOA-Storage.gz

   163 $(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.thy \

   164   IOA/Storage/Correctness.thy IOA/Storage/Impl.thy \

   165   IOA/Storage/ROOT.ML IOA/Storage/Spec.thy

   166 	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Storage

   169 ## IOA-ex

   171 IOA-ex: IOA $(LOG)/IOA-ex.gz

   173 $(LOG)/IOA-ex.gz: $(OUT)/IOA IOA/ex/ROOT.ML IOA/ex/TrivEx.thy IOA/ex/TrivEx2.thy

   174 	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex

   177 ## clean

   179 clean:

   180 	@rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \

   181 	  $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz \

   182           $(OUT)/IOA $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz \

   183 	  $(LOG)/IOA-NTP.gz $(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz

author	wenzelm
	Sat, 04 Oct 2008 16:05:09 +0200
changeset 28500	4b79e5d3d0aa
parent 27420	aa335405f0c5
child 29130	685c9e05a6ab
permissions	-rw-r--r--