wneuper/isa: doc-src/TutorialI/IsaMakefile@8d309beb66d6

1 #

     2 # IsaMakefile for Tutorial

3 #

     5 ## targets

     7 default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Fun \

     8   HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Complex-Types HOL-Misc \

     9   HOL-Protocol HOL-Documents styles

    10 images:

    11 test:

    12 all: default

    15 ## global settings

    17 SRC = $(ISABELLE_HOME)/src

    18 OUT = $(ISABELLE_OUTPUT)

    19 LOG = $(OUT)/log

    20 OPTIONS = -m brackets -i true -d "" -D document

    21 USEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL

    22 REALUSEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL-Complex

    25 ## HOL

    27 HOL:

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

    30 HOL-Complex:

    31 	@cd $(SRC)/HOL; $(ISATOOL) make HOL-Complex

    33 styles:

    34 	@rm -f isabelle.sty

    35 	@rm -f isabellesym.sty

    36 	@rm -f pdfsetup.sty

    37 	@$(ISATOOL) latex -o sty >/dev/null

    38 	@rm -f pdfsetup.sty

    39 	@rm -f */document/isabelle.sty

    40 	@rm -f */document/isabellesym.sty

    41 	@rm -f */document/pdfsetup.sty

    42 	@rm -f */document/session.tex

    46 ## HOL-Ifexpr

    48 HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz

    50 $(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML

    51 	$(USEDIR) Ifexpr

    52 	@rm -f tutorial.dvi

    54 ## HOL-ToyList

    56 HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz

    58 ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2

    59 	cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy

    61 $(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML

    62 	$(USEDIR) ToyList2

    63 	@rm -f tutorial.dvi

    65 $(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML

    66 	$(USEDIR) ToyList

    67 	@rm -f tutorial.dvi

    69 ## HOL-CodeGen

    71 HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz

    73 $(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/ROOT.ML CodeGen/CodeGen.thy

    74 	$(USEDIR) CodeGen

    75 	@rm -f tutorial.dvi

    78 ## HOL-Datatype

    80 HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz

    82 $(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \

    83   Datatype/Nested.thy Datatype/unfoldnested.thy \

    84   Datatype/Fundata.thy

    85 	$(USEDIR) Datatype

    86 	@rm -f tutorial.dvi

    89 ## HOL-Trie

    91 HOL-Trie: HOL $(LOG)/HOL-Trie.gz

    93 $(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy

    94 	$(USEDIR) Trie

    95 	@rm -f tutorial.dvi

    98 ## HOL-Fun

   100 HOL-Fun: HOL $(LOG)/HOL-Fun.gz

   102 $(LOG)/HOL-Fun.gz: $(OUT)/HOL Fun/ROOT.ML Fun/fun0.thy

   103 	$(USEDIR) Fun

   104 	@rm -f tutorial.dvi

   107 ## HOL-Advanced

   109 HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz

   111 $(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML

   112 	$(USEDIR) Advanced

   113 	@rm -f tutorial.dvi

   115 ## HOL-Rules

   117 HOL-Rules: HOL $(LOG)/HOL-Rules.gz

   119 $(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \

   120 	Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \

   121 	Rules/Tacticals.thy Rules/find2.thy Rules/ROOT.ML

   122 	@$(USEDIR) Rules

   123 	@rm -f tutorial.dvi

   125 ## HOL-Sets

   127 HOL-Sets: HOL $(LOG)/HOL-Sets.gz

   129 $(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \

   130 	Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML

   131 	@$(USEDIR) Sets

   132 	@rm -f tutorial.dvi

   134 ## HOL-CTL

   136 HOL-CTL: HOL $(LOG)/HOL-CTL.gz

   138 $(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML

   139 	$(USEDIR) CTL

   140 	@rm -f tutorial.dvi

   142 ## HOL-Inductive

   144 HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz

   146 $(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \

   147   Inductive/Even.thy Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \

   148   Inductive/Advanced.thy

   149 	$(USEDIR) Inductive

   150 	@rm -f tutorial.dvi

   152 ## HOL-Types

   154 HOL-Complex-Types: HOL-Complex $(LOG)/HOL-Complex-Types.gz

   156 $(LOG)/HOL-Complex-Types.gz: $(OUT)/HOL-Complex Types/ROOT.ML \

   157   Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \

   158   Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \

   159   Types/Overloading.thy Types/Axioms.thy

   160 	$(REALUSEDIR) Types

   161 	@rm -f tutorial.dvi

   163 ## HOL-Misc

   165 HOL-Misc: HOL $(LOG)/HOL-Misc.gz

   167 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \

   168   Misc/Plus.thy Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy \

   169   Misc/Option2.thy Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \

   170   Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy

   171 	$(USEDIR) Misc

   172 	@rm -f tutorial.dvi

   175 ## HOL-Protocol

   177 HOL-Protocol: HOL $(LOG)/HOL-Protocol.gz

   179 $(LOG)/HOL-Protocol.gz: $(OUT)/HOL Protocol/ROOT.ML  \

   180   Protocol/Message.thy Protocol/Event.thy \

   181   Protocol/Public.thy Protocol/NS_Public.thy

   182 	$(USEDIR) Protocol

   183 	@rm -f tutorial.dvi

   185 ## HOL-Documents

   187 HOL-Documents: HOL $(LOG)/HOL-Documents.gz

   189 $(LOG)/HOL-Documents.gz: $(OUT)/HOL Documents/Documents.thy Documents/ROOT.ML

   190 	$(USEDIR) Documents

   191 	@rm -f tutorial.dvi

   193 ## clean

   195 clean:

   196 	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Fun.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz $(LOG)/HOL-Protocol.gz $(LOG)/HOL-Documents.gz Rules/document/*.tex Sets/document/*.tex

author	nipkow
	Mon, 05 Nov 2007 15:37:41 +0100
changeset 25281	8d309beb66d6
parent 25258	22d16596c306
child 27423	b8ff8497de6a
permissions	-rw-r--r--