src/HOL/IsaMakefile
author paulson
Tue Jul 22 11:16:57 1997 +0200 (1997-07-22)
changeset 3540 acd60238f191
parent 3505 1cb4ea47d967
child 3616 fcd7e70258f7
permissions -rw-r--r--
Fixed the spelling of AUTH_NAMES--it could not have worked before\!
wenzelm@2448
     1
#
wenzelm@2448
     2
# $Id$
wenzelm@2448
     3
#
wenzelm@2448
     4
# IsaMakefile for HOL
wenzelm@2448
     5
#
wenzelm@2448
     6
wenzelm@2448
     7
#### Base system
wenzelm@2448
     8
wenzelm@3118
     9
OUT = $(ISABELLE_OUTPUT)
wenzelm@2448
    10
paulson@3195
    11
NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
nipkow@3025
    12
	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
paulson@3390
    13
	Divides Power Sexp Univ List RelPow Option
wenzelm@2448
    14
paulson@3232
    15
PROVERS = hypsubst.ML classical.ML blast.ML \
paulson@3232
    16
	simplifier.ML splitter.ML nat_transitive.ML 
paulson@3232
    17
paulson@3354
    18
TFL   = dcterm.sml post.sml rules.new.sml rules.sig \
paulson@3232
    19
	sys.sml tfl.sig tfl.sml thms.sig thms.sml thry.sig thry.sml   \
paulson@3232
    20
	usyntax.sig usyntax.sml utils.sig utils.sml
paulson@3232
    21
wenzelm@2448
    22
FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
wenzelm@2448
    23
	ind_syntax.ML cladata.ML simpdata.ML \
wenzelm@2448
    24
	typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML \
paulson@3232
    25
	$(NAMES:%=%.thy) $(NAMES:%=%.ML) $(TFL:%=../TFL/%) \
paulson@3232
    26
	$(PROVERS:%=../Provers/%)
wenzelm@2448
    27
wenzelm@2448
    28
$(OUT)/HOL: $(OUT)/Pure $(FILES)
wenzelm@2826
    29
	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
wenzelm@2448
    30
wenzelm@2448
    31
$(OUT)/Pure:
wenzelm@2473
    32
	@cd ../Pure; $(ISATOOL) make
wenzelm@2448
    33
wenzelm@2448
    34
wenzelm@2473
    35
#### Tests and examples
wenzelm@2473
    36
paulson@3125
    37
## Inductive definitions: simple examples
paulson@3125
    38
paulson@3125
    39
INDUCT_FILES =  Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult
paulson@3125
    40
paulson@3125
    41
INDUCT_FILES = Induct/ROOT.ML \
paulson@3125
    42
	    $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML)
paulson@3125
    43
paulson@3125
    44
Induct:	$(OUT)/HOL $(INDUCT_FILES)
paulson@3125
    45
	@$(ISATOOL) usedir $(OUT)/HOL Induct
paulson@3125
    46
paulson@3125
    47
wenzelm@2448
    48
## IMP-semantics example
wenzelm@2448
    49
wenzelm@2448
    50
IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
wenzelm@2448
    51
IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
wenzelm@2448
    52
wenzelm@2448
    53
IMP:	$(OUT)/HOL $(IMP_FILES)
wenzelm@2826
    54
	@$(ISATOOL) usedir $(OUT)/HOL IMP
wenzelm@2448
    55
wenzelm@2448
    56
wenzelm@2448
    57
## Hoare logic
wenzelm@2448
    58
wenzelm@2448
    59
Hoare_NAMES = Hoare Arith2 Examples
wenzelm@2448
    60
Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
wenzelm@2448
    61
	      $(Hoare_NAMES:%=Hoare/%.ML)
wenzelm@2448
    62
wenzelm@2448
    63
Hoare:	$(OUT)/HOL $(Hoare_FILES)
wenzelm@2826
    64
	@$(ISATOOL) usedir $(OUT)/HOL Hoare
wenzelm@2448
    65
wenzelm@2448
    66
wenzelm@2448
    67
## The integers in HOL
wenzelm@2448
    68
wenzelm@2448
    69
INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing
wenzelm@2448
    70
wenzelm@2448
    71
INTEG_FILES = Integ/ROOT.ML \
wenzelm@2448
    72
	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
wenzelm@2448
    73
wenzelm@2448
    74
