doc-src/TutorialI/IsaMakefile
author paulson
Tue Apr 10 16:11:01 2001 +0200 (2001-04-10)
changeset 11249 a0e3c67c1394
parent 11203 881222d48777
child 11279 aaa0ad8fea6b
permissions -rw-r--r--
Protocols chapter
nipkow@8743
     1
#
nipkow@8743
     2
# IsaMakefile for Tutorial
nipkow@8743
     3
#
nipkow@8743
     4
nipkow@8743
     5
## targets
nipkow@8743
     6
paulson@11249
     7
default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Real-Types HOL-Misc HOL-Protocol styles
wenzelm@9520
     8
images:
wenzelm@9520
     9
test:
wenzelm@9520
    10
all: default
nipkow@8743
    11
nipkow@8743
    12
nipkow@8743
    13
## global settings
nipkow@8743
    14
nipkow@8743
    15
SRC = $(ISABELLE_HOME)/src
nipkow@8743
    16
OUT = $(ISABELLE_OUTPUT)
nipkow@8743
    17
LOG = $(OUT)/log
wenzelm@10682
    18
USEDIR = @$(ISATOOL) usedir -m brackets -i true -d dvi -D document $(OUT)/HOL
paulson@10765
    19
REALUSEDIR = @$(ISATOOL) usedir -m brackets -i true -d dvi -D document $(OUT)/HOL-Real
nipkow@8743
    20
nipkow@8743
    21
## HOL
nipkow@8743
    22
nipkow@8743
    23
HOL:
nipkow@8743
    24
	@cd $(SRC)/HOL; $(ISATOOL) make HOL
nipkow@8743
    25
paulson@10765
    26
HOL-Real:
paulson@10765
    27
	@cd $(SRC)/HOL; $(ISATOOL) make HOL-Real
paulson@10765
    28
wenzelm@8825
    29
styles:
nipkow@10654
    30
	@rm -f isabelle.sty
nipkow@10654
    31
	@rm -f isabellesym.sty
nipkow@10654
    32
	@rm -f pdfsetup.sty
wenzelm@8847
    33
	@$(ISATOOL) latex -o sty >/dev/null
wenzelm@8847
    34
	@rm -f pdfsetup.sty
wenzelm@8825
    35
	@rm -f */document/isabelle.sty
wenzelm@8825
    36
	@rm -f */document/isabellesym.sty
wenzelm@8825
    37
	@rm -f */document/pdfsetup.sty
wenzelm@10002
    38
	@rm -f */document/session.tex
nipkow@8743
    39
nipkow@8743
    40
nipkow@8743
    41
## HOL-Ifexpr
nipkow@8743
    42
nipkow@8743
    43
HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz
nipkow@8743
    44
nipkow@8743
    45
