wneuper/isa: doc-src/TutorialI/IsaMakefile@778f0897e7e5

1 #

     2 # IsaMakefile for Tutorial

3 #

     5 ## targets

     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 styles

     8 images:

     9 test:

    10 all: default

    13 ## global settings

    15 SRC = $(ISABELLE_HOME)/src

    16 OUT = $(ISABELLE_OUTPUT)

    17 LOG = $(OUT)/log

    18 USEDIR = @$(ISATOOL) usedir -m brackets -i true -d dvi -D document $(OUT)/HOL

    19 REALUSEDIR = @$(ISATOOL) usedir -m brackets -i true -d dvi -D document $(OUT)/HOL-Real

    21 ## HOL

    23 HOL:

    24 	@cd $(SRC)/HOL; $(ISATOOL) make HOL

    26 HOL-Real:

    27 	@cd $(SRC)/HOL; $(ISATOOL) make HOL-Real

    29 styles:

    30 	@rm -f isabelle.sty

    31 	@rm -f isabellesym.sty

    32 	@rm -f pdfsetup.sty

    33 	@$(ISATOOL) latex -o sty >/dev/null

    34 	@rm -f pdfsetup.sty

    35 	@rm -f */document/isabelle.sty

    36 	@rm -f */document/isabellesym.sty

    37 	@rm -f */document/pdfsetup.sty

    38 	@rm -f */document/session.tex

    41 ## HOL-Ifexpr

    43 HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz

    45 $(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML

    46 	$(USEDIR) Ifexpr

    47 	@rm -f tutorial.dvi

    49 ## HOL-ToyList

    51 HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz

    53 ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2

    54 	cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy

    56 $(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML

    57 	$(USEDIR) ToyList2

    58 	@rm -f tutorial.dvi

    60 $(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML

    61 	$(USEDIR) ToyList

    62 	@rm -f tutorial.dvi

    64 ## HOL-CodeGen

    66 HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz

    68 $(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/ROOT.ML CodeGen/CodeGen.thy

    69 	$(USEDIR) CodeGen

    70 	@rm -f tutorial.dvi

    73 ## HOL-Datatype

    75 HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz

    77 $(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \

    78   Datatype/Nested.thy Datatype/unfoldnested.thy \

    79   Datatype/Fundata.thy

    80 	$(USEDIR) Datatype

    81 	@rm -f tutorial.dvi

    84 ## HOL-Trie

    86 HOL-Trie: HOL $(LOG)/HOL-Trie.gz

    88 $(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy

    89 	$(USEDIR) Trie

    90 	@rm -f tutorial.dvi

    93 ## HOL-Recdef

    95 HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz

    97 $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \

    98   Recdef/simplification.thy Recdef/Induction.thy \

    99   Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy

   100 	$(USEDIR) Recdef

   101 	@rm -f tutorial.dvi

   104 ## HOL-Advanced

   106 HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz

   108 $(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML Advanced/WFrec.thy \

   109 	Advanced/Partial.thy

   110 	$(USEDIR) Advanced

   111 	@rm -f tutorial.dvi

   113 ## HOL-Rules

   115 HOL-Rules: HOL $(LOG)/HOL-Rules.gz

   117 $(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \

   118 	Rules/Blast.thy Rules/Force.thy Rules/Primes.thy  \

   119 	Rules/ROOT.ML

   120 	@$(ISATOOL) usedir -d dvi -D document $(OUT)/HOL Rules

   121 	@rm -f tutorial.dvi

   123 ## HOL-Sets

   125 HOL-Sets: HOL $(LOG)/HOL-Sets.gz

   127 $(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \

   128 	Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML

   129 	@$(ISATOOL) usedir -d dvi -D document $(OUT)/HOL Sets

   130 	@rm -f tutorial.dvi

   132 ## HOL-CTL

   134 HOL-CTL: HOL $(LOG)/HOL-CTL.gz

   136 $(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML

   137 	$(USEDIR) CTL

   138 	@rm -f tutorial.dvi

   140 ## HOL-Inductive

   142 HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz

   144 $(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \

   145   Inductive/Even.thy Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \

   146   Inductive/Advanced.thy

   147 	$(USEDIR) Inductive

   148 	@rm -f tutorial.dvi

   150 ## HOL-Types

   152 HOL-Real-Types: HOL-Real $(LOG)/HOL-Real-Types.gz

   154 $(LOG)/HOL-Real-Types.gz: $(OUT)/HOL-Real Types/ROOT.ML \

   155   Types/Numbers.thy Types/Pairs.thy Types/Typedef.thy \

   156   Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \

   157   Types/Overloading.thy Types/Axioms.thy

   158 	$(REALUSEDIR) Types

   159 	@rm -f tutorial.dvi

   161 ## HOL-Misc

   163 HOL-Misc: HOL $(LOG)/HOL-Misc.gz

   165 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \

   166   Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \

   167   Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \

   168   Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy

   169 	$(USEDIR) Misc

   170 	@rm -f tutorial.dvi

   173 ## clean

   175 clean:

   176 	@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

author	nipkow
	Fri, 05 Jan 2001 15:39:34 +0100
changeset 10791	778f0897e7e5
parent 10765	94aa0b568009
child 10840	28a53b68a8c0
permissions	-rw-r--r--