Integ:	$(OUT)/HOL $(INTEG_FILES)
wenzelm@2826
    75
	@$(ISATOOL) usedir $(OUT)/HOL Integ
wenzelm@2448
    76
wenzelm@2448
    77
mueller@3079
    78
## I/O Automata (meta theory only)
wenzelm@2448
    79
wenzelm@2448
    80
mueller@3079
    81
IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \
mueller@3079
    82
  IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML
wenzelm@2448
    83
mueller@3079
    84
IOA: $(OUT)/HOL $(IOA_FILES)
mueller@3079
    85
	@$(ISATOOL) usedir $(OUT)/HOL IOA
wenzelm@2448
    86
wenzelm@2448
    87
wenzelm@2448
    88
## Authentication & Security Protocols
wenzelm@2448
    89
paulson@3540
    90
AUTH_NAMES = Message Event Shared NS_Shared \
paulson@3540
    91
	     OtwayRees OtwayRees_AN OtwayRees_Bad \
paulson@3482
    92
	     Recur WooLam Yahalom Yahalom2 \
paulson@3482
    93
	     Public NS_Public_Bad NS_Public TLS
wenzelm@2448
    94
wenzelm@2448
    95
AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
wenzelm@2448
    96
wenzelm@2448
    97
Auth:	$(OUT)/HOL $(AUTH_FILES)
wenzelm@2826
    98
	@$(ISATOOL) usedir $(OUT)/HOL Auth
wenzelm@2448
    99
wenzelm@2448
   100
mueller@3218
   101
## Modelchecker invocation
mueller@3218
   102
mueller@3218
   103
MC_FILES = Modelcheck/CTL.thy Modelcheck/Example.ML \
mueller@3218
   104
  Modelcheck/Example.thy Modelcheck/MCSyn.ML Modelcheck/MCSyn.thy \
mueller@3218
   105
  Modelcheck/MuCalculus.ML Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML
mueller@3218
   106
mueller@3218
   107
Modelcheck: $(OUT)/HOL $(MC_FILES)
mueller@3218
   108
	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
mueller@3218
   109
mueller@3218
   110
wenzelm@2448
   111
## Properties of substitutions
wenzelm@2448
   112
paulson@3195
   113
SUBST_NAMES = AList Subst Unifier UTerm Unify
wenzelm@2448
   114
wenzelm@2448
   115
SUBST_FILES = Subst/ROOT.ML \
wenzelm@2448
   116
	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
wenzelm@2448
   117
wenzelm@2448
   118
Subst:	$(OUT)/HOL $(SUBST_FILES)
wenzelm@2826
   119
	@$(ISATOOL) usedir $(OUT)/HOL Subst
wenzelm@2448
   120
wenzelm@2448
   121
wenzelm@2448
   122
## Confluence of Lambda-calculus
wenzelm@2448
   123
wenzelm@2448
   124
LAMBDA_NAMES = Lambda ParRed Commutation Eta
wenzelm@2448
   125
wenzelm@2448
   126
LAMBDA_FILES = Lambda/ROOT.ML \
wenzelm@2448
   127
	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
wenzelm@2448
   128
wenzelm@2448
   129
Lambda:	 $(OUT)/HOL $(LAMBDA_FILES)
wenzelm@2826
   130
	@$(ISATOOL) usedir $(OUT)/HOL Lambda
wenzelm@2448
   131
wenzelm@2448
   132
nipkow@2527
   133
## Type inference without let
nipkow@2527
   134
nipkow@2527
   135
W0_NAMES = I Maybe MiniML Type W
nipkow@2527
   136
nipkow@2527
   137
W0_FILES = W0/ROOT.ML \
nipkow@2527
   138
	      $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)
wenzelm@2448
   139
nipkow@2527
   140
W0: $(OUT)/HOL $(W0_FILES)
wenzelm@2826
   141
	@$(ISATOOL) usedir $(OUT)/HOL W0
nipkow@2527
   142
nipkow@2527
   143
nipkow@2527
   144
## Type inference with let
nipkow@2527
   145
nipkow@2527
   146
MINIML_NAMES = Generalize Instance Maybe MiniML Type W
wenzelm@2448
   147
wenzelm@2448
   148
MINIML_FILES = MiniML/ROOT.ML \
wenzelm@2448
   149
	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
wenzelm@2448
   150
wenzelm@2448
   151
MiniML: $(OUT)/HOL $(MINIML_FILES)
wenzelm@2826
   152
	@$(ISATOOL) usedir $(OUT)/HOL MiniML
