doc-src/TutorialI/IsaMakefile
author nipkow
Wed Apr 19 11:54:39 2000 +0200 (2000-04-19)
changeset 8743 3253c6046d57
child 8751 9ed0548177fb
permissions -rw-r--r--
I wonder if that's all?
nipkow@8743
     1
#
nipkow@8743
     2
# IsaMakefile for Tutorial
nipkow@8743
     3
#
nipkow@8743
     4
nipkow@8743
     5
## targets
nipkow@8743
     6
nipkow@8743
     7
default: styles HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Misc
nipkow@8743
     8
nipkow@8743
     9
nipkow@8743
    10
## global settings
nipkow@8743
    11
nipkow@8743
    12
SRC = $(ISABELLE_HOME)/src
nipkow@8743
    13
OUT = $(ISABELLE_OUTPUT)
nipkow@8743
    14
LOG = $(OUT)/log
nipkow@8743
    15
nipkow@8743
    16
nipkow@8743
    17
## HOL
nipkow@8743
    18
nipkow@8743
    19
HOL:
nipkow@8743
    20
	@cd $(SRC)/HOL; $(ISATOOL) make HOL
nipkow@8743
    21
nipkow@8743
    22
styles: isabelle.sty isabellesym.sty pdfsetup.sty
nipkow@8743
    23
nipkow@8743
    24
isabelle.sty: $(ISABELLE_HOME)/lib/texinputs/isabelle.sty
nipkow@8743
    25
	cp $(ISABELLE_HOME)/lib/texinputs/isabelle.sty .
nipkow@8743
    26
nipkow@8743
    27
isabellesym.sty: $(ISABELLE_HOME)/lib/texinputs/isabellesym.sty
nipkow@8743
    28
	cp $(ISABELLE_HOME)/lib/texinputs/isabellesym.sty .
nipkow@8743
    29
nipkow@8743
    30
pdfsetup.sty: $(ISABELLE_HOME)/lib/texinputs/pdfsetup.sty
nipkow@8743
    31
	cp $(ISABELLE_HOME)/lib/texinputs/pdfsetup.sty .
nipkow@8743
    32
nipkow@8743
    33
nipkow@8743
    34
## HOL-Ifexpr
nipkow@8743
    35
nipkow@8743
    36
HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz
nipkow@8743
    37
nipkow@8743
    38
$(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML
nipkow@8743
    39
	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Ifexpr
nipkow@8743
    40
nipkow@8743
    41
nipkow@8743
    42
## HOL-ToyList
nipkow@8743
    43
nipkow@8743
    44
HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz
nipkow@8743
    45
nipkow@8743
    46
ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2
nipkow@8743
    47
	cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy
nipkow@8743
    48
nipkow@8743
    49
$(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML
nipkow@8743
    50
	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL ToyList2
nipkow@8743
    51
nipkow@8743
    52
$(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML
nipkow@8743
    53
	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL ToyList
nipkow@8743
    54
nipkow@8743
    55
## HOL-CodeGen
nipkow@8743
    56
nipkow@8743
    57
HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz
nipkow@8743
    58
nipkow@8743
    59
$(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/CodeGen.thy
nipkow@8743
    60
	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CodeGen
nipkow@8743
    61
nipkow@8743
    62
nipkow@8743
    63
## HOL-Datatype
nipkow@8743
    64
nipkow@8743
    65
HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz
nipkow@8743
    66
nipkow@8743
    67
$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy Datatype/Nested.thy \
nipkow@8743
    68
  Datatype/Fundata.thy
nipkow@8743
    69
	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Datatype
nipkow@8743
    70
nipkow@8743
    71
nipkow@8743
    72
## HOL-Trie
nipkow@8743
    73
nipkow@8743
    74
HOL-Trie: HOL $(LOG)/HOL-Trie.gz
nipkow@8743
    75
nipkow@8743
    76
$(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/Option2.thy Trie/Trie.thy
nipkow@8743
    77
	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Trie
nipkow@8743
    78
nipkow@8743
    79
nipkow@8743
    80
## HOL-Recdef
nipkow@8743
    81
nipkow@8743
    82
HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz
nipkow@8743
    83
nipkow@8743
    84
$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/examples.thy Recdef/termination.thy \
nipkow@8743
    85
  Recdef/simplification.thy Recdef/Induction.thy
nipkow@8743
    86
	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Recdef
nipkow@8743
    87
nipkow@8743
    88
nipkow@8743
    89
## HOL-Misc
nipkow@8743
    90
nipkow@8743
    91
HOL-Misc: HOL $(LOG)/HOL-Misc.gz
nipkow@8743
    92
nipkow@8743
    93
$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/cases.thy \
nipkow@8743
    94
  Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy Misc/prime_def.thy \
nipkow@8743
    95
  Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy Misc/arith4.thy \
nipkow@8743
    96
  Misc/def_rewr.thy Misc/let_rewr.thy Misc/cond_rewr.thy Misc/case_splits.thy \
nipkow@8743
    97
  Misc/trace_simp.thy Misc/Itrev.thy Misc/asm_simp.thy
nipkow@8743
    98
	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc
nipkow@8743
    99
nipkow@8743
   100
nipkow@8743
   101
## clean
nipkow@8743
   102
nipkow@8743
   103
clean:
nipkow@8743
   104
	@rm -f $(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