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 Walther Neuper <neuper@ist.tugraz.at>
Thu, 12 Aug 2010 15:03:34 +0200
branchisac-from-Isabelle2009-2
changeset 37913 20e3616b2d9c
parent 32835 00c14c4a6b4f
child 43383 f1ca2b0e0265
permissions -rw-r--r--
prepare reactivation of isac-update-Isa09-2 
     1 #

     2 # IsaMakefile for Tutorial

     3 #

     4 

     5 ## targets

     6 

     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-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 = -m brackets -i true -d "" -D document -M 1

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

    22 

    23 

    24 ## HOL

    25 

    26 HOL:

    27 	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL

    28 

    29 styles:

    30 	@rm -f isabelle.sty

    31 	@rm -f isabellesym.sty

    32 	@rm -f pdfsetup.sty

    33 	@$(ISABELLE_TOOL) latex -o sty >/dev/null

    34 	@rm -f pdfsetup.sty

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

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

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

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

    39 

    40 

    41 

    42 ## HOL-Ifexpr

    43 

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

    45 

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

    47 	$(USEDIR) Ifexpr

    48 	@rm -f tutorial.dvi

    49 

    50 ## HOL-ToyList

    51 

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

    53 

    54 ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2

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

    56 

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

    58 	$(USEDIR) ToyList2

    59 	@rm -f tutorial.dvi

    60 

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

    62 	$(USEDIR) ToyList

    63 	@rm -f tutorial.dvi

    64 

    65 ## HOL-CodeGen

    66 

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

    68 

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

    70 	$(USEDIR) CodeGen

    71 	@rm -f tutorial.dvi

    72 

    73 

    74 ## HOL-Datatype

    75 

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

    77 

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

    79   Datatype/Nested.thy Datatype/unfoldnested.thy \

    80   Datatype/Fundata.thy

    81 	$(USEDIR) Datatype

    82 	@rm -f tutorial.dvi

    83 

    84 

    85 ## HOL-Trie

    86 

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

    88 

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

    90 	$(USEDIR) Trie

    91 	@rm -f tutorial.dvi

    92 

    93 

    94 ## HOL-Fun

    95 

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

    97 

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

    99 	$(USEDIR) Fun

   100 	@rm -f tutorial.dvi

   101 

   102 

   103 ## HOL-Advanced

   104 

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

   106 

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

   108 	$(USEDIR) Advanced

   109 	@rm -f tutorial.dvi

   110 

   111 ## HOL-Rules

   112 

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

   114 

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

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

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

   118 	@$(USEDIR) Rules

   119 	@rm -f tutorial.dvi

   120 

   121 ## HOL-Sets

   122 

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

   124 

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

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

   127 	@$(USEDIR) Sets

   128 	@rm -f tutorial.dvi

   129 

   130 ## HOL-CTL

   131 

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

   133 

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

   135 	$(USEDIR) CTL

   136 	@rm -f tutorial.dvi

   137 

   138 ## HOL-Inductive

   139 

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

   141 

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

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

   144   Inductive/Advanced.thy

   145 	$(USEDIR) Inductive

   146 	@rm -f tutorial.dvi

   147 

   148 ## HOL-Types

   149 

   150 HOL-Types: HOL $(LOG)/HOL-Types.gz

   151 

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

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

   154   Types/Overloading.thy Types/Axioms.thy

   155 	$(USEDIR) Types

   156 	@rm -f tutorial.dvi

   157 

   158 ## HOL-Misc

   159 

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

   161 

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

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

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

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

   166 	$(USEDIR) Misc

   167 	@rm -f tutorial.dvi

   168 

   169 

   170 ## HOL-Protocol

   171 

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

   173 

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

   175   Protocol/Message.thy Protocol/Event.thy \

   176   Protocol/Public.thy Protocol/NS_Public.thy    

   177 	$(USEDIR) Protocol

   178 	@rm -f tutorial.dvi

   179 

   180 ## HOL-Documents

   181 

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

   183 

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

   185 	$(USEDIR) Documents

   186 	@rm -f tutorial.dvi

   187 

   188 ## clean

   189 

   190 clean:

   191 	@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
wneuper/isa