# HG changeset patch # User wenzelm # Date 882523138 -3600 # Node ID b7ee449eb3454876a70c3175b666cf59fb61b0e4 # Parent 097004a470fb5cde2a45cf6ee82ab8273252ce78 log files; 'clean' target; diff -r 097004a470fb -r b7ee449eb345 src/CCL/IsaMakefile --- a/src/CCL/IsaMakefile Fri Dec 19 10:18:03 1997 +0100 +++ b/src/CCL/IsaMakefile Fri Dec 19 10:18:58 1997 +0100 @@ -5,6 +5,7 @@ # OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log SET_FILES = ROOT.ML Set.thy Set.ML subset.ML equalities.ML mono.ML \ Gfp.thy Gfp.ML Lfp.thy Lfp.ML @@ -23,7 +24,13 @@ $(OUT)/FOL: @cd ../FOL; $(ISATOOL) make -test: ex/ROOT.ML $(OUT)/CCL $(EX_FILES) +$(LOG)/CCL-ex.gz: ex/ROOT.ML $(OUT)/CCL $(EX_FILES) @$(ISATOOL) usedir $(OUT)/CCL ex +test: $(OUT)/CCL $(LOG)/CCL-ex.gz + +clean: + @rm -f $(OUT)/CCL $(LOG)/CCL-ex.gz + + .PRECIOUS: $(OUT)/FOL $(OUT)/CCL diff -r 097004a470fb -r b7ee449eb345 src/CTT/IsaMakefile --- a/src/CTT/IsaMakefile Fri Dec 19 10:18:03 1997 +0100 +++ b/src/CTT/IsaMakefile Fri Dec 19 10:18:58 1997 +0100 @@ -5,6 +5,7 @@ # OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log FILES = ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \ Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML @@ -17,7 +18,13 @@ $(OUT)/Pure: @cd ../Pure; $(ISATOOL) make -test: ex/ROOT.ML $(OUT)/CTT $(EX_FILES) +$(LOG)/CTT-ex.gz: ex/ROOT.ML $(OUT)/CTT $(EX_FILES) @$(ISATOOL) usedir $(OUT)/CTT ex +test: $(OUT)/CTT $(LOG)/CTT-ex.gz + +clean: + @rm -f $(OUT)/CTT $(LOG)/CTT-ex.gz + + .PRECIOUS: $(OUT)/Pure $(OUT)/CTT diff -r 097004a470fb -r b7ee449eb345 src/Cube/IsaMakefile --- a/src/Cube/IsaMakefile Fri Dec 19 10:18:03 1997 +0100 +++ b/src/Cube/IsaMakefile Fri Dec 19 10:18:58 1997 +0100 @@ -5,6 +5,8 @@ # OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log + FILES = ROOT.ML Cube.thy Cube.ML $(OUT)/Cube: $(OUT)/Pure $(FILES) @@ -13,7 +15,13 @@ $(OUT)/Pure: @cd ../Pure; $(ISATOOL) make -test: ex/ROOT.ML ex/ex.ML $(OUT)/Cube +$(LOG)/Cube-ex.gz: ex/ROOT.ML ex/ex.ML $(OUT)/Cube @$(ISATOOL) usedir $(OUT)/Cube ex +test: $(OUT)/Cube $(LOG)/Cube-ex.gz + +clean: + @rm -f $(OUT)/Cube $(LOG)/Cube-ex.gz + + .PRECIOUS: $(OUT)/Pure $(OUT)/Cube diff -r 097004a470fb -r b7ee449eb345 src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Fri Dec 19 10:18:03 1997 +0100 +++ b/src/FOL/IsaMakefile Fri Dec 19 10:18:58 1997 +0100 @@ -5,12 +5,13 @@ # OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log PROVERS = hypsubst.ML classical.ML blast.ML \ simplifier.ML splitter.ML ind.ML FILES = ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \ - fologic.ML cladata.ML $(PROVERS:%=../Provers/%) + fologic.ML cladata.ML $(PROVERS:%=$(ISABELLE_HOME)/src/Provers/%) EX_NAMES = If List Nat Nat2 Prolog IffOracle EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/int.ML ex/intro.ML \ @@ -23,7 +24,13 @@ $(OUT)/Pure: @cd ../Pure; $(ISATOOL) make -test: ex/ROOT.ML $(OUT)/FOL $(EX_FILES) +$(LOG)/FOL-ex.gz: ex/ROOT.ML $(OUT)/FOL $(EX_FILES) @$(ISATOOL) usedir $(OUT)/FOL ex +test: $(OUT)/FOL $(LOG)/FOL-ex.gz + +clean: + @rm -f $(OUT)/FOL $(LOG)/FOL-ex.gz + + .PRECIOUS: $(OUT)/Pure $(OUT)/FOL diff -r 097004a470fb -r b7ee449eb345 src/FOLP/IsaMakefile --- a/src/FOLP/IsaMakefile Fri Dec 19 10:18:03 1997 +0100 +++ b/src/FOLP/IsaMakefile Fri Dec 19 10:18:58 1997 +0100 @@ -5,6 +5,7 @@ # OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log FILES = ROOT.ML IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML \ hypsubst.ML classical.ML simp.ML @@ -19,7 +20,13 @@ $(OUT)/Pure: @cd ../Pure; $(ISATOOL) make -test: ex/ROOT.ML $(OUT)/FOLP $(EX_FILES) +$(LOG)/FOLP-ex.gz: ex/ROOT.ML $(OUT)/FOLP $(EX_FILES) @$(ISATOOL) usedir $(OUT)/FOLP ex +test: $(OUT)/FOLP $(LOG)/FOLP-ex.gz + +clean: + @rm -f $(OUT)/FOLP $(LOG)/FOLP-ex.gz + + .PRECIOUS: $(OUT)/Pure $(OUT)/FOLP diff -r 097004a470fb -r b7ee449eb345 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Dec 19 10:18:03 1997 +0100 +++ b/src/HOL/IsaMakefile Fri Dec 19 10:18:58 1997 +0100 @@ -7,6 +7,7 @@ #### Base system OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \ mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \ @@ -41,7 +42,7 @@ INDUCT_FILES = Induct/ROOT.ML \ $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML) -Induct: $(OUT)/HOL $(INDUCT_FILES) +$(LOG)/HOL-Induct.gz: $(OUT)/HOL $(INDUCT_FILES) @$(ISATOOL) usedir $(OUT)/HOL Induct @@ -50,7 +51,7 @@ IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML) -IMP: $(OUT)/HOL $(IMP_FILES) +$(LOG)/HOL-IMP.gz: $(OUT)/HOL $(IMP_FILES) @$(ISATOOL) usedir $(OUT)/HOL IMP @@ -60,7 +61,7 @@ Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \ $(Hoare_NAMES:%=Hoare/%.ML) -Hoare: $(OUT)/HOL $(Hoare_FILES) +$(LOG)/HOL-Hoare.gz: $(OUT)/HOL $(Hoare_FILES) @$(ISATOOL) usedir $(OUT)/HOL Hoare @@ -71,7 +72,7 @@ INTEG_FILES = Integ/ROOT.ML \ $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML) -Integ: $(OUT)/HOL $(INTEG_FILES) +$(LOG)/HOL-Integ.gz: $(OUT)/HOL $(INTEG_FILES) @$(ISATOOL) usedir $(OUT)/HOL Integ @@ -97,16 +98,16 @@ TLA/Memory/RPCParameters.ML TLA/Memory/RPCParameters.thy -TLA: $(OUT)/HOL $(TLA_FILES) +$(OUT)/TLA: $(OUT)/HOL $(TLA_FILES) @cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA -TLA_Inc: $(OUT)/TLA $(TLA_INC_FILES) +$(LOG)/TLA-Inc.gz: $(OUT)/TLA $(TLA_INC_FILES) @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc -TLA_Buffer: $(OUT)/TLA $(TLA_BUFFER_FILES) +$(LOG)/TLA-Buffer.gz: $(OUT)/TLA $(TLA_BUFFER_FILES) @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer -TLA_Memory: $(OUT)/TLA $(TLA_MEMORY_FILES) +$(LOG)/TLA-Memory.gz: $(OUT)/TLA $(TLA_MEMORY_FILES) @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory @@ -115,7 +116,7 @@ IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \ IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML -IOA: $(OUT)/HOL $(IOA_FILES) +$(LOG)/HOL-IOA.gz: $(OUT)/HOL $(IOA_FILES) @$(ISATOOL) usedir $(OUT)/HOL IOA @@ -128,7 +129,7 @@ AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML) -Auth: $(OUT)/HOL $(AUTH_FILES) +$(LOG)/HOL-Auth.gz: $(OUT)/HOL $(AUTH_FILES) @$(ISATOOL) usedir $(OUT)/HOL Auth @@ -138,7 +139,7 @@ Modelcheck/Example.thy Modelcheck/MCSyn.ML Modelcheck/MCSyn.thy \ Modelcheck/MuCalculus.ML Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML -Modelcheck: $(OUT)/HOL $(MC_FILES) +$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL $(MC_FILES) @$(ISATOOL) usedir $(OUT)/HOL Modelcheck @@ -149,7 +150,7 @@ SUBST_FILES = Subst/ROOT.ML \ $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML) -Subst: $(OUT)/HOL $(SUBST_FILES) +$(LOG)/HOL-Subst.gz: $(OUT)/HOL $(SUBST_FILES) @$(ISATOOL) usedir $(OUT)/HOL Subst @@ -160,7 +161,7 @@ LAMBDA_FILES = Lambda/ROOT.ML \ $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML) -Lambda: $(OUT)/HOL $(LAMBDA_FILES) +$(LOG)/HOL-Lambda.gz: $(OUT)/HOL $(LAMBDA_FILES) @$(ISATOOL) usedir $(OUT)/HOL Lambda @@ -171,7 +172,7 @@ W0_FILES = W0/ROOT.ML \ $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML) -W0: $(OUT)/HOL $(W0_FILES) +$(LOG)/HOL-W0.gz: $(OUT)/HOL $(W0_FILES) @$(ISATOOL) usedir $(OUT)/HOL W0 @@ -182,7 +183,7 @@ MINIML_FILES = MiniML/ROOT.ML \ $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML) -MiniML: $(OUT)/HOL $(MINIML_FILES) +$(LOG)/HOL-MiniML.gz: $(OUT)/HOL $(MINIML_FILES) @$(ISATOOL) usedir $(OUT)/HOL MiniML @@ -193,7 +194,7 @@ LEX_FILES = Lex/ROOT.ML \ $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML) -Lex: $(OUT)/HOL $(LEX_FILES) +$(LOG)/HOL-Lex.gz: $(OUT)/HOL $(LEX_FILES) @$(ISATOOL) usedir $(OUT)/HOL Lex @@ -212,15 +213,19 @@ ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \ Xor.ML Xor.thy -AXCLASSES_FILES = AxClasses/ROOT.ML \ - $(AXC_GROUP_FILES:%=AxClasses/Group/%) \ - $(AXC_LATTICE_FILES:%=AxClasses/Lattice/%) \ - $(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%) +$(LOG)/HOL-AxClasses.gz: AxClasses/ROOT.ML $(OUT)/HOL + @$(ISATOOL) usedir $(OUT)/HOL AxClasses + +$(LOG)/HOL-AxClasses-Group.gz: $(LOG)/HOL-AxClasses.gz \ + $(AXC_GROUP_FILES:%=AxClasses/Group/%) + @$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group -AxClasses: $(OUT)/HOL $(AXCLASSES_FILES) - @$(ISATOOL) usedir $(OUT)/HOL AxClasses - @$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group +$(LOG)/HOL-AxClasses-Lattice.gz: $(LOG)/HOL-AxClasses.gz \ + $(AXC_LATTICE_FILES:%=AxClasses/Lattice/%) @$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice + +$(LOG)/HOL-AxClasses-Tutorial.gz: $(LOG)/HOL-AxClasses.gz \ + $(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%) @$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial @@ -229,7 +234,8 @@ QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \ Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \ Quot/FRACT.thy Quot/FRACT.ML -Quot: $(OUT)/HOL $(QUOT_FILES) + +$(LOG)/HOL-Quot.gz: $(OUT)/HOL $(QUOT_FILES) @$(ISATOOL) usedir $(OUT)/HOL Quot @@ -240,16 +246,25 @@ EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) -ex: $(OUT)/HOL $(EX_FILES) +$(LOG)/HOL-ex.gz: $(OUT)/HOL $(EX_FILES) @$(ISATOOL) usedir $(OUT)/HOL ex ## Full test -test: $(OUT)/HOL \ - Subst Induct IMP Hoare Lex Integ Auth Modelcheck Lambda \ - W0 MiniML TLA TLA_Inc TLA_Buffer TLA_Memory IOA AxClasses Quot ex - echo 'Test examples ran successfully' > test +ALL_TARGETS = $(OUT)/HOL $(LOG)/HOL-Subst.gz $(LOG)/HOL-Induct.gz \ + $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz $(LOG)/HOL-Lex.gz \ + $(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-Modelcheck.gz \ + $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \ + $(OUT)/TLA $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \ + $(LOG)/TLA-Memory.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \ + $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \ + $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz $(LOG)/HOL-ex.gz + +test: $(ALL_TARGETS) + +clean: + @rm -f $(ALL_TARGETS) .PRECIOUS: $(OUT)/Pure $(OUT)/HOL diff -r 097004a470fb -r b7ee449eb345 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Fri Dec 19 10:18:03 1997 +0100 +++ b/src/HOLCF/IsaMakefile Fri Dec 19 10:18:58 1997 +0100 @@ -7,6 +7,7 @@ #### Base system OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log THYS = Porder.thy Porder0.thy Pcpo.thy \ Fun1.thy Fun2.thy Fun3.thy \ @@ -79,13 +80,13 @@ IOA/NTP/Spec.thy -IOA: $(OUT)/HOLCF $(IOA_FILES) +$(OUT)/IOA: $(OUT)/HOLCF $(IOA_FILES) @cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA -IOA_ABP: $(OUT)/IOA $(IOA_ABP_FILES) +$(LOG)/IOA-ABP.gz: $(OUT)/IOA $(IOA_ABP_FILES) @cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP -IOA_NTP: $(OUT)/IOA $(IOA_NTP_FILES) +$(LOG)/IOA-NTP.gz: $(OUT)/IOA $(IOA_NTP_FILES) @cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP @@ -94,7 +95,7 @@ IMP_THYS = IMP/Denotational.thy IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML) -IMP: $(OUT)/HOLCF $(IMP_FILES) +$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF $(IMP_FILES) @$(ISATOOL) usedir $(OUT)/HOLCF IMP @@ -106,14 +107,19 @@ EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) -ex: ex/ROOT.ML $(EX_FILES) +$(LOG)/HOLCF-ex.gz: ex/ROOT.ML $(EX_FILES) @$(ISATOOL) usedir $(OUT)/HOLCF ex ## Full test -test: $(OUT)/HOLCF IOA IOA_ABP IOA_NTP IMP ex - echo 'Test examples ran successfully' > test +ALL_TARGETS = $(OUT)/HOLCF $(OUT)/IOA $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \ + $(LOG)/HOLCF-IMP.gz $(LOG)/HOLCF-ex.gz + +test: $(ALL_TARGETS) + +clean: + @rm -f $(ALL_TARGETS) .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF diff -r 097004a470fb -r b7ee449eb345 src/LCF/IsaMakefile --- a/src/LCF/IsaMakefile Fri Dec 19 10:18:03 1997 +0100 +++ b/src/LCF/IsaMakefile Fri Dec 19 10:18:58 1997 +0100 @@ -5,6 +5,8 @@ # OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log + FILES = ROOT.ML LCF.thy LCF.ML simpdata.ML pair.ML fix.ML $(OUT)/LCF: $(OUT)/FOL $(FILES) @@ -13,7 +15,13 @@ $(OUT)/FOL: @cd ../FOL; $(ISATOOL) make -test: ex/ROOT.ML ex/ex.ML $(OUT)/LCF +$(LOG)/LCF-ex.gz: ex/ROOT.ML ex/ex.ML $(OUT)/LCF @$(ISATOOL) usedir $(OUT)/LCF ex +test: $(OUT)/LCF $(LOG)/LCF-ex.gz + +clean: + @rm -f $(OUT)/LCF $(LOG)/LCF-ex.gz + + .PRECIOUS: $(OUT)/FOL $(OUT)/LCF diff -r 097004a470fb -r b7ee449eb345 src/Sequents/IsaMakefile --- a/src/Sequents/IsaMakefile Fri Dec 19 10:18:03 1997 +0100 +++ b/src/Sequents/IsaMakefile Fri Dec 19 10:18:58 1997 +0100 @@ -5,6 +5,7 @@ # OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log NAMES = ILL LK S4 S43 T FILES = ROOT.ML Sequents.thy prover.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML) @@ -22,7 +23,13 @@ $(OUT)/Pure: @cd ../Pure; $(ISATOOL) make -test: $(OUT)/Sequents $(EX_FILES) +$(LOG)/Sequents-ex.gz: $(OUT)/Sequents $(EX_FILES) @$(ISATOOL) usedir $(OUT)/Sequents ex +test: $(OUT)/Sequents $(LOG)/Sequents-ex.gz + +clean: + @rm -f $(OUT)/Sequents $(LOG)/Sequents-ex.gz + + .PRECIOUS: $(OUT)/Pure $(OUT)/Sequents diff -r 097004a470fb -r b7ee449eb345 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Fri Dec 19 10:18:03 1997 +0100 +++ b/src/ZF/IsaMakefile Fri Dec 19 10:18:58 1997 +0100 @@ -7,6 +7,7 @@ #### Base system OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log NAMES = ZF upair subset pair domrange \ func AC equalities Bool \ @@ -35,7 +36,7 @@ IMP_NAMES = Com Denotation Equiv IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML) -IMP: $(OUT)/ZF $(IMP_FILES) +$(LOG)/ZF-IMP.gz: $(OUT)/ZF $(IMP_FILES) @$(ISATOOL) usedir $(OUT)/ZF IMP @@ -46,7 +47,7 @@ COIND_FILES = Coind/ROOT.ML Coind/Language.thy Coind/BCR.thy Coind/Dynamic.thy \ $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML) -Coind: $(OUT)/ZF $(COIND_FILES) +$(LOG)/ZF-Coind.gz: $(OUT)/ZF $(COIND_FILES) @$(ISATOOL) usedir $(OUT)/ZF Coind @@ -62,7 +63,7 @@ AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML \ $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML) -AC: $(OUT)/ZF $(AC_FILES) +$(LOG)/ZF-AC.gz: $(OUT)/ZF $(AC_FILES) @$(ISATOOL) usedir $(OUT)/ZF AC @@ -73,7 +74,7 @@ RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) $(RESID_NAMES:%=Resid/%.ML) -Resid: $(OUT)/ZF $(RESID_FILES) +$(LOG)/ZF-Resid.gz: $(OUT)/ZF $(RESID_FILES) @$(ISATOOL) usedir $(OUT)/ZF Resid @@ -84,13 +85,19 @@ EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) -ex: $(OUT)/ZF $(EX_FILES) +$(LOG)/ZF-ex.gz: $(OUT)/ZF $(EX_FILES) @$(ISATOOL) usedir $(OUT)/ZF ex ## Full test -test: $(OUT)/ZF IMP Coind AC Resid ex - echo 'Test examples ran successfully' > test +ALL_TARGETS = $(OUT)/ZF $(LOG)/ZF-IMP.gz $(LOG)/ZF-Coind.gz \ + $(LOG)/ZF-AC.gz $(LOG)/ZF-Resid.gz $(LOG)/ZF-ex.gz + +test: $(ALL_TARGETS) + +clean: + @rm -f $(ALL_TARGETS) + .PRECIOUS: $(OUT)/FOL $(OUT)/ZF