$(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML
nipkow@10676
    46
	$(USEDIR) Ifexpr
nipkow@8754
    47
	@rm -f tutorial.dvi
nipkow@8743
    48
nipkow@8743
    49
## HOL-ToyList
nipkow@8743
    50
nipkow@8743
    51
HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz
nipkow@8743
    52
nipkow@8743
    53
ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2
nipkow@8743
    54
	cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy
nipkow@8743
    55
nipkow@8743
    56
$(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML
nipkow@10676
    57
	$(USEDIR) ToyList2
nipkow@8754
    58
	@rm -f tutorial.dvi
nipkow@8743
    59
nipkow@8743
    60
$(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML
nipkow@10676
    61
	$(USEDIR) ToyList
nipkow@8754
    62
	@rm -f tutorial.dvi
nipkow@8743
    63
nipkow@8743
    64
## HOL-CodeGen
nipkow@8743
    65
nipkow@8743
    66
HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz
nipkow@8743
    67
nipkow@10676
    68
$(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/ROOT.ML CodeGen/CodeGen.thy
nipkow@10676
    69
	$(USEDIR) CodeGen
nipkow@8754
    70
	@rm -f tutorial.dvi
nipkow@8743
    71
nipkow@8743
    72
nipkow@8743
    73
## HOL-Datatype
nipkow@8743
    74
nipkow@8743
    75
HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz
nipkow@8743
    76
nipkow@8751
    77
$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \
nipkow@9666
    78
  Datatype/Nested.thy Datatype/unfoldnested.thy \
nipkow@9644
    79
  Datatype/Fundata.thy
nipkow@10676
    80
	$(USEDIR) Datatype
nipkow@8754
    81
	@rm -f tutorial.dvi
nipkow@8743
    82
nipkow@8743
    83
nipkow@8743
    84
## HOL-Trie
nipkow@8743
    85
nipkow@8743
    86
HOL-Trie: HOL $(LOG)/HOL-Trie.gz
nipkow@8743
    87
nipkow@10543
    88
$(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy
nipkow@10676
    89
	$(USEDIR) Trie
nipkow@8754
    90
	@rm -f tutorial.dvi
nipkow@8743
    91
nipkow@8743
    92
nipkow@8743
    93
## HOL-Recdef
nipkow@8743
    94
nipkow@8743
    95
HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz
nipkow@8743
    96
nipkow@10186
    97
$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \
nipkow@9644
    98
  Recdef/simplification.thy Recdef/Induction.thy \
nipkow@10187
    99
  Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy
nipkow@10676
   100
	$(USEDIR) Recdef
nipkow@8754
   101
	@rm -f tutorial.dvi
nipkow@8743
   102
nipkow@8743
   103
nipkow@9933
   104
## HOL-Advanced
nipkow@9933
   105
nipkow@9933
   106
HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz
nipkow@9933
   107
nipkow@10654
   108
$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML Advanced/WFrec.thy \
nipkow@10654
   109
	Advanced/Partial.thy
nipkow@10676
   110
	$(USEDIR) Advanced
nipkow@9933
   111
	@rm -f tutorial.dvi
nipkow@9933
   112
paulson@10296
   113
## HOL-Rules
paulson@10296
   114
paulson@10296
   115
HOL-Rules: HOL $(LOG)/HOL-Rules.gz
paulson@10296
   116
paulson@10296
   117
$(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \
paulson@10956
   118
	Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \
paulson@10956
   119
	Rules/Tacticals.thy Rules/ROOT.ML 
paulson@10840
   120
	@$(USEDIR) Rules
paulson@10296
   121
	@rm -f tutorial.dvi
paulson@10296
   122
paulson@10296
   123
## HOL-Sets
paulson@10296
   124
paulson@10296
   125
HOL-Sets: HOL $(LOG)/HOL-Sets.gz
paulson@10296
   126
paulson@10296
   127
$(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \
paulson@10296
   128
	Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML
paulson@10840
   129
	@$(USEDIR) Sets
paulson@10296
   130
	@rm -f tutorial.dvi
paulson@10296
   131
nipkow@9958
   132
## HOL-CTL
nipkow@9958
   133
nipkow@9958
   134
HOL-CTL: HOL $(LOG)/HOL-CTL.gz
nipkow@9958
   135
nipkow@10212
   136
$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML
nipkow@10676
   137
	$(USEDIR) CTL
nipkow@9958
   138
	@rm -f tutorial.dvi
nipkow@9958
   139
nipkow@10217
   140
## HOL-Inductive
nipkow@10217
   141
nipkow@10217
   142
HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz
nipkow@10217
   143
nipkow@10225
   144
$(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \
nipkow@10762
   145
  Inductive/Even.thy Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \
nipkow@10762
   146
  Inductive/Advanced.thy
nipkow@10676
   147
	$(USEDIR) Inductive
nipkow@10217
   148
	@rm -f tutorial.dvi
nipkow@10217
   149
nipkow@10328
   150
## HOL-Types
nipkow@10328
   151
nipkow@10791
   152
HOL-Real-Types: HOL-Real $(LOG)/HOL-Real-Types.gz
nipkow@10328
   153
nipkow@10791
   154
$(LOG)/HOL-Real-Types.gz: $(OUT)/HOL-Real Types/ROOT.ML \
paulson@10598
   155
  Types/Numbers.thy Types/Pairs.thy Types/Typedef.thy \
nipkow@10328
   156
  Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
nipkow@10328
   157
  Types/Overloading.thy Types/Axioms.thy
paulson@10765
   158
	$(REALUSEDIR) Types
nipkow@10328
   159
	@rm -f tutorial.dvi
nipkow@10328
   160
nipkow@8743
   161
## HOL-Misc
nipkow@8743
   162
nipkow@8743
   163
HOL-Misc: HOL $(LOG)/HOL-Misc.gz
nipkow@8743
   164
nipkow@9722
   165
$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
nipkow@10543
   166
  Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \
nipkow@11203
   167
  Misc/types.thy Misc/prime_def.thy Misc/Translations.thy Misc/case_exprs.thy \
nipkow@10978
   168
  Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy
nipkow@10676
   169
	$(USEDIR) Misc
nipkow@8754
   170
	@rm -f tutorial.dvi
nipkow@8743
   171
nipkow@8743
   172
paulson@11249
   173
## HOL-Protocol
paulson@11249
   174
paulson@11249
   175
HOL-Protocol: HOL $(LOG)/HOL-Protocol.gz
paulson@11249
   176
paulson@11249
   177
$(LOG)/HOL-Protocol.gz: $(OUT)/HOL Protocol/ROOT.ML  \
paulson@11249
   178
  Protocol/Message.thy Protocol/Message_lemmas.ML  \
paulson@11249
   179
  Protocol/Event.thy Protocol/Event_lemmas.ML  \
paulson@11249
   180
  Protocol/Public.thy Protocol/Public_lemmas.ML \
paulson@11249
   181
  Protocol/NS_Public.thy    
paulson@11249
   182
	$(USEDIR) Protocol
paulson@11249
   183
	@rm -f tutorial.dvi
paulson@11249
   184
nipkow@8743
   185
## clean
nipkow@8743
   186
nipkow@8743
   187
clean:
paulson@11249
   188
	@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