src/HOLCF/IsaMakefile
author wenzelm
Mon Jul 07 09:09:21 1997 +0200 (1997-07-07)
changeset 3505 1cb4ea47d967
parent 3350 a3abf29660e6
child 3921 e88ea232977c
permissions -rw-r--r--
eliminated chmod -w;
     1 #
     2 # $Id$
     3 #
     4 # IsaMakefile for HOLCF
     5 #
     6 
     7 #### Base system
     8 
     9 OUT = $(ISABELLE_OUTPUT)
    10 
    11 THYS = Porder.thy Porder0.thy Pcpo.thy \
    12        Fun1.thy Fun2.thy Fun3.thy \
    13        Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
    14        Cprod1.thy Cprod2.thy Cprod3.thy \
    15        Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
    16        Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
    17        Up1.thy Up2.thy Up3.thy Fix.thy \
    18        One.thy Tr.thy\
    19        Discrete0.thy Discrete1.thy Discrete.thy\
    20        Lift1.thy Lift2.thy Lift3.thy Lift.thy HOLCF.thy
    21 
    22 ONLYTHYS = 
    23 
    24 FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) \
    25         ax_ops/holcflogic.ML ax_ops/thy_axioms.ML \
    26         ax_ops/thy_ops.ML    ax_ops/thy_syntax.ML \
    27         domain/library.ML  domain/syntax.ML   domain/axioms.ML \
    28         domain/theorems.ML domain/extender.ML domain/interface.ML
    29 
    30 $(OUT)/HOLCF: $(OUT)/HOL $(FILES)
    31 	@$(ISATOOL) usedir -b $(OUT)/HOL HOLCF
    32 
    33 $(OUT)/HOL:
    34 	@cd ../HOL; $(ISATOOL) make
    35 
    36 
    37 
    38 #### Tests and examples
    39 
    40 ## IOA meta theory and examples
    41 
    42 
    43 IOA_FILES = IOA/ROOT.ML IOA/meta_theory/Traces.thy \
    44   IOA/meta_theory/Asig.ML IOA/meta_theory/Asig.thy \
    45   IOA/meta_theory/CompoScheds.thy IOA/meta_theory/CompoExecs.ML \
    46   IOA/meta_theory/CompoTraces.thy IOA/meta_theory/CompoScheds.ML \
    47   IOA/meta_theory/CompoTraces.ML IOA/meta_theory/Sequence.ML \
    48   IOA/meta_theory/Seq.thy IOA/meta_theory/RefCorrectness.thy \
    49   IOA/meta_theory/Automata.thy IOA/meta_theory/Traces.ML \
    50   IOA/meta_theory/Seq.ML IOA/meta_theory/RefMappings.ML \
    51   IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/ShortExecutions.ML \
    52   IOA/meta_theory/IOA.thy IOA/meta_theory/IOA.ML \
    53   IOA/meta_theory/Sequence.thy IOA/meta_theory/Automata.ML \
    54   IOA/meta_theory/CompoExecs.thy IOA/meta_theory/RefMappings.thy \
    55   IOA/meta_theory/RefCorrectness.ML IOA/meta_theory/Compositionality.ML \
    56   IOA/meta_theory/Compositionality.thy
    57 
    58 
    59 IOA_ABP_FILES = IOA/ABP/Abschannel.thy \
    60   IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.ML \
    61   IOA/ABP/Action.thy IOA/ABP/Check.ML \
    62   IOA/ABP/Correctness.ML IOA/ABP/Correctness.thy \
    63   IOA/ABP/Env.thy IOA/ABP/Impl.thy \
    64   IOA/ABP/Impl_finite.thy IOA/ABP/Lemmas.ML \
    65   IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \
    66   IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy \
    67   IOA/ABP/Sender.thy IOA/ABP/Spec.thy 
    68 
    69 
    70 IOA_NTP_FILES = IOA/NTP/Abschannel.ML \
    71   IOA/NTP/Abschannel.thy IOA/NTP/Action.ML  \
    72   IOA/NTP/Action.thy IOA/NTP/Correctness.ML \
    73   IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \
    74   IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML \
    75   IOA/NTP/Lemmas.thy IOA/NTP/Multiset.ML \
    76   IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \
    77   IOA/NTP/Packet.thy IOA/NTP/ROOT.ML \
    78   IOA/NTP/Receiver.ML IOA/NTP/Receiver.thy \
    79   IOA/NTP/Sender.ML IOA/NTP/Sender.thy \
    80   IOA/NTP/Spec.thy 
    81 
    82  
    83 IOA: $(OUT)/HOLCF $(IOA_FILES)
    84 	@cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA
    85 
    86 IOA_ABP: $(OUT)/IOA $(IOA_ABP_FILES)
    87 	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP
    88 
    89 IOA_NTP: $(OUT)/IOA $(IOA_NTP_FILES)
    90 	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP
    91 
    92 ## IMP
    93 
    94 IMP_THYS = IMP/Denotational.thy
    95 IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
    96 
    97 IMP:	$(OUT)/HOLCF $(IMP_FILES)
    98 	@$(ISATOOL) usedir $(OUT)/HOLCF IMP
    99 
   100 ## Miscellaneous examples
   101 
   102 EX_THYS = ex/Classlib.thy\
   103 	  ex/Dnat.thy ex/Dlist.thy ex/Stream.thy\
   104 	  ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy\
   105 	  ex/Hoare.thy ex/Loop.thy
   106 
   107 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
   108 
   109 EX:	ex/ROOT.ML $(EX_FILES)
   110 	@$(ISATOOL) usedir $(OUT)/HOLCF ex
   111 
   112 ## Full test
   113 
   114 test:	$(OUT)/HOLCF IOA IOA_ABP IOA_NTP IMP EX
   115 	echo 'Test examples ran successfully' > test
   116 
   117 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF