doc-src/TutorialI/IsaMakefile
author wenzelm
Wed Jul 25 12:38:54 2012 +0200 (2012-07-25)
changeset 48497 ba61aceaa18a
parent 42512 f1ca2b0e0265
child 48506 af1dabad14c0
permissions -rw-r--r--
some updates on "Building a repository version of Isabelle";
     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
    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 
    30 
    31 ## HOL-Ifexpr
    32 
    33 HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz
    34 
    35 $(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML
    36 	$(USEDIR) Ifexpr
    37 	@rm -f Ifexpr/document/isabelle.sty
    38 	@rm -f Ifexpr/document/isabellesym.sty
    39 	@rm -f Ifexpr/document/pdfsetup.sty
    40 	@rm -f Ifexpr/document/session.tex
    41 	@rm -f tutorial.dvi
    42 
    43 ## HOL-ToyList
    44 
    45 HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz
    46 
    47 ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2
    48 	cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy
    49 
    50 $(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML
    51 	$(USEDIR) ToyList2
    52 	@rm -f ToyList2/document/isabelle.sty
    53 	@rm -f ToyList2/document/isabellesym.sty
    54 	@rm -f ToyList2/document/pdfsetup.sty
    55 	@rm -f ToyList2/document/session.tex
    56 	@rm -f tutorial.dvi
    57 
    58 $(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML
    59 	$(USEDIR) ToyList
    60 	@rm -f ToyList/document/isabelle.sty
    61 	@rm -f ToyList/document/isabellesym.sty
    62 	@rm -f ToyList/document/pdfsetup.sty
    63 	@rm -f ToyList/document/session.tex
    64 	@rm -f tutorial.dvi
    65 
    66 ## HOL-CodeGen
    67 
    68 HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz
    69 
    70 $(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/ROOT.ML CodeGen/CodeGen.thy
    71 	$(USEDIR) CodeGen
    72 	@rm -f CodeGen/document/isabelle.sty
    73 	@rm -f CodeGen/document/isabellesym.sty
    74 	@rm -f CodeGen/document/pdfsetup.sty
    75 	@rm -f CodeGen/document/session.tex
    76 	@rm -f tutorial.dvi
    77 
    78 
    79 ## HOL-Datatype
    80 
    81 HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz
    82 
    83 $(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \
    84   Datatype/Nested.thy Datatype/unfoldnested.thy \
    85   Datatype/Fundata.thy
    86 	$(USEDIR) Datatype
    87 	@rm -f Datatype/document/isabelle.sty
    88 	@rm -f Datatype/document/isabellesym.sty
    89 	@rm -f Datatype/document/pdfsetup.sty
    90 	@rm -f Datatype/document/session.tex
    91 	@rm -f tutorial.dvi
    92 
    93 
    94 ## HOL-Trie
    95 
    96 HOL-Trie: HOL $(LOG)/HOL-Trie.gz
    97 
    98 $(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy
    99 	$(USEDIR) Trie
   100 	@rm -f Trie/document/isabelle.sty
   101 	@rm -f Trie/document/isabellesym.sty
   102 	@rm -f Trie/document/pdfsetup.sty
   103 	@rm -f Trie/document/session.tex
   104 	@rm -f tutorial.dvi
   105 
   106 
   107 ## HOL-Fun
   108 
   109 HOL-Fun: HOL $(LOG)/HOL-Fun.gz
   110 
   111 $(LOG)/HOL-Fun.gz: $(OUT)/HOL Fun/ROOT.ML Fun/fun0.thy
   112 	$(USEDIR) Fun
   113 	@rm -f Fun/document/isabelle.sty
   114 	@rm -f Fun/document/isabellesym.sty
   115 	@rm -f Fun/document/pdfsetup.sty
   116 	@rm -f Fun/document/session.tex
   117 	@rm -f tutorial.dvi
   118 
   119 
   120 ## HOL-Advanced
   121 
   122 HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz
   123 
   124 $(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML
   125 	$(USEDIR) Advanced
   126 	@rm -f Advanced/document/isabelle.sty
   127 	@rm -f Advanced/document/isabellesym.sty
   128 	@rm -f Advanced/document/pdfsetup.sty
   129 	@rm -f Advanced/document/session.tex
   130 	@rm -f tutorial.dvi
   131 
   132 ## HOL-Rules
   133 
   134 HOL-Rules: HOL $(LOG)/HOL-Rules.gz
   135 
   136 $(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \
   137 	Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \
   138 	Rules/Tacticals.thy Rules/find2.thy Rules/ROOT.ML 
   139 	@$(USEDIR) Rules
   140 	@rm -f Rules/document/isabelle.sty
   141 	@rm -f Rules/document/isabellesym.sty
   142 	@rm -f Rules/document/pdfsetup.sty
   143 	@rm -f Rules/document/session.tex
   144 	@rm -f tutorial.dvi
   145 
   146 ## HOL-Sets
   147 
   148 HOL-Sets: HOL $(LOG)/HOL-Sets.gz
   149 
   150 $(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \
   151 	Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML
   152 	@$(USEDIR) Sets
   153 	@rm -f Sets/document/isabelle.sty
   154 	@rm -f Sets/document/isabellesym.sty
   155 	@rm -f Sets/document/pdfsetup.sty
   156 	@rm -f Sets/document/session.tex
   157 	@rm -f tutorial.dvi
   158 
   159 ## HOL-CTL
   160 
   161 HOL-CTL: HOL $(LOG)/HOL-CTL.gz
   162 
   163 $(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML
   164 	$(USEDIR) CTL
   165 	@rm -f CTL/document/isabelle.sty
   166 	@rm -f CTL/document/isabellesym.sty
   167 	@rm -f CTL/document/pdfsetup.sty
   168 	@rm -f CTL/document/session.tex
   169 	@rm -f tutorial.dvi
   170 
   171 ## HOL-Inductive
   172 
   173 HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz
   174 
   175 $(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \
   176   Inductive/Even.thy Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \
   177   Inductive/Advanced.thy
   178 	$(USEDIR) Inductive
   179 	@rm -f Inductive/document/isabelle.sty
   180 	@rm -f Inductive/document/isabellesym.sty
   181 	@rm -f Inductive/document/pdfsetup.sty
   182 	@rm -f Inductive/document/session.tex
   183 	@rm -f tutorial.dvi
   184 
   185 ## HOL-Types
   186 
   187 HOL-Types: HOL $(LOG)/HOL-Types.gz
   188 
   189 $(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \
   190   Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \
   191   Types/Overloading.thy Types/Axioms.thy
   192 	$(USEDIR) Types
   193 	@rm -f Types/document/isabelle.sty
   194 	@rm -f Types/document/isabellesym.sty
   195 	@rm -f Types/document/pdfsetup.sty
   196 	@rm -f Types/document/session.tex
   197 	@rm -f tutorial.dvi
   198 
   199 ## HOL-Misc
   200 
   201 HOL-Misc: HOL $(LOG)/HOL-Misc.gz
   202 
   203 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
   204   Misc/Plus.thy Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy \
   205   Misc/Option2.thy Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
   206   Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy
   207 	$(USEDIR) Misc
   208 	@rm -f Misc/document/isabelle.sty
   209 	@rm -f Misc/document/isabellesym.sty
   210 	@rm -f Misc/document/pdfsetup.sty
   211 	@rm -f Misc/document/session.tex
   212 	@rm -f tutorial.dvi
   213 
   214 
   215 ## HOL-Protocol
   216 
   217 HOL-Protocol: HOL $(LOG)/HOL-Protocol.gz
   218 
   219 $(LOG)/HOL-Protocol.gz: $(OUT)/HOL Protocol/ROOT.ML  \
   220   Protocol/Message.thy Protocol/Event.thy \
   221   Protocol/Public.thy Protocol/NS_Public.thy    
   222 	$(USEDIR) Protocol
   223 	@rm -f Protocol/document/isabelle.sty
   224 	@rm -f Protocol/document/isabellesym.sty
   225 	@rm -f Protocol/document/pdfsetup.sty
   226 	@rm -f Protocol/document/session.tex
   227 	@rm -f tutorial.dvi
   228 
   229 ## HOL-Documents
   230 
   231 HOL-Documents: HOL $(LOG)/HOL-Documents.gz
   232 
   233 $(LOG)/HOL-Documents.gz: $(OUT)/HOL Documents/Documents.thy Documents/ROOT.ML
   234 	$(USEDIR) Documents
   235 	@rm -f Documents/document/isabelle.sty
   236 	@rm -f Documents/document/isabellesym.sty
   237 	@rm -f Documents/document/pdfsetup.sty
   238 	@rm -f Documents/document/session.tex
   239 	@rm -f tutorial.dvi
   240 
   241 ## clean
   242 
   243 clean:
   244 	@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