Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
doc-src/TutorialI/IsaMakefile
author nipkow
Wed, 25 May 2005 09:04:24 +0200
changeset 16069 3f2a9f400168
parent 13977 eb5fe146a4e0
child 16543 4dd8b4d1cfc3
permissions -rw-r--r--
*** empty log message *** 
     1 #

     2 # IsaMakefile for Tutorial

     3 #

     4 

     5 ## targets

     6 

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

     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

    13 

    14 

    15 ## global settings

    16 

    17 SRC = $(ISABELLE_HOME)/src

    18 OUT = $(ISABELLE_OUTPUT)

    19 LOG = $(OUT)/log

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

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

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

    23 

    24 

    25 ## HOL

    26 

    27 HOL:

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

    29 

    30 HOL-Complex:

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

    32 

    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

    43 

    44 

    45 

    46 ## HOL-Ifexpr

    47 

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

    49 

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

    51 	$(USEDIR) Ifexpr

    52 	@rm -f tutorial.dvi

    53 

    54 ## HOL-ToyList

    55 

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

    57 

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

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

    60 

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

    62 	$(USEDIR) ToyList2

    63 	@rm -f tutorial.dvi

    64 

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

    66 	$(USEDIR) ToyList

    67 	@rm -f tutorial.dvi

    68 

    69 ## HOL-CodeGen

    70 

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

    72 

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

    74 	$(USEDIR) CodeGen

    75 	@rm -f tutorial.dvi

    76 

    77 

    78 ## HOL-Datatype

    79 

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

    81 

    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

    87 

    88 

    89 ## HOL-Trie

    90 

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

    92 

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

    94 	$(USEDIR) Trie

    95 	@rm -f tutorial.dvi

    96 

    97 

    98 ## HOL-Recdef

    99 

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

   101 

   102 $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \

   103   Recdef/simplification.thy Recdef/Induction.thy \

   104   Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy

   105 	$(USEDIR) Recdef

   106 	@rm -f tutorial.dvi

   107 

   108 

   109 ## HOL-Advanced

   110 

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

   112 

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

   114 	Advanced/Partial.thy

   115 	$(USEDIR) Advanced

   116 	@rm -f tutorial.dvi

   117 

   118 ## HOL-Rules

   119 

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

   121 

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

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

   124 	Rules/Tacticals.thy Rules/ROOT.ML 

   125 	@$(USEDIR) Rules

   126 	@rm -f tutorial.dvi

   127 

   128 ## HOL-Sets

   129 

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

   131 

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

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

   134 	@$(USEDIR) Sets

   135 	@rm -f tutorial.dvi

   136 

   137 ## HOL-CTL

   138 

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

   140 

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

   142 	$(USEDIR) CTL

   143 	@rm -f tutorial.dvi

   144 

   145 ## HOL-Inductive

   146 

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

   148 

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

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

   151   Inductive/Advanced.thy

   152 	$(USEDIR) Inductive

   153 	@rm -f tutorial.dvi

   154 

   155 ## HOL-Types

   156 

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

   158 

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

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

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

   162   Types/Overloading.thy Types/Axioms.thy

   163 	$(REALUSEDIR) Types

   164 	@rm -f tutorial.dvi

   165 

   166 ## HOL-Misc

   167 

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

   169 

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

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

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

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

   174 	$(USEDIR) Misc

   175 	@rm -f tutorial.dvi

   176 

   177 

   178 ## HOL-Protocol

   179 

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

   181 

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

   183   Protocol/Message.thy Protocol/Message_lemmas.ML  \

   184   Protocol/Event.thy Protocol/Event_lemmas.ML  \

   185   Protocol/Public.thy Protocol/Public_lemmas.ML \

   186   Protocol/NS_Public.thy    

   187 	$(USEDIR) Protocol

   188 	@rm -f tutorial.dvi

   189 

   190 ## HOL-Documents

   191 

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

   193 

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

   195 	$(USEDIR) Documents

   196 	@rm -f tutorial.dvi

   197 

   198 ## clean

   199 

   200 clean:

   201 	@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-Recdef.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
wneuper/isa