src/HOL/HOLCF/IsaMakefile
changeset 40774 0437dbc127b3
parent 40772 c8b52f9e1680
child 41112 866148b76247
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/IsaMakefile	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,224 @@
     1.4 +#
     1.5 +# IsaMakefile for HOLCF
     1.6 +#
     1.7 +
     1.8 +## targets
     1.9 +
    1.10 +default: HOLCF
    1.11 +images: HOLCF IOA
    1.12 +test: \
    1.13 +  HOLCF-FOCUS \
    1.14 +  HOLCF-IMP \
    1.15 +  HOLCF-Library \
    1.16 +  HOLCF-Tutorial \
    1.17 +  HOLCF-ex \
    1.18 +  IOA-ABP \
    1.19 +  IOA-NTP \
    1.20 +  IOA-Storage \
    1.21 +  IOA-ex
    1.22 +all: images test
    1.23 +
    1.24 +
    1.25 +## global settings
    1.26 +
    1.27 +SRC = $(ISABELLE_HOME)/src
    1.28 +OUT = $(ISABELLE_OUTPUT)
    1.29 +LOG = $(OUT)/log
    1.30 +
    1.31 +
    1.32 +## HOLCF
    1.33 +
    1.34 +HOLCF: HOL $(OUT)/HOLCF
    1.35 +
    1.36 +HOL:
    1.37 +	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
    1.38 +
    1.39 +$(OUT)/HOLCF: $(OUT)/HOL \
    1.40 +  ROOT.ML \
    1.41 +  Adm.thy \
    1.42 +  Algebraic.thy \
    1.43 +  Bifinite.thy \
    1.44 +  Cfun.thy \
    1.45 +  CompactBasis.thy \
    1.46 +  Completion.thy \
    1.47 +  Cont.thy \
    1.48 +  ConvexPD.thy \
    1.49 +  Cpodef.thy \
    1.50 +  Cprod.thy \
    1.51 +  Discrete.thy \
    1.52 +  Deflation.thy \
    1.53 +  Domain.thy \
    1.54 +  Domain_Aux.thy \
    1.55 +  Fixrec.thy \
    1.56 +  Fix.thy \
    1.57 +  Fun_Cpo.thy \
    1.58 +  HOLCF.thy \
    1.59 +  Lift.thy \
    1.60 +  LowerPD.thy \
    1.61 +  Map_Functions.thy \
    1.62 +  One.thy \
    1.63 +  Pcpo.thy \
    1.64 +  Plain_HOLCF.thy \
    1.65 +  Porder.thy \
    1.66 +  Powerdomains.thy \
    1.67 +  Product_Cpo.thy \
    1.68 +  Sfun.thy \
    1.69 +  Sprod.thy \
    1.70 +  Ssum.thy \
    1.71 +  Tr.thy \
    1.72 +  Universal.thy \
    1.73 +  UpperPD.thy \
    1.74 +  Up.thy \
    1.75 +  Tools/cont_consts.ML \
    1.76 +  Tools/cont_proc.ML \
    1.77 +  Tools/holcf_library.ML \
    1.78 +  Tools/Domain/domain.ML \
    1.79 +  Tools/Domain/domain_axioms.ML \
    1.80 +  Tools/Domain/domain_constructors.ML \
    1.81 +  Tools/Domain/domain_induction.ML \
    1.82 +  Tools/Domain/domain_isomorphism.ML \
    1.83 +  Tools/Domain/domain_take_proofs.ML \
    1.84 +  Tools/cpodef.ML \
    1.85 +  Tools/domaindef.ML \
    1.86 +  Tools/fixrec.ML \
    1.87 +  document/root.tex
    1.88 +	@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOLCF
    1.89 +
    1.90 +
    1.91 +## HOLCF-Tutorial
    1.92 +
    1.93 +HOLCF-Tutorial: HOLCF $(LOG)/HOLCF-Tutorial.gz
    1.94 +
    1.95 +$(LOG)/HOLCF-Tutorial.gz: $(OUT)/HOLCF \
    1.96 +  Tutorial/Domain_ex.thy \
    1.97 +  Tutorial/Fixrec_ex.thy \
    1.98 +  Tutorial/New_Domain.thy \
    1.99 +  Tutorial/document/root.tex \
   1.100 +  Tutorial/ROOT.ML
   1.101 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial
   1.102 +
   1.103 +
   1.104 +## HOLCF-Library
   1.105 +
   1.106 +HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz
   1.107 +
   1.108 +$(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
   1.109 +  Library/Defl_Bifinite.thy \
   1.110 +  Library/List_Cpo.thy \
   1.111 +  Library/Stream.thy \
   1.112 +  Library/Sum_Cpo.thy \
   1.113 +  Library/HOLCF_Library.thy \
   1.114 +  Library/ROOT.ML
   1.115 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library
   1.116 +
   1.117 +
   1.118 +## HOLCF-IMP
   1.119 +
   1.120 +HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz
   1.121 +
   1.122 +$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \
   1.123 +  IMP/Denotational.thy IMP/ROOT.ML IMP/document/root.tex
   1.124 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP
   1.125 +
   1.126 +
   1.127 +## HOLCF-ex
   1.128 +
   1.129 +HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
   1.130 +
   1.131 +$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \
   1.132 +  ../Library/Nat_Infinity.thy \
   1.133 +  ex/Dagstuhl.thy \
   1.134 +  ex/Dnat.thy \
   1.135 +  ex/Domain_Proofs.thy \
   1.136 +  ex/Fix2.thy \
   1.137 +  ex/Focus_ex.thy \
   1.138 +  ex/Hoare.thy \
   1.139 +  ex/Letrec.thy \
   1.140 +  ex/Loop.thy \
   1.141 +  ex/Pattern_Match.thy \
   1.142 +  ex/Powerdomain_ex.thy \
   1.143 +  ex/ROOT.ML
   1.144 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex
   1.145 +
   1.146 +
   1.147 +## HOLCF-FOCUS
   1.148 +
   1.149 +HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
   1.150 +
   1.151 +$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF \
   1.152 +  Library/Stream.thy \
   1.153 +  FOCUS/Fstreams.thy \
   1.154 +  FOCUS/Fstream.thy FOCUS/FOCUS.thy \
   1.155 +  FOCUS/Stream_adm.thy ../Library/Continuity.thy \
   1.156 +  FOCUS/Buffer.thy FOCUS/Buffer_adm.thy
   1.157 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS
   1.158 +
   1.159 +## IOA
   1.160 +
   1.161 +IOA: HOLCF $(OUT)/IOA
   1.162 +
   1.163 +$(OUT)/IOA: $(OUT)/HOLCF IOA/ROOT.ML IOA/meta_theory/Traces.thy        \
   1.164 +  IOA/meta_theory/Asig.thy IOA/meta_theory/CompoScheds.thy	       \
   1.165 +  IOA/meta_theory/CompoTraces.thy IOA/meta_theory/Seq.thy	       \
   1.166 +  IOA/meta_theory/RefCorrectness.thy IOA/meta_theory/Automata.thy      \
   1.167 +  IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/IOA.thy	       \
   1.168 +  IOA/meta_theory/Sequence.thy IOA/meta_theory/CompoExecs.thy	       \
   1.169 +  IOA/meta_theory/RefMappings.thy IOA/meta_theory/Compositionality.thy \
   1.170 +  IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy		       \
   1.171 +  IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy		       \
   1.172 +  IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy      \
   1.173 +  IOA/meta_theory/SimCorrectness.thy
   1.174 +	@cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
   1.175 +
   1.176 +
   1.177 +## IOA-ABP
   1.178 +
   1.179 +IOA-ABP: IOA $(LOG)/IOA-ABP.gz
   1.180 +
   1.181 +$(LOG)/IOA-ABP.gz: $(OUT)/IOA IOA/ABP/Abschannel.thy \
   1.182 +  IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.thy \
   1.183 +  IOA/ABP/Check.ML IOA/ABP/Correctness.thy \
   1.184 +  IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \
   1.185 +  IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \
   1.186 +  IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \
   1.187 +  IOA/ABP/Spec.thy
   1.188 +	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP
   1.189 +
   1.190 +## IOA-NTP
   1.191 +
   1.192 +IOA-NTP: IOA $(LOG)/IOA-NTP.gz
   1.193 +
   1.194 +$(LOG)/IOA-NTP.gz: $(OUT)/IOA \
   1.195 +  IOA/NTP/Abschannel.thy IOA/NTP/Action.thy IOA/NTP/Correctness.thy \
   1.196 +  IOA/NTP/Impl.thy IOA/NTP/Lemmas.thy IOA/NTP/Multiset.thy \
   1.197 +  IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.thy IOA/NTP/Sender.thy \
   1.198 +  IOA/NTP/Spec.thy
   1.199 +	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP
   1.200 +
   1.201 +
   1.202 +## IOA-Storage
   1.203 +
   1.204 +IOA-Storage: IOA $(LOG)/IOA-Storage.gz
   1.205 +
   1.206 +$(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.thy \
   1.207 +  IOA/Storage/Correctness.thy IOA/Storage/Impl.thy \
   1.208 +  IOA/Storage/ROOT.ML IOA/Storage/Spec.thy
   1.209 +	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Storage
   1.210 +
   1.211 +
   1.212 +## IOA-ex
   1.213 +
   1.214 +IOA-ex: IOA $(LOG)/IOA-ex.gz
   1.215 +
   1.216 +$(LOG)/IOA-ex.gz: $(OUT)/IOA IOA/ex/ROOT.ML IOA/ex/TrivEx.thy IOA/ex/TrivEx2.thy
   1.217 +	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex
   1.218 +
   1.219 +
   1.220 +## clean
   1.221 +
   1.222 +clean:
   1.223 +	@rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz	\
   1.224 +	  $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA	\
   1.225 +	  $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz	\
   1.226 +	  $(LOG)/IOA-Storage.gz $(LOG)/HOLCF-Library.gz		\
   1.227 +	  $(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz