Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOLCF/IsaMakefile
author huffman
Wed, 19 May 2010 17:01:07 -0700
changeset 36991 41a22e7c1145
parent 35930 86559356502d
child 37093 e67760c1b851
permissions -rw-r--r--
move some example files into new HOLCF/Tutorial directory 
     1 #

     2 # IsaMakefile for HOLCF

     3 #

     4 

     5 ## targets

     6 

     7 default: HOLCF

     8 images: HOLCF IOA

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

    10   HOLCF-Tutorial \

    11       IOA-ABP IOA-NTP IOA-Modelcheck IOA-Storage IOA-ex

    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; $(ISABELLE_TOOL) make HOL

    28 

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

    30   ROOT.ML \

    31   Adm.thy \

    32   Algebraic.thy \

    33   Bifinite.thy \

    34   Cfun.thy \

    35   CompactBasis.thy \

    36   Completion.thy \

    37   Cont.thy \

    38   ConvexPD.thy \

    39   Cprod.thy \

    40   Discrete.thy \

    41   Deflation.thy \

    42   Domain.thy \

    43   Domain_Aux.thy \

    44   Eventual.thy \

    45   Ffun.thy \

    46   Fixrec.thy \

    47   Fix.thy \

    48   HOLCF.thy \

    49   Lift.thy \

    50   LowerPD.thy \

    51   One.thy \

    52   Pcpodef.thy \

    53   Pcpo.thy \

    54   Porder.thy \

    55   Powerdomains.thy \

    56   Product_Cpo.thy \

    57   Representable.thy \

    58   Sprod.thy \

    59   Ssum.thy \

    60   Sum_Cpo.thy \

    61   Tr.thy \

    62   Universal.thy \

    63   UpperPD.thy \

    64   Up.thy \

    65   Tools/cont_consts.ML \

    66   Tools/cont_proc.ML \

    67   Tools/holcf_library.ML \

    68   Tools/Domain/domain_extender.ML \

    69   Tools/Domain/domain_axioms.ML \

    70   Tools/Domain/domain_constructors.ML \

    71   Tools/Domain/domain_isomorphism.ML \

    72   Tools/Domain/domain_library.ML \

    73   Tools/Domain/domain_take_proofs.ML \

    74   Tools/Domain/domain_theorems.ML \

    75   Tools/fixrec.ML \

    76   Tools/pcpodef.ML \

    77   Tools/repdef.ML \

    78   document/root.tex

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

    80 

    81 

    82 ## HOLCF-Tutorial

    83 

    84 HOLCF-Tutorial: HOLCF $(LOG)/HOLCF-Tutorial.gz

    85 

    86 $(LOG)/HOLCF-Tutorial.gz: $(OUT)/HOLCF \

    87   Tutorial/Domain_ex.thy \

    88   Tutorial/Fixrec_ex.thy \

    89   Tutorial/New_Domain.thy \

    90   Tutorial/document/root.tex \

    91   Tutorial/ROOT.ML

    92 	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial

    93 

    94 

    95 ## HOLCF-IMP

    96 

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

    98 

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

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

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

   102 

   103 

   104 ## HOLCF-ex

   105 

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

   107 

   108 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \

   109   ../HOL/Library/Nat_Infinity.thy \

   110   ex/Dagstuhl.thy \

   111   ex/Dnat.thy \

   112   ex/Domain_Proofs.thy \

   113   ex/Fix2.thy \

   114   ex/Focus_ex.thy \

   115   ex/Hoare.thy \

   116   ex/Letrec.thy \

   117   ex/Loop.thy \

   118   ex/Powerdomain_ex.thy \

   119   ex/Stream.thy \

   120   ex/Strict_Fun.thy \

   121   ex/ROOT.ML

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

   123 

   124 

   125 ## HOLCF-FOCUS

   126 

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

   128 

   129 $(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF \

   130   ex/Stream.thy \

   131   FOCUS/Fstreams.thy \

   132   FOCUS/Fstream.thy FOCUS/FOCUS.thy \

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

   134   FOCUS/Buffer.thy FOCUS/Buffer_adm.thy

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

   136 

   137 ## IOA

   138 

   139 IOA: HOLCF $(OUT)/IOA

   140 

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

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

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

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

   145   IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/IOA.thy	       \

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

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

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

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

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

   151   IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/automaton.ML

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

   153 

   154 

   155 ## IOA-ABP

   156 

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

   158 

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

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

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

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

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

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

   165   IOA/ABP/Spec.thy

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

   167 

   168 ## IOA-NTP

   169 

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

   171 

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

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

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

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

   176   IOA/NTP/Spec.thy

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

   178 

   179 

   180 ## IOA-Modelcheck

   181 

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

   183 

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

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

   186   IOA/Modelcheck/MuIOAOracle.thy IOA/Modelcheck/Ring3.thy

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

   188 

   189 

   190 ## IOA-Storage

   191 

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

   193 

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

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

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

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

   198 

   199 

   200 ## IOA-ex

   201 

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

   203 

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

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

   206 

   207 

   208 ## clean

   209 

   210 clean:

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

   212 	  $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA	\

   213 	  $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz	\

   214 	  $(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz	\

   215 	  $(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz
wneuper/isa