doc-src/TutorialI/IsaMakefile
author nipkow
Wed Dec 13 09:39:53 2000 +0100 (2000-12-13)
changeset 10654 458068404143
parent 10598 f92037156f4d
child 10655 ddd33e0f4935
permissions -rw-r--r--
*** empty log message ***
     1 #
     2 # IsaMakefile for Tutorial
     3 #
     4 
     5 ## targets
     6 
     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-Types HOL-Misc styles
     8 images:
     9 test:
    10 all: default
    11 
    12 
    13 ## global settings
    14 
    15 SRC = $(ISABELLE_HOME)/src
    16 OUT = $(ISABELLE_OUTPUT)
    17 LOG = $(OUT)/log
    18 
    19 
    20 ## HOL
    21 
    22 HOL:
    23 	@cd $(SRC)/HOL; $(ISATOOL) make HOL
    24 
    25 styles:
    26 	@rm -f isabelle.sty
    27 	@rm -f isabellesym.sty
    28 	@rm -f pdfsetup.sty
    29 	@$(ISATOOL) latex -o sty >/dev/null
    30 	@rm -f pdfsetup.sty
    31 	@rm -f */document/isabelle.sty
    32 	@rm -f */document/isabellesym.sty
    33 	@rm -f */document/pdfsetup.sty
    34 	@rm -f */document/session.tex
    35 
    36 
    37 ## HOL-Ifexpr
    38 
    39 HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz
    40 
    41 $(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML
    42 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Ifexpr
    43 	@rm -f tutorial.dvi
    44 
    45 ## HOL-ToyList
    46 
    47 HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz
    48 
    49 ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2
    50 	cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy
    51 
    52 $(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML
    53 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL ToyList2
    54 	@rm -f tutorial.dvi
    55 
    56 $(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML
    57 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL ToyList
    58 	@rm -f tutorial.dvi
    59 
    60 ## HOL-CodeGen
    61 
    62 HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz
    63 
    64 $(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/CodeGen.thy
    65 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CodeGen
    66 	@rm -f tutorial.dvi
    67 
    68 
    69 ## HOL-Datatype
    70 
    71 HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz
    72 
    73 $(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \
    74   Datatype/Nested.thy Datatype/unfoldnested.thy \
    75   Datatype/Fundata.thy
    76 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Datatype
    77 	@rm -f tutorial.dvi
    78 
    79 
    80 ## HOL-Trie
    81 
    82 HOL-Trie: HOL $(LOG)/HOL-Trie.gz
    83 
    84 $(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy
    85 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Trie
    86 	@rm -f tutorial.dvi
    87 
    88 
    89 ## HOL-Recdef
    90 
    91 HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz
    92 
    93 $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \
    94   Recdef/simplification.thy Recdef/Induction.thy \
    95   Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy
    96 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Recdef
    97 	@rm -f tutorial.dvi
    98 
    99 
   100 ## HOL-Advanced
   101 
   102 HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz
   103 
   104 $(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML Advanced/WFrec.thy \
   105 	Advanced/Partial.thy
   106 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Advanced
   107 	@rm -f tutorial.dvi
   108 
   109 ## HOL-Rules
   110 
   111 HOL-Rules: HOL $(LOG)/HOL-Rules.gz
   112 
   113 $(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \
   114 	Rules/Blast.thy Rules/Force.thy Rules/Primes.thy  \
   115 	Rules/ROOT.ML 
   116 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Rules
   117 	@rm -f tutorial.dvi
   118 
   119 ## HOL-Sets
   120 
   121 HOL-Sets: HOL $(LOG)/HOL-Sets.gz
   122 
   123 $(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \
   124 	Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML
   125 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Sets
   126 	@rm -f tutorial.dvi
   127 
   128 ## HOL-CTL
   129 
   130 HOL-CTL: HOL $(LOG)/HOL-CTL.gz
   131 
   132 $(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML
   133 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CTL
   134 	@rm -f tutorial.dvi
   135 
   136 ## HOL-Inductive
   137 
   138 HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz
   139 
   140 $(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \
   141   Inductive/Even.thy Inductive/Star.thy Inductive/AB.thy Inductive/Advanced.thy
   142 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Inductive
   143 	@rm -f tutorial.dvi
   144 
   145 ## HOL-Types
   146 
   147 HOL-Types: HOL $(LOG)/HOL-Types.gz
   148 
   149 $(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \
   150   Types/Numbers.thy Types/Pairs.thy Types/Typedef.thy \
   151   Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
   152   Types/Overloading.thy Types/Axioms.thy
   153 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Types
   154 	@rm -f tutorial.dvi
   155 
   156 ## HOL-Misc
   157 
   158 HOL-Misc: HOL $(LOG)/HOL-Misc.gz
   159 
   160 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
   161   Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \
   162   Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
   163   Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy
   164 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc
   165 	@rm -f tutorial.dvi
   166 
   167 
   168 ## clean
   169 
   170 clean:
   171 	@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