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";
nipkow@8743
     1
#
nipkow@8743
     2
# IsaMakefile for Tutorial
nipkow@8743
     3
#
nipkow@8743
     4
nipkow@8743
     5
## targets
nipkow@8743
     6
nipkow@25281
     7
default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Fun \
haftmann@27423
     8
  HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Types HOL-Misc \
wenzelm@42512
     9
  HOL-Protocol HOL-Documents
wenzelm@9520
    10
images:
wenzelm@9520
    11
test:
wenzelm@9520
    12
all: default
nipkow@8743
    13
nipkow@8743
    14
nipkow@8743
    15
## global settings
nipkow@8743
    16
nipkow@8743
    17
SRC = $(ISABELLE_HOME)/src
nipkow@8743
    18
OUT = $(ISABELLE_OUTPUT)
nipkow@8743
    19
LOG = $(OUT)/log
wenzelm@32835
    20
OPTIONS = -m brackets -i true -d "" -D document -M 1
wenzelm@28500
    21
USEDIR = @$(ISABELLE_TOOL) usedir $(OPTIONS) $(OUT)/HOL
wenzelm@11617
    22
nipkow@8743
    23
nipkow@8743
    24
## HOL
nipkow@8743
    25
nipkow@8743
    26
HOL:
wenzelm@28500
    27
	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
nipkow@8743
    28
nipkow@8743
    29
nipkow@8743
    30
nipkow@8743
    31
## HOL-Ifexpr
nipkow@8743
    32
nipkow@8743
    33
HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz
nipkow@8743
    34
nipkow@8743
    35
$(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML
nipkow@10676
    36
	$(USEDIR) Ifexpr
wenzelm@42512
    37
	@rm -f Ifexpr/document/isabelle.sty
wenzelm@42512
    38
	@rm -f Ifexpr/document/isabellesym.sty
wenzelm@42512
    39
	@rm -f Ifexpr/document/pdfsetup.sty
wenzelm@42512
    40
	@rm -f Ifexpr/document/session.tex
nipkow@8754
    41
	@rm -f tutorial.dvi
nipkow@8743
    42
nipkow@8743
    43
## HOL-ToyList
nipkow@8743
    44
nipkow@8743
    45
HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz
nipkow@8743
    46
nipkow@8743
    47
ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2
nipkow@8743
    48
	cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy
nipkow@8743
    49
nipkow@8743
    50
$(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML
nipkow@10676
    51
	$(USEDIR) ToyList2
wenzelm@42512
    52
	@rm -f ToyList2/document/isabelle.sty
wenzelm@42512
    53
	@rm -f ToyList2/document/isabellesym.sty
wenzelm@42512
    54
	@rm -f ToyList2/document/pdfsetup.sty
wenzelm@42512
    55
	@rm -f ToyList2/document/session.tex
nipkow@8754
    56
	@rm -f tutorial.dvi
nipkow@8743
    57
nipkow@8743
    58
$(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML
nipkow@10676
    59
	$(USEDIR) ToyList
wenzelm@42512
    60
	@rm -f ToyList/document/isabelle.sty
wenzelm@42512
    61
	@rm -f ToyList/document/isabellesym.sty
wenzelm@42512
    62
	@rm -f ToyList/document/pdfsetup.sty
wenzelm@42512
    63
	@rm -f ToyList/document/session.tex
nipkow@8754
    64
	@rm -f tutorial.dvi
nipkow@8743
    65
nipkow@8743
    66
## HOL-CodeGen
nipkow@8743
    67
nipkow@8743
    68
HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz
nipkow@8743
    69
nipkow@10676
    70
$(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/ROOT.ML CodeGen/CodeGen.thy
nipkow@10676
    71
	$(USEDIR) CodeGen
wenzelm@42512
    72
	@rm -f CodeGen/document/isabelle.sty
wenzelm@42512
    73
	@rm -f CodeGen/document/isabellesym.sty
wenzelm@42512
    74
	@rm -f CodeGen/document/pdfsetup.sty
wenzelm@42512
    75
	@rm -f CodeGen/document/session.tex
nipkow@8754
    76
	@rm -f tutorial.dvi
nipkow@8743
    77
nipkow@8743
    78
nipkow@8743
    79
## HOL-Datatype
nipkow@8743
    80
nipkow@8743
    81
HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz
nipkow@8743
    82
nipkow@8751
    83
$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \
nipkow@9666
    84
  Datatype/Nested.thy Datatype/unfoldnested.thy \
nipkow@9644
    85
  Datatype/Fundata.thy
nipkow@10676
    86
	$(USEDIR) Datatype
wenzelm@42512
    87
	@rm -f Datatype/document/isabelle.sty
wenzelm@42512
    88
	@rm -f Datatype/document/isabellesym.sty
wenzelm@42512
    89
	@rm -f Datatype/document/pdfsetup.sty
wenzelm@42512
    90
	@rm -f Datatype/document/session.tex
nipkow@8754
    91
	@rm -f tutorial.dvi
nipkow@8743
    92
nipkow@8743
    93
nipkow@8743
    94
## HOL-Trie
nipkow@8743
    95
nipkow@8743
    96
HOL-Trie: HOL $(LOG)/HOL-Trie.gz
nipkow@8743
    97
nipkow@10543
    98
$(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy
nipkow@10676
    99
	$(USEDIR) Trie
wenzelm@42512
   100
	@rm -f Trie/document/isabelle.sty
wenzelm@42512
   101
	@rm -f Trie/document/isabellesym.sty
wenzelm@42512
   102
	@rm -f Trie/document/pdfsetup.sty
wenzelm@42512
   103
	@rm -f Trie/document/session.tex
nipkow@8754
   104
	@rm -f tutorial.dvi
nipkow@8743
   105
nipkow@8743
   106
nipkow@25258
   107
## HOL-Fun
nipkow@25258
   108
nipkow@25258
   109
HOL-Fun: HOL $(LOG)/HOL-Fun.gz
nipkow@25258
   110
nipkow@25258
   111
$(LOG)/HOL-Fun.gz: $(OUT)/HOL Fun/ROOT.ML Fun/fun0.thy
nipkow@25258
   112
	$(USEDIR) Fun
wenzelm@42512
   113
	@rm -f Fun/document/isabelle.sty
wenzelm@42512
   114
	@rm -f Fun/document/isabellesym.sty
wenzelm@42512
   115
	@rm -f Fun/document/pdfsetup.sty
wenzelm@42512
   116
	@rm -f Fun/document/session.tex
nipkow@25258
   117
	@rm -f tutorial.dvi
nipkow@25258
   118
nipkow@25258
   119
nipkow@9933
   120
## HOL-Advanced
nipkow@9933
   121
nipkow@9933
   122
HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz
nipkow@9933
   123
nipkow@25281
   124
$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML
nipkow@10676
   125
	$(USEDIR) Advanced
wenzelm@42512
   126
	@rm -f Advanced/document/isabelle.sty
wenzelm@42512
   127
	@rm -f Advanced/document/isabellesym.sty
wenzelm@42512
   128
	@rm -f Advanced/document/pdfsetup.sty
wenzelm@42512
   129
	@rm -f Advanced/document/session.tex
nipkow@9933
   130
	@rm -f tutorial.dvi
nipkow@9933
   131
paulson@10296
   132
## HOL-Rules
paulson@10296
   133
paulson@10296
   134
HOL-Rules: HOL $(LOG)/HOL-Rules.gz
paulson@10296
   135
paulson@10296
   136
$(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \
paulson@10956
   137
	Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \
nipkow@16543
   138
	Rules/Tacticals.thy Rules/find2.thy Rules/ROOT.ML 
paulson@10840
   139
	@$(USEDIR) Rules
wenzelm@42512
   140
	@rm -f Rules/document/isabelle.sty
wenzelm@42512
   141
	@rm -f Rules/document/isabellesym.sty
wenzelm@42512
   142
	@rm -f Rules/document/pdfsetup.sty
wenzelm@42512
   143
	@rm -f Rules/document/session.tex
paulson@10296
   144
	@rm -f tutorial.dvi
paulson@10296
   145
paulson@10296
   146
## HOL-Sets
paulson@10296
   147
paulson@10296
   148
HOL-Sets: HOL $(LOG)/HOL-Sets.gz
paulson@10296
   149
paulson@10296
   150
$(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \
paulson@10296
   151
	Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML
paulson@10840
   152
	@$(USEDIR) Sets
wenzelm@42512
   153
	@rm -f Sets/document/isabelle.sty
wenzelm@42512
   154
	@rm -f Sets/document/isabellesym.sty
wenzelm@42512
   155
	@rm -f Sets/document/pdfsetup.sty
wenzelm@42512
   156
	@rm -f Sets/document/session.tex
paulson@10296
   157
	@rm -f tutorial.dvi
paulson@10296
   158
nipkow@9958
   159
## HOL-CTL
nipkow@9958
   160
nipkow@9958
   161
HOL-CTL: HOL $(LOG)/HOL-CTL.gz
nipkow@9958
   162
nipkow@10212
   163
$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML
nipkow@10676
   164
	$(USEDIR) CTL
wenzelm@42512
   165
	@rm -f CTL/document/isabelle.sty
wenzelm@42512
   166
	@rm -f CTL/document/isabellesym.sty
wenzelm@42512
   167
	@rm -f CTL/document/pdfsetup.sty
wenzelm@42512
   168
	@rm -f CTL/document/session.tex
nipkow@9958
   169
	@rm -f tutorial.dvi
nipkow@9958
   170
nipkow@10217
   171
## HOL-Inductive
nipkow@10217
   172
nipkow@10217
   173
HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz
nipkow@10217
   174
nipkow@10225
   175
$(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \
nipkow@10762
   176
  Inductive/Even.thy Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \
nipkow@10762
   177
  Inductive/Advanced.thy
nipkow@10676
   178
	$(USEDIR) Inductive
wenzelm@42512
   179
	@rm -f Inductive/document/isabelle.sty
wenzelm@42512
   180
	@rm -f Inductive/document/isabellesym.sty
wenzelm@42512
   181
	@rm -f Inductive/document/pdfsetup.sty
wenzelm@42512
   182
	@rm -f Inductive/document/session.tex
nipkow@10217
   183
	@rm -f tutorial.dvi
nipkow@10217
   184
nipkow@10328
   185
## HOL-Types
nipkow@10328
   186
haftmann@27423
   187
HOL-Types: HOL $(LOG)/HOL-Types.gz
nipkow@10328
   188
haftmann@27423
   189
$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \
wenzelm@11858
   190
  Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \
nipkow@10328
   191
  Types/Overloading.thy Types/Axioms.thy
haftmann@27423
   192
	$(USEDIR) Types
wenzelm@42512
   193
	@rm -f Types/document/isabelle.sty
wenzelm@42512
   194
	@rm -f Types/document/isabellesym.sty
wenzelm@42512
   195
	@rm -f Types/document/pdfsetup.sty
wenzelm@42512
   196
	@rm -f Types/document/session.tex
nipkow@10328
   197
	@rm -f tutorial.dvi
nipkow@10328
   198
nipkow@8743
   199
## HOL-Misc
nipkow@8743
   200
nipkow@8743
   201
HOL-Misc: HOL $(LOG)/HOL-Misc.gz
nipkow@8743
   202
nipkow@9722
   203
$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
nipkow@13305
   204
  Misc/Plus.thy Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy \
nipkow@13305
   205
  Misc/Option2.thy Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
nipkow@10978
   206
  Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy
nipkow@10676
   207
	$(USEDIR) Misc
wenzelm@42512
   208
	@rm -f Misc/document/isabelle.sty
wenzelm@42512
   209
	@rm -f Misc/document/isabellesym.sty
wenzelm@42512
   210
	@rm -f Misc/document/pdfsetup.sty
wenzelm@42512
   211
	@rm -f Misc/document/session.tex
nipkow@8754
   212
	@rm -f tutorial.dvi
nipkow@8743
   213
nipkow@8743
   214
paulson@11249
   215
## HOL-Protocol
paulson@11249
   216
paulson@11249
   217
HOL-Protocol: HOL $(LOG)/HOL-Protocol.gz
paulson@11249
   218
paulson@11249
   219
$(LOG)/HOL-Protocol.gz: $(OUT)/HOL Protocol/ROOT.ML  \
berghofe@23926
   220
  Protocol/Message.thy Protocol/Event.thy \
berghofe@23926
   221
  Protocol/Public.thy Protocol/NS_Public.thy    
paulson@11249
   222
	$(USEDIR) Protocol
wenzelm@42512
   223
	@rm -f Protocol/document/isabelle.sty
wenzelm@42512
   224
	@rm -f Protocol/document/isabellesym.sty
wenzelm@42512
   225
	@rm -f Protocol/document/pdfsetup.sty
wenzelm@42512
   226
	@rm -f Protocol/document/session.tex
paulson@11249
   227
	@rm -f tutorial.dvi
paulson@11249
   228
wenzelm@11647
   229
## HOL-Documents
wenzelm@11647
   230
wenzelm@11647
   231
HOL-Documents: HOL $(LOG)/HOL-Documents.gz
wenzelm@11647
   232
wenzelm@11647
   233
$(LOG)/HOL-Documents.gz: $(OUT)/HOL Documents/Documents.thy Documents/ROOT.ML
wenzelm@11647
   234
	$(USEDIR) Documents
wenzelm@42512
   235
	@rm -f Documents/document/isabelle.sty
wenzelm@42512
   236
	@rm -f Documents/document/isabellesym.sty
wenzelm@42512
   237
	@rm -f Documents/document/pdfsetup.sty
wenzelm@42512
   238
	@rm -f Documents/document/session.tex
wenzelm@11647
   239
	@rm -f tutorial.dvi
wenzelm@11647
   240
nipkow@8743
   241
## clean
nipkow@8743
   242
nipkow@8743
   243
clean:
nipkow@25281
   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