wenzelm@2448
   153
wenzelm@2448
   154
wenzelm@2448
   155
## Lexical analysis
wenzelm@2448
   156
wenzelm@2448
   157
LEX_FILES = Auto AutoChopper Chopper Prefix
wenzelm@2448
   158
wenzelm@2448
   159
LEX_FILES = Lex/ROOT.ML \
wenzelm@2448
   160
	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
wenzelm@2448
   161
wenzelm@2448
   162
Lex:	$(OUT)/HOL $(LEX_FILES)
wenzelm@2826
   163
	@$(ISATOOL) usedir $(OUT)/HOL Lex
wenzelm@2448
   164
wenzelm@2448
   165
wenzelm@2545
   166
## Axiomatic type classes examples
wenzelm@2545
   167
wenzelm@2545
   168
AXC_GROUP_FILES = Group.ML Group.thy GroupDefs.ML GroupDefs.thy \
wenzelm@2545
   169
	GroupInsts.thy Monoid.thy MonoidGroupInsts.thy ROOT.ML Sigs.thy
wenzelm@2545
   170
wenzelm@2545
   171
AXC_LATTICE_FILES = CLattice.ML CLattice.thy LatInsts.ML LatInsts.thy \
wenzelm@2545
   172
	LatMorph.ML LatMorph.thy LatPreInsts.ML LatPreInsts.thy \
wenzelm@2545
   173
	Lattice.ML Lattice.thy OrdDefs.ML OrdDefs.thy OrdInsts.thy \
wenzelm@2545
   174
	Order.ML Order.thy ROOT.ML tools.ML
wenzelm@2545
   175
wenzelm@2545
   176
AXC_TUTORIAL_FILES = BoolGroupInsts.thy Group.ML Group.thy Monoid.thy \
wenzelm@2545
   177
	MonoidGroupInsts.thy ProdGroupInsts.thy Product.thy \
wenzelm@2545
   178
	ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \
wenzelm@2545
   179
	Xor.ML Xor.thy
wenzelm@2545
   180
wenzelm@2545
   181
AXCLASSES_FILES = AxClasses/ROOT.ML \
wenzelm@2545
   182
	$(AXC_GROUP_FILES:%=AxClasses/Group/%) \
wenzelm@2545
   183
	$(AXC_LATTICE_FILES:%=AxClasses/Lattice/%) \
wenzelm@2545
   184
	$(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)
wenzelm@2545
   185
wenzelm@2545
   186
AxClasses: $(OUT)/HOL $(AXCLASSES_FILES)
wenzelm@2826
   187
	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
wenzelm@2827
   188
	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
wenzelm@2827
   189
	@$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice
wenzelm@2827
   190
	@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
wenzelm@2545
   191
wenzelm@2545
   192
slotosch@2909
   193
## Higher-order quotients and example fractionals
wenzelm@2900
   194
slotosch@2909
   195
QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \
slotosch@2909
   196
	Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \
slotosch@2909
   197
	Quot/FRACT.thy Quot/FRACT.ML
wenzelm@2900
   198
Quot:	$(OUT)/HOL $(QUOT_FILES)
wenzelm@2900
   199
	@$(ISATOOL) usedir $(OUT)/HOL Quot
wenzelm@2900
   200
wenzelm@2900
   201
wenzelm@2448
   202
## Miscellaneous examples
wenzelm@2448
   203
paulson@3417
   204
EX_NAMES = Recdef Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT
wenzelm@2448
   205
wenzelm@2448
   206
EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
wenzelm@2448
   207
	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
wenzelm@2448
   208
wenzelm@2448
   209
ex:	$(OUT)/HOL $(EX_FILES)
wenzelm@2826
   210
	@$(ISATOOL) usedir $(OUT)/HOL ex
wenzelm@2448
   211
wenzelm@2448
   212
wenzelm@2448
   213
## Full test
wenzelm@2448
   214
oheimb@2635
   215
test:	$(OUT)/HOL \
mueller@3218
   216
		Subst Induct IMP Hoare Lex Integ Auth Modelcheck Lambda  \
paulson@3125
   217
		W0 MiniML IOA AxClasses Quot ex
wenzelm@2448
   218
	echo 'Test examples ran successfully' > test
wenzelm@2448
   219
wenzelm@2448
   220
wenzelm@2448
   221
.PRECIOUS: $(OUT)/Pure $(OUT)/